Lambda-Kalkül, normale Ordnung, Normalform,

Question

In Lambda-Kalkül, wenn ein Begriff normale Form hat, wird normale Ordnungsreduktions-Strategie immer es produzieren.

Ich frage mich nur, wie man den obigen Vorschlag strikt zu beweisen?

Answer 1

Das Ergebnis, das Sie erwähnen, ist eine logische Folge des so genannten Standardisierungssatzes, der besagt, dass für jede Reduktionsfolge M-> N eine andere "Standard" zwischen den gleichen Termen M und N existiert, in der Sie Redexe ganz links ausführen Auftrag. Der Beweis ist nicht so trivial, und es gibt verschiedene Ansätze in der Literatur. Ich füge unten eine kurze Bibliographie hinzu.

Der jüngste Beweis von Kashima 5 (siehe auch 1) hat den Vorteil, dass er nicht den Restbegriff verwendet und auf rein induktiven Techniken basiert. Es ist auch gut für Formalisierung 2, aber wenn Sie nicht bereits mit dem Thema vertraut sind, ist es nicht besonders aufschlussreich.

Die allgemeine Idee hinter der Standardisierung ist die folgende. Angenommen, zwei Redexe uber R und S zu haben, wobei S in Bezug auf R in ganz links äußersten Position ist, und betrachten die folgende Ermäßigung:

   R  S 
      M -> P -> N 

Dann können Sie Brennen S beginnen, statt, aber auf diese Weise Sie kann den Redex R möglicherweise duplizieren (oder löschen). Diese Re-Indizes, die im Wesentlichen die Reste von R nach dem Abfeuern von S sind, werden als Reste bezeichnet und werden üblicherweise als R/S angezeigt (gelesen: Reste von R nach S). So ist der Grund Lemma, dass

   R S = S (R/S) 

Um es zu benutzen, für die Standardisierung, müssen wir R auf eine beliebige Sequenz ρ verallgemeinern (dass wir ohne redex in ganz links äußerster Position WRT können davon ausgehen, Standard zu sein, S). Es ist immer noch wahr, dass

  (*) ρS = S (ρ/S) 

aber was nicht so offensichtlich ist die Standardisierung von (ρ/S) ist. Zu diesem Zweck, lassen Sie uns beobachten, dass ρ durchgeführt wurde vor dem Brennen S = C [\ xM N], dass teilt im Wesentlichen den Begriff in drei getrennten Regionen: der Kontext C, M, und N. Dies induziert eine Neuverteilung von ρ in drei aufeinander folgenden Sequenzen:

  ρ1 inside M 
      ρ2 inside N 
      ρ3 inside C 

(denken Sie daran, dass kein redex in äußerst linken äußersten Position WRT S war). Der einzige Teil, der dupliziert (oder gelöscht) werden kann, ist ρ2, und die Residuen ρ2-0 ... ρ2-k sind leicht nach den verschiedenen Positionen von der k Kopien von N geordnet, die durch das Brennen von S erzeugt wurden. So

S ρ1 ρ2-0 ... ρ2-k ρ_3 

ist die Standardversion von (*).

Grundlegende Bibliographie.

1 A.Asperti, JJ. Erheben. The cost of usage in the lambda-calculus. LICS 2013.

3 H. P. Barendregt. Der Lambda-Kalkül, Nord-Holland (1984).

4 G.Gonthier, JJ. Levy, PA. Mellies. An abstract standardisation theorem. LICS '92.

2 F.Guidi. Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. Journal of Formalisierte Begründung 5 (1): 1-25, 2012.

5 R.Kashima. A proof of the standardization theorem in lambda-calculus. Technischer Bericht C-145 ,, Tokyo Institut für Technologie, 2000.

[6] JW. Klop. Kombinatorische Reduktionssysteme. Doktorarbeit, CWI, Amsterdam, 1980.

[7] G.Mitschke. Der Standardsatz für die Lambda-Kalkül. Z. Math.Logik. Grundlag. Math., 25: 29-31, 1979

[8] M.Takahashi. Parallele Reduktion des Lambda-Kalküls. Information and Computation 118, S. 120-127, 1995.

[9] H. Xi, Upper bounds for standardizations and an application. Journal of Symboloc Logic 64, pp.291-303, 1999.