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

Übungsblatt 8

zur Vorlesung Lambda-Kalkül und Typen im Sommer 2000 21. Juli 2000

1. Wir betrachten eine einfache Erweiterung von System F, die nicht normalisierend ist.

Wir setzen σ := ∀α∀β.(α → α) → β → β. Wir nehmen eine Konstante J vom Typ σ in unser System auf, d. h., wir zeichnen eine Variable aus, benennen sie mit J, abstrahieren nie über J und meinen mit Γ ⊢ r : ρ nunmehr Γ, J : σ ⊢ r : ρ. Die Relation →_{βη} wird um einen weiteren Anfangsfall angereichert, nämlich Jρρr →_{βη} r. Dann gilt:

Γ ⊢ Jρρr : τ ⇔ τ = ρ → ρ ∧ Γ ⊢ r : τ,

mithin Typerhaltung unter Reduktion (Subject Reduction). Beachte, daß die Regel Jρρr →_{βη} r lediglich einen Abstieg zu einem Teilterm bewirkt. Da aber →_{βη} unter allen Termbildungsregeln abgeschlossen ist, läßt sich eine in dieser Erweiterung typisierbare Variante von ωω = (λx.xx)(λx.xx) finden, die wie ωω eine Reduktion in mehreren Schritten zu sich selbst erlaubt. Gib eine solche an.

Tip: Der Typ 1 := ∀α.α → α ist wesentliches Hilfsmittel, da ⊢ λx^{1}.x1x : 1 → 1 bereits in System F gilt.

2. Setze tree(ρ) := μα.1 + (ρ → α) für ein α ∉ FV(ρ). Dann setze τ := tree(α) → α. Zeige, daß es in System F einen Term m gibt mit

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

Konstruiere damit einen geschlossenen Bewohner von μα.1 + τ.

3. (zeitraubende Aufgabe) Zeige, daß die Funktion breadth aus dem Beispiel der Vorlesung (der Programmcode ist auf der WWW-Seite zu finden) in System F berechnet werden kann, wobei die Funktion apply als Konstante vom Typ cont → (cont → list) → list (siehe oben, wie das gemeint ist) anzunehmen ist. Dafür setze nat := μα.1 + α, list := μα.1 + nat × α und btree := μα.nat + (nat × (α × α)).

Hinweis: Die Mühsal besteht in der Bereitstellung all der Konstruktoren, was wiederum Monotoniezeugen verlangt.

Besprechung in der Übung am 24. Juli 2000.