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

Übungsblatt 7

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

1. Sei ρ beliebiger Typ mit α ∉ FV(ρ). Setze

τ := 1 + (((α → ρ) → α) → α) → α.

Zeige, daß es in System F einen Term m gibt mit

⊢ m : ∀α∀β.(α → β) → τ → τ[α := β].

Konstruiere damit einen geschlossenen Bewohner von ματ, d. h. einen Term r mit ⊢ r : ματ. (Dabei sei ματ := ∀α.(τ → α) → α gemäß Vorlesung von heute. 1 := ∀α.α → α und ρ + σ := ∀α.(ρ → α) → (σ → α) → α wurden am 20. Juni eingeführt.) Hinweis: Ohne die Typannotationen der abstrahierten Variablen ist eine Lösung für m gegeben durch:

ΛαΛβλfλxΛγλzλz_{1}.xγz(λz_{2}.z_{1}(λz_{3}.z_{3}(λz_{4}.f(z_{2}(λz_{5}.z_{5}(λz_{6}.z_{4}(fz_{6}))))))).

2. Zeige, daß es keinen Term r in System F gibt mit ⊢ r : 0. (0 := ∀αα.) Hinweis: Studiere das Aussehen von Normalformen und benutze den (in der Vorlesung nicht bewiesenen, aber im Skriptum ausgeführten) Normalisierungssatz.

3. (Schwierige Aufgabe) Setze cont(ρ) := μα.1 + (α → ρ) → ρ für ein α ∉ FV(ρ), finde einen Term m, der die Monotonie von 1 + (α → ρ) → ρ in α ausdrückt, und setze D := C_{cont(ρ)}m(INL_{1,(cont(ρ)→ρ)→ρ}IN1) und Cf := C_{cont(ρ)}m(INR_{1,(cont(ρ)→ρ)→ρ}f). (Die Definition von C_{cont(ρ)}mt ist Instanz der Definition von C_{μαρ}mt in der heutigen Vorlesung.) Zeige, daß ⊢ D : cont(ρ), und aus Γ ⊢ f : (cont(ρ) → ρ) → ρ folgt Γ ⊢ Cf : cont(ρ). Gib einen Term e an mit ⊢ e : cont(nat) → nat und eD →_{βη}^{∗} 0 und e(Cf) →_{βη}^{∗} fe für alle Terme f (mit nat und 0 aus der Vorlesung). (Bemerkung: Dies ist Iteration über einem nicht-strikt positiven induktiven Datentypen. Da jeweils →_{βη}^{∗} durch →_{βη}^{+}—den transitiven Abschluß von →_{βη}—ersetzt werden könnte, ist also auch eine solche Iteration von vorneherein stark normalisierend, weil System F es ist.)

Besprechung in der Übung am 3. Juli 2000.