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

Übungsblatt 6

zur Vorlesung Lambda-Kalkül und Typen im Sommer 2000 20. Juni 2000

1. Zeige: Hat r eine Normalform und gilt r →_{β} r′, so hat auch r′ eine Normalform.

(Zum Vergleich: Nach Definition von starker Normalisierung gilt: Ist r stark normalisierend und r →_{β} r′, so ist auch r′ stark normalisierend.)

2. Zeige für M := SN und N := cl({(λxx)t | t ∈ SN}), daß M →_{I} N ≠ M →_{E} N.

Hinweis: Studiere, wie Abstraktionen in den saturierten Abschluß hineingelangen können und wende dies auf die Identität an.

3. Zeige folgende Typisierungen im System universeller Typen:

(a) ⊢ ω : ∀β.∀αα → β.

(b) ⊢ ω : ∀β.∀αα → β → β.

(c) ⊢ ω : ∀αα → ∀αα.

4. Zeige, daß der Term \underline{2} \underline{2} K stark normalisierend ist, wobei \underline{2} := λfλx.f(fx) die zweite Church-Ziffer ist und K := λxλy.x.

Bemerkung: Man kann zeigen, daß \underline{2} \underline{2} K nicht typisierbar ist mithilfe universeller Typen.

Besprechung in der Übung am 26. Juni 2000.