Normalisierungseigenschaft (abstrakte Umschreibung) - Normalization property (abstract rewriting)

In der mathematischen Logik und der theoretischen Informatik hat ein Rewrite-System die ( starke ) Normalisierungseigenschaft oder terminiert, wenn jeder Term stark normalisiert ; das heißt, wenn jede Folge von Rewrites schließlich mit einem irreduziblen Term endet , der auch Normalform genannt wird . Ein Rewrite-System kann auch die schwache Normalisierungseigenschaft haben , was bedeutet, dass für jeden Term mindestens eine bestimmte Folge von Rewrites existiert, die schließlich eine Normalform, dh einen irreduziblen Term, ergibt.

Lambda-Kalkül

Nicht typisierte Lambda-Rechnung

Der reine untypisierte Lambda-Kalkül erfüllt nicht die starke Normalisierungseigenschaft und nicht einmal die schwache Normalisierungseigenschaft. Betrachten Sie den Begriff . Es hat die folgende Umschreibungsregel: Für jeden Begriff , ${\displaystyle \lambda x.xxx}$${\displaystyle t}$

${\displaystyle (\mathbf {\lambda} x.xxx)t\rightarrow ttt}$

Aber bedenken Sie, was passiert, wenn wir auf sich selbst anwenden : ${\displaystyle \lambda x.xxx}$

${\displaystyle {\begin{ausgerichtet}(\mathbf {\lambda} x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda} x.xxx)(\lambda x.xxx)(\ lambda x.xxx)\\&\rightarrow (\mathbf {\lambda} x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \ldots\,\end{ausgerichtet }}}$

Daher ist der Begriff weder stark noch schwach normalisierend. ${\displaystyle (\lambda x.xxx)(\lambda x.xxx)}$

Typisierter Lambda-Kalkül

Verschiedene Systeme von typisierten Lambda - Kalkül einschließlich das einfach typisierten Lambda - Kalkül , Jean-Yves Girard ‚s System F , und Thierry Coquand ‘ s Kalkül der Konstruktionen sind stark Normalisieren.

Ein Lambda-Kalkülsystem mit der Eigenschaft Normalisierung kann als Programmiersprache mit der Eigenschaft angesehen werden, dass jedes Programm beendet wird . Obwohl dies eine sehr nützliche Eigenschaft ist, hat sie einen Nachteil: Eine Programmiersprache mit der Eigenschaft normalization kann nicht Turing complete sein , sonst könnte man das Halteproblem lösen, indem man sieht, ob das Programm den Typ überprüft. Das bedeutet, dass es berechenbare Funktionen gibt, die im einfach typisierten Lambda-Kalkül nicht definiert werden können (und ebenso gibt es berechenbare Funktionen, die nicht im Kalkül der Konstruktionen oder System F berechnet werden können ).

Selbstinterpretation im typisierten Lambda-Kalkül

Beispielsweise ist es unmöglich, in einem der oben genannten Kalküle einen Selbstinterpretierer zu definieren .

Hier meinen wir mit "Selbstinterpreter" ein Programm, das eine Quellbegriffsdarstellung in einem einfachen Format (wie einer Zeichenkette) annimmt und eine Darstellung des entsprechenden normalisierten Begriffs zurückgibt. Dieses Unmöglichkeitsergebnis gilt nicht für andere Definitionen von "Selbstausleger". Zum Beispiel haben einige Autoren Funktionen des Typs als Selbstinterpreter bezeichnet, wobei der Typ der Darstellung von -typisierten Begriffen ist. Um Verwechslungen zu vermeiden, bezeichnen wir diese Funktionen als Selbsterkenner . Brown und Palsberg zeigten, dass Selbsterkenner in mehreren stark normalisierenden Sprachen definiert werden können, darunter System F und System F _ω . Dies erwies sich als möglich , weil die Typen der codierten Terme , die sich in den Typen ihrer Darstellungen widerspiegeln , die Konstruktion eines diagonalen Arguments verhindert . In ihrem Papier behaupten Brown und Palsberg, die "konventionelle Weisheit" zu widerlegen, dass Selbstinterpretation unmöglich ist (und sie bezeichnen genau diese Wikipedia-Seite als Beispiel für die konventionelle Weisheit), aber was sie tatsächlich widerlegen, ist die Unmöglichkeit der Selbstinterpretation. Erkenner, ein ganz anderes Konzept. In ihrer Folgearbeit wechseln sie zu der hier verwendeten spezifischeren Terminologie "Selbsterkenner" und unterscheiden diese insbesondere von "Selbstevaluatoren" vom Typ . Sie erkennen auch, dass die Umsetzung der Selbstevaluation schwieriger erscheint als die der Selbstanerkennung, und lassen die Umsetzung der ersteren in einer stark normalisierenden Sprache als offenes Problem. ${\displaystyle \pi\,\tau\to\tau}$${\displaystyle \pi\,\tau}$${\displaystyle \tau}$${\displaystyle \pi\,\tau\to \pi\,\tau}$

Siehe auch

• Typisierter Lambda-Kalkül
• Umschreiben
• Vollständige funktionale Programmierung
• Barendregt–Geuvers–Klop-Vermutung
• Newmans Lemma
• Normalisierung durch Auswertung

Anmerkungen

Verweise

• Baader, Franz ; Nipkow, Tobias (1999). Begriff umschreiben und so . Cambridge University Press. ISBN 0-521-77920-0. 316 Seiten.