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

Übungsblatt 3

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

1. Wir wollen schwache Normalisierung des einfach getypten Lambda-Kalküls auf eine besonders einfache Weise einsehen. Alle Terme seien also einfach getypt. Das bedeute, wir lassen die Typisierungsherleitungen implizit und verwenden gleich eine induktive Definition der einfach getypten Terme:

• Ist x eine Variable und ρ ein Typ, so ist x^{ρ} ein Term vom Typ ρ.

• Ist x eine Variable, ρ ein Typ und r ein Term vom Typ σ, so ist λx^{ρ}r ein Term vom Typ ρ → σ.

• Ist r ein Term vom Typ ρ → σ und s ein Term vom Typ ρ, so ist rs ein Term vom Typ σ.

Die Tatsache, daß r ein Term vom Typ ρ ist, wird durch r : ρ oder r^{ρ} ausgedrückt, also z. B. λf^{ρ→ρ}λx^{ρ}.f(f(fx)) : (ρ → ρ) → ρ → ρ. Dabei werden die Typen der gebundenen Variablen nicht extra angeschrieben, wenn nur eine Lesart möglich ist, was z. B. in λx^{ρ}λx^{σ}.x nicht der Fall ist. (Man vermeide solche Terme in expliziten Darstellungen!)

(a) Wir benutzen die Menge NF von Termen, induktiv definiert durch • r⃗ ⊆ NF ⇒ xr⃗ ∈ NF

• r ∈ NF ⇒ λxr ∈ NF Zeige, daß NF genau aus den β-normalen Termen besteht, d. h., aus den Termen r, zu denen es kein s gibt mit r →_{β} s.

(b) Definiere r ↓ :⇔ ∃t ∈ NF.r →_{β}^{∗} t. r ↓ bedeutet also, daß r eine Normalform hat. Zeige: Wenn r ∈ NF und s^{ρ} ∈ NF, dann gilt (i) rs ↓, falls rs ein einfach getypter Term ist, und (ii) r[x^{ρ} := s] ↓. Tip: Der Beweis kann durch Hauptinduktion über ρ und Nebeninduktion über r ∈ NF geführt werden. Wer es etwas schwerer haben will, zeigt nur (ii) alleine und benutzt noch r^{ρ→σ} ∈ NF ⇒ rx^{ρ} ↓.

(c) Zeige nun, daß für alle einfach getypten Terme r gilt r ↓.

2. Zeige, daß für eine stark normalisierende binäre Relation → aus der lokalen Konfluenz die Konfluenz folgt. Hinweis: Durch Induktion über die starke Normalisierbarkeit von r zeige, daß jedes von r ausgehende Konfluenzdiagramm zu schließen ist.

Besprechung in der Übung am 29. Mai 2000.