In Girards Beweisen und Typen können wir lesen:
Aus algorithmischer Sicht weist der sequentielle Kalkül keinen Curry-Howard-Isomorphismus auf, da es eine Vielzahl von Möglichkeiten gibt, denselben Beweis zu schreiben. Dies hindert uns daran, es als typisierten Kalkül zu verwenden, obwohl wir eine tiefe Struktur dieser Art sehen, die wahrscheinlich mit Parallelität verbunden ist.
Beweise und Typen , JY Girard (Seite 28)
Aber wir können das auch lesen (über lineare Logik)
Aus Sicht der Informatik bietet es einen neuen Ansatz für Fragen der Faulheit, der Nebenwirkungen und der Speicherzuordnung [GirLaf, Laf87, Laf88] mit vielversprechenden Anwendungen für die Parallelität.
Beweise und Typen , JY Girard (Seite 149, geschrieben von Yves Lafont)
Wie sind parallele Programme mit dem Curry-Howard-Isomorphismus verbunden? Was sind die aktuellen Gedanken dazu?
par
, um dies zu steuern (dh , es könnte standardmäßig eine weniger parallele Reduktionsreihenfolge verwendet werden, die selektiv paralleler gestaltet werden könnte), aber sie hätten keine logische Bedeutung.Für die Parallelität im Allgemeinen gibt es eine sehr aktive Forschungslinie, die ich in dieser Antwort zusammenzufassen versuchte: /cs//a/102711/98901
Ich füge hier unten einen Kommentar zur Parallelität hinzu.
Avron [1996] führte den Begriff der Hypersequenzen ein , dh Sammlungen von Sequenzen in Urteilen.
Wir haben gerade angefangen, die Oberfläche der semantischen Interpretation zu kratzen, aber dass dies Parallelität ist, ist ziemlich offensichtlich: Die Semantik der parallelen Komposition ermöglicht es, simultane Aktionen aus beiden Prozessen zu sehen, und es gibt einen Satz in der Arbeit, der besagt, dass keiner von beiden Die beiden Prozesse müssen warten, bis der andere mindestens eine Aktion ausführt (der Bereitschaftssatz). Die Erweiterung auf mehr als zwei Aktionen gleichzeitig scheint unkompliziert. (Die Eingabe erlaubt es bereits, aber die Semantik in diesem Artikel nutzt es nicht vollständig aus.)
quelle