Prof. Dr. Reinhold Letz Institut für Informatik Dr. Ralph Matthes der Universität München

Übungsblatt 2

zur Vorlesung Lambda-Kalkül und Typen im Sommer 2000 9. Mai 2000

In der Vorlesung wird die Konfluenz der β-Reduktion bewiesen. Wir benennen die Reduktionsrelation der Einfachheit halber mit → statt →_{β}. →^{∗} sei der transitive und reflexive Abschluß von →. Dann besagt Konfluenz die Existenz eines Terms t zu Termen r, r′ und r′′ mit r →^{∗} r′ und r →^{∗} r′′ so, daß r′ →^{∗} t und r′′ →^{∗} t. In Zeichen:

∀r∀r′∀r′′(r →^{∗} r′ ∧ r →^{∗} r′′ ⇒ ∃t.r′ →^{∗} t ∧ r′′ →^{∗} t).

In den folgenden Aufgaben darf die Konfluenz von → immer vorausgesetzt werden. Ziel ist es, den Nutzen der Konfluenzaussage zu erkennen.

1. Zeige, daß → die Church-Rosser-Eigenschaft hat, d.h., daß für alle Terme r und s aus r =_{β} s folgt: ∃t.r →^{∗} t ∧ s →^{∗} t.

2. Zeige λxλyx ≠_{β} λxλyy. (Also sind die Projektionen auf das erste und auf das zweite von zwei Argumenten tatsächlich verschieden im Sinne unserer Beta-Gleichheit. Natürlich nehmen wir dabei implizit an, daß x und y verschiedene Variablen bezeichnen.)

3. In Fortsetzung von Aufgabe 2 auf Blatt 1 zeige für alle Zahlen m, n ∈ ℕ

\underline{m} \underline{n} →^{∗} \underline{n^{m}},

falls m ≠ 0.

4. Ein einfaches Lemma besagt: ∀s∃r.sr =_{β} r. Die Beweisidee: Setze bei

gegebenem Term s

r := (λx.s(xx))(λx.s(xx))

für eine in s nicht frei vorkommende Variable x. Verifiziere, daß sr =_{β} r. (Also stellt r einen Fixpunkt von s dar, wenn s als Funktion interpretiert wird.) In Aufgabe 3 auf Blatt 1 haben wir einen Nachfolger auf Church-Ziffern gebraucht, also einen Term S mit ∀n ∈ ℕ.S\underline{n} =_{β} \underline{n + 1}. Dafür eignet sich S := λzλfλx.f(zfx). (Verifiziere das.) Nach obigem Lemma gibt es einen Term r mit Sr =_{β} r. Der Term r im obigen Beweis ist keine Church-Ziffer, also nicht von der Form \underline{n} mit einer natürlichen Zahl n. Zeige, (daß dies kein Zufall ist, sondern) daß es keine Church-Ziffer gibt, die Fixpunkt von S ist.

Besprechung in der Übung am 22. Mai 2000.