Wenn Sie sich die rekursiven Kombinatoren im untypisierten Lambda-Kalkül ansehen, wie den Y-Kombinator oder den Omega-Kombinator: Es ist klar, dass all diese Kombinatoren eine Variable irgendwo in ihrer Definition duplizieren.
Darüber hinaus sind alle diese Kombinatoren im einfach typisierten Lambda-Kalkül typisierbar, wenn Sie ihn mit den rekursiven Typen , wobei im rekursiven Typ negativ vorkommen darf.
Was passiert jedoch, wenn Sie dem exponentialfreien Fragment der linearen Logik (dh MALL) vollständige (negativ auftretende) rekursive Typen hinzufügen?
Dann haben Sie kein Exponential , um sich zusammenzuziehen. Sie können die Art der Exponentiale mit etwas wie aber ich verstehe nicht, wie ich die Einführungsregel dafür definieren soll, da dies einen Festkomma-Kombinator zu erfordern scheint. Und ich habe versucht, Exponentiale zu definieren, Kontraktion zu bekommen, einen Fixpunkt-Kombinator zu bekommen!
Ist es so, dass sich MALL plus uneingeschränkte rekursive Typen immer noch normalisieren?
quelle
Antworten:
Wenn additive Kommutierungen in MALL weggelassen werden, ist es einfach zu zeigen, dass die Größe eines Proofs mit jedem Schnitteliminierungsschritt abnimmt. Wenn additive Kommutierungen zulässig sind, ist der Beweis nicht so einfach, er wurde jedoch im Originalpapier „Lineare Logik“ bereitgestellt. Es heißt Small Normalization Theorem (Korollar 4.22, S. 71), das besagt, dass die Normalisierung gilt, solange die Kontraktionsförderungsregel nicht involviert ist (was in MALL der Fall ist). Das Argument beruht nicht auf Formeln selbst, sie können unendlich sein (z. B. rekursiv definiert).
Dies bedeutet, dass es nicht möglich ist, eine Promotion für den Typ in MALL, da dies Fixpunktkombinatoren erlauben würde. Dazu wäre ein zusätzliches Rekursionskonstrukt erforderlich.μ α .ich&EIN&( α ⊗ α )
Hinweis: Ich glaube, dass es möglich ist, MALL zusammen mit einem Coinduktionsprinzip (Einführung von 's dual) zu verwenden, um das System zu normalisieren und eine Promotion für diese Codierung von . Das Zulassen rekursiver Typen in der MALL + -Koinduktion würde Turing dann vervollständigen. Solange MALL allein betrachtet wird, ist es jedoch keine große Sache, rekursive Typen zuzulassen.μ ! EIN
quelle