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

Übungsblatt 4

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

Wir beschäftigen uns auf diesem Blatt nur mit einfachen Typen!

1. Sei ρ ein beliebiger Typ. Zeige, daß die n-te Church-Ziffer

\underline{n} = λfλx. \underbrace{f(… (f}_{n-mal} x) …)

im leeren Kontext den Typ (ρ → ρ) → ρ → ρ erhält, i. Z.

∅ ⊢ \underline{n} : (ρ → ρ) → ρ → ρ.

Untersuche, welche Typen \underline{m} ∘ \underline{n} = λx.\underline{m}(\underline{n}x) und \underline{m} \underline{n} im leeren Kontext haben können, wenn \underline{m} und \underline{n} die m-te bzw. die n-te Church-Ziffer sind.

2. Zeige, daß jeder geschlossene (d. h. ohne freie Variablen) Term in NF (der induktiven Charakterisierung der Normalformen), der im leeren Kontext den Typ (ι → ι) → ι → ι (ι gemäß Vereinbarung ein Grundtyp) erhält, eine Church-Ziffer oder gleich λff ist. (Was unterscheidet \underline{1} von λff?)

3. Zeige, daß für typisierbare Terme in Normalform rekonstruierbar ist, welcher Typ ρ jeweils in der Anwendung der Abstraktionsregel benutzt wurde, d. h. in der Regel Γ, x : ρ ⊢ r : σ ⇒ Γ ⊢ λxr : ρ → σ. Zeige anhand eines Beispiels, daß dies nicht für beliebige Terme gilt.

4. (Nun noch eine Aufgabe ohne Typen:) Sei sn(k) die Menge der Terme, für die alle Beta-Reduktionsfolgen höchstens die Länge k haben. Wir zählen dabei so, daß sn(0) gerade die Menge der Normalformen ist. Zeige nun, daß SN ⊆ ⋃_{k∈ℕ} sn(k). Dies soll konstruktiv geschehen. Natürlich mittels Induktion, aber wie folgt: Gib Funktionen f_{n} mit n Stellen für n ∈ ℕ sowie eine einstellige Funktion g und eine zweistellige Funktion h an so, daß gilt:

• Falls r_{i} ∈ sn(k_{i}) für i ∈ {1, …, n}, so xr⃗ ∈ sn(f_{n}(k_{1}, …, k_{n})).

• Falls r ∈ sn(k), so λxr ∈ sn(g(k)).

• Falls r[x := s]s⃗ ∈ sn(k) und s ∈ sn(ℓ), so (λxr)ss⃗ ∈ sn(h(k, ℓ)).

Dies ist der Weg, um die Induktion über sn durch Induktion über Zahlen zu ersetzen und so die Argumentation mittels unendlicher Reduktionsfolgen zu vermeiden.

Besprechung in der Übung am 5. Juni 2000.