Was ist das Curry-Howard-Analogon für lineare Logik?

Wie von Wikipedia definiert,

(Die Curry-Howard-Korrespondenz) ist eine Verallgemeinerung einer syntaktischen Analogie zwischen formalen Logiksystemen und Rechenkalkülen, die erstmals vom amerikanischen Mathematiker Haskell Curry und dem Logiker William Alvin Howard entdeckt wurde.

Damit verbunden ist der λ-Würfel, eine grafische Darstellung der möglichen Verfeinerungsachsen von einfachen Typen bis zur Konstruktionsrechnung, die eine logische Interpretation hat:

Soweit ich weiß, ist die Curry-Howard-Korrespondenz eine Verbindung zwischen Typentheorie und klassischer Logik. Meine Frage ist: Gibt es eine analoge Entsprechung zwischen Typsystemen und linearer Logik?

Sie können ähnliche Anforderungen in Ihr Typsystem stellen, was bedeutet, dass Objekte niemals zerstört oder dupliziert werden müssen. Ein Beispiel für eine praktische Anwendung finden Sie unter Lineare Typen können die Welt verändern! von Philip Wadler, der die Schreibregeln dafür festlegt. Es zeigt auch, wie ein Typsystem lineare und nichtlineare Typen kombinieren kann.

Eine praktische Anwendung finden Sie std::unique_ptrin C ++. Hierbei sorgt die Linearität dafür, dass die Freigabe immer genau einmal erfolgt.

In einer funktionalen Sprache bietet Linearität auch die Möglichkeit destruktiver Aktualisierungen (die dem Programmierer als rein erscheinen). In der Praxis scheinen Monaden jedoch ein häufigerer Ansatz zur Lösung dieses Problems zu sein.

Update : Ich habe festgestellt, dass in der NLab Computational Trinitarianism-Tabelle das Fehlen einer Kontraktion in einer Logik (dh die Unfähigkeit, eine Annahme zu duplizieren) dem No-Cloning-Theorem aus der Quantenmechanik entspricht. Ich verstehe (leider) die Auswirkungen nicht, aber ich dachte, Sie könnten es interessant finden.

Die lineare Logik entspricht einem Typsystem für eine Prozessrechnung (eine Variante der internen π-Rechnung ), wobei:

• Beweise entsprechen Prozessen ;
• Vorschläge entsprechen Sitzungstypen (Kommunikationsprotokollen).

Dies ist ein ziemlich aktives Forschungsgebiet. Während die Menschen seit der Einführung der linearen Logik durch Girard [1987] eine Entsprechung zwischen linearer Logik und einem Parallelitätsmodell erwarteten, war es etwas schwierig, etwas zu finden, das sowohl aus der Perspektive der logischen als auch der Parallelitätsmodellierung zufriedenstellend ist.

Hier finden Sie eine Zusammenfassung der wichtigsten Entwicklungen.

• $A \otimes B$$A$$B$$A$$B$(ein Paar, wenn Sie möchten), und dann darf der Kanal nicht mehr verwendet werden. Die Schlüsselidee ist, dass die Schnittregel der linearen Logik verwendet werden kann, um die parallele Ausführung von zwei Prozessen zu tippen, die über einen privaten Kanal kommunizieren. Die von der Schnittregel in linearer Logik durchgeführte Dualitätsprüfung entspricht der Überprüfung, ob die beiden Prozesse den gemeinsam genutzten privaten Kanal auf kompatible Weise verwenden.
• Die Idee der Dualität inspirierte auch mehrere Typisierungsdisziplinen für Prozesskalküle, insbesondere lineare Typen und Sitzungstypen, aber die direkte Verbindung zur linearen Logik ging verloren. Insbesondere Sitzungstypen von Honda [1993] beschreiben Kommunikationsprotokolle, und ihre Anwendbarkeit wurde ziemlich bald offensichtlich: Die Idee brachte einen Forschungsbereich hervor.
• $A \otimes B$$A$$B$
• Wadler [2014] formulierte die Korrespondenz mit Sitzungstypen für die klassische lineare Logik neu und formalisierte die erste Verbindung zwischen einer Standarddarstellung von Sitzungstypen für eine funktionale Sprache und linearer Logik.
• $P|Q$$\otimes$

Wenn Sie nach ein paar Artikeln suchen, um loszulegen, würde ich von [Wadler, 2014] und dann von [Kokke et al., 2019] ausgehen (um das neueste System zu sehen).