Gibt es Zwischen-Eta-Theorien für die Lambda-Rechnung?

15

Es gibt zwei Haupttheorien des Lambda-Kalküls, die Beta-Theorie und die Post-Complete-Erweiterung, die Beta-Eta-Theorie.

Haben diese beiden Theorien eine Zwischenregel, eine Art Zwischenregel, die eine konfluente Neuschreibungstheorie liefert? Gibt es eine interessante Vorstellung von partieller Extensionalität, der sie entspricht?

Dies ist die zweite Frage , die ich auf der Suche nach Zwischen eta gefragt habe, die bisherigen Wesen Erweiterungen von Beta-Theorie des Lambda - Kalkül , die sich um einen orthogonalen Begriff der Erweiterung Frage geführt, unsichtbar Äquivalenzen Charakterisieren von konfluenten Rewrite - Regeln , die eine Klärung gesucht Antwort auf diese frühere Frage.

Charles Stewart
quelle

Antworten:

10

Wenn Sie für typisierte Kalküle die negativen Typen ( , × , ) berücksichtigen , können Sie die eta-Regeln grundsätzlich nach Belieben aktivieren oder deaktivieren, ohne die Konfluenz zu beeinträchtigen.1×

Bei positiven Typen (Summen und Paaren mit der Beseitigung der Musterübereinstimmung) ist die Situation viel unübersichtlicher. Grundsätzlich stellt sich die Frage, ob der Begriff eine geschlossene Eliminierungsform hat, die es ermöglicht, dass Kontexte auf komplizierte Weise mit Eta-Erweiterungen interagieren. Wenn zum Beispiel den Typ A × B hat , dann ist seine eta-Expansion l e teA×B . Um die Gleichungstheorie zu erhalten, die ein Kategorietheoretiker erwarten würde, müssen Sie die Kontexte C [ - ] betrachten und die Gleichung zu C [ e ] l e t verallgemeinernlet(a,b)=ein(a,b)C[] (mit den erwarteten Gültigkeitsbeschränkungen).C[e]let(a,b)=einC[(a,b)]

Ich denke, dass Sie immer noch ein Konfluenzergebnis nachweisen können, wenn Sie die Pendelkonvertierungen nicht zulassen. Aber das ist Hörensagen - ich habe es nie selbst ausprobiert oder mir Papiere angeschaut, die es dokumentieren.

Ich weiß allerdings nichts über untypisierte Lambda-Rechnung.

EDIT: Charles fragt nach Eta-Reduktionen. Dies ist vielversprechend für die Art von Beispiel, die er sucht, da sie meiner Meinung nach im Allgemeinen nicht stark genug sind, um die vollständige Gleichheitstheorie zu modellieren, die ich anhand eines einfachen Beispiels mit Booleschen veranschaulichen werde. Die eta-Expansion für Boolesche Werte ist . (Die Eta-Reduktion ist natürlich die andere Richtung.)C[e]if(e,C[true],C[false])

Betrachte nun den Term . Zeigen, dass dieser Ausdruck äquivalent ist zu i f ( e , fif(e,f,g)if(e,x,y) muss durch eine eta-Expansion gehen, weil wir die haben ersetzen e in einem der if-then-elses mit t r u eichf(e,fx,Gy)etrue und , um eine zum Antrieb β -Reduktion. falseβ

Neel Krishnaswami
quelle
Ich hätte klarstellen müssen, dass es sich um den untypisierten Lambda-Kalkül handelt: Die Logik, die beiseite gelegt wird, könnte dies unklar machen. Im typisierten Fall erwarte ich, dass die Post-Vollständigkeit für die 〈→, ×〉 -Theorie gilt, aber bei anderen Typen bin ich mir überhaupt nicht sicher. Kontexte interagieren auf komplizierte Weise mit ETA-Erweiterungen. Dies ist ein Grund, warum Sie die ETA-Reduzierung in Betracht ziehen sollten, nicht wahr?
Charles Stewart
4

Laut John C. Mitchell in Grundlagen der Programmiersprachen, sowohl in der STLC als auch in der nicht typisierten Lambda-Rechnung, pair (proj₁ P, proj₂ P) → Pbricht die Reduktionsregel die Konfluenz, wenn sie mit der fixReduktion kombiniert wird (oder, ich nehme an, wenn ich den Beweis betrachte), ohne solche Bedingungen für den nicht typisierten Fall. Dies ist der Satz 4.4.19 (Seite 289).

Blaisorblade
quelle
2
Ich denke, das ist ein ausführlicher Kommentar zu Neels Antwort. Klop & De Vrijer (1989) untersuchen die Theorie des untypisierten Lambda-Kalküls mit surjektiver Paarung: Der Fall mit eta-Reduktionen ist zwar nicht konfluent, aber die Theorie ist konsistent (sie hat ein Modell in der Scott-D_inf-Konstruktion) und liefert Ergebnisse Es kann eine konfluente konservative Rewrite-Theorie für surjektive Paare vorgeschlagen werden (immer noch ein offenes Problem, AFAIK).
Charles Stewart