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

Übungsblatt 5

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

Ziel dieses Blattes ist es, eine induktive Charakterisierung der Menge wn der schwach normalisierenden Terme zu bekommen, die analog^{1} zu der der stark normalisierenden Terme mittels SN ist. Dazu dient die Serie der Aufgaben, die keineswegs in der Reihenfolge bearbeitet werden müssen. Man muß eben nur notfalls eine der noch nicht eingesehenen vorherigen Aussagen als ”black box“ einsetzen. Zunächst definieren wir induktiv die Menge WN:

• Falls r⃗ ⊂ WN, dann xr⃗ ∈ WN.

• Falls r ∈ WN, dann λxr ∈ WN.

• Falls r[x := s]s⃗ ∈ WN, dann (λxr)ss⃗ ∈ WN.

Der Unterschied zur Definition von SN ist lediglich das Weglassen von ”s ∈ SN“ in der letzten Klausel.

1. Gib einen Term an, der in WN, nicht aber in SN ist und zeige ohne Verwendung des Normalisierungsresultats, daß dieser Term auch nicht mit Schnitt-Typen typisiert werden kann.

2. Definiere die Relation ⇝ zwischen Lambda-Termen induktiv (dabei ist die Vektornotation elementweise zu verstehen, was die gleiche Länge der beiden Vektoren implizit verlangt)

• r⃗ ⇝ r⃗′ ⇒ xr⃗ ⇝ xr⃗′

• r ⇝ r′ ∧ s⃗ ⇝ s⃗′ ⇒ (λxr)s⃗ ⇝ (λxr′)s⃗′

• r[x := s]s⃗ ⇝ t ⇒ (λxr)ss⃗ ⇝ t

⇝ ist reflexiv (3. Regel dafür unnötig).

Zeige Lemma 1: r ⇝ r′ ∧ s ⇝ s′ ⇒ rs ⇝ r′s′.

Tip: Induktion über die Ableitung von r ⇝ r′.

3. Zeige Lemma 2: →_{β}⊆⇝⊆→_{β}^{∗}.

Tip: Für jede Inklusion Induktion über die Erzeugung der als kleiner zu beweisenden Relation.

siehe zweite Seite 4. Zeige Lemma 3: r ⇝ r′ ∧ s ⇝ s′ ⇒ r[x := s] ⇝ r′[x := s′].

1In der Aussage analog, nicht aber im Beweis!

Tip: Induktion über die Ableitung von r ⇝ r′.

5. Zeige Lemma 4: r ⇝ r′ →_{β} r′′ ⇒ r ⇝ r′′.

Tip: Induktion über die Ableitung von r ⇝ r′ und Überlegung, auf welche Weise dann jeweils r′ →_{β} r′′ geschehen kann. Das ist die Hauptarbeit dieses Übungsblattes und braucht die Lemmata 1 und 3.

6. Zeige das Korollar: r →_{β}^{∗} r′ ⇒ r ⇝ r′.

Bemerkung: Damit haben wir →_{β}^{∗}=⇝, also ein neues Induktionsprinzip für →_{β}^{∗} gelernt, nämlich Induktion über die Erzeugung von ⇝. Bisher konnten wir ja nur über die Anzahl der Schritte in r →_{β}^{∗} r′ argumentieren.

7. Definiere nun ⇝^{−} durch Weglassen von s⃗ in der zweiten Klausel der Definition von ⇝, weshalb offenbar ⇝^{−}⊆⇝ gelten wird. Also sei ⇝^{−} definiert durch

• r⃗ ⇝^{−} r⃗′ ⇒ xr⃗ ⇝^{−} xr⃗′

• r ⇝^{−} r′ ⇒ λxr ⇝^{−} λxr′

• r[x := s]s⃗ ⇝^{−} t ⇒ (λxr)ss⃗ ⇝^{−} t

Zeige Lemma 5: r ⇝^{−} r′ ⇒ r ∈ WN ∧ r′ ∈ NF. Tip: Induktion über die Ableitung von r ⇝^{−} r′.

8. Zeige Lemma 6: r ∈ WN ⇒ ∃r′.r ⇝^{−} r′.

9. Zeige Lemma 7: r ⇝ r′ ∈ NF ⇒ r ⇝^{−} r′.

Tip: Induktion über ⇝. (Es gilt sogar, daß die Herleitung von r ⇝ r′ nur Regeln von ⇝^{−} benutzt, also keine Transformation nötig ist.)

10. Satz WN ist die Menge wn der Terme, die eine Normalform besitzen, also derjenigen Terme r, zu denen es ein r′ ∈ NF gibt mit r →_{β}^{∗} r′.

Beweis: ”WN ⊆ wn“ Nach L. 6 gilt r ⇝^{−} r′ für ein r′. Nach L. 5 ist r′ ∈ NF. Wegen ⇝^{−}⊆→_{β}^{∗} folgt r ∈ wn. ”wn ⊆ WN“ Gelte r →_{β}^{∗} r′ ∈ NF. Mit dem Korollar folgt r ⇝ r′ ∈ NF. L. 7 ergibt r ⇝^{−} r′ und schließlich L. 5 r ∈ WN. Aufgabe: Welche der beiden Teilaussagen braucht den vorgestellten trickreichen Ansatz?

Nun noch etwas mit Schnitt-Typen: Seien ι und κ zwei verschiedene Grundtypen. Zeige, daß es keinen Term r geben kann mit

⊢ r : ((ι → κ) → ι) → ι,

wobei ⊢ aus dem System mit den Schnitt-Typen genommen werde. Bemerkung: Es ist sehr ratsam, den Normalisierungssatz zu verwenden.

Besprechung in der Übung am 19. Juni 2000.