Geben Sie diese Hausaufgabe bis 27. Juli 2015 ab. Entweder bis 14:00 per Email an Tillmann Rendel
AlumniTillmann Rendel (schreiben Sie “pl2” in den Betreff!) oder zu Beginn der Übung (!) auf Papier.

Gruppen

Sie können in Gruppen von bis zu 3 Personen arbeiten. Schreiben Sie in jedem Fall die Namen und Matrikelnummern aller Gruppenmitglieder mit auf die Hausaufgabe / in die Email. Wenn Sie in einer Gruppe arbeiten, achten Sie darauf, daß alle Mitglieder der Gruppe den Stoff verstehen. Nur dann sind die Hausaufgaben eine gute Vorbereitung auf die Prüfung.

Aufgabe 12

In dieser Aufgabe geht es um parametrische Polymorphie.

Im ungetypten λ-Kalkül terminiert die Multistep-Reduktion von (λx.x x) (λx.x x) nicht, aber im einfach getypten λ-Kalkül kann schon der Term λx.x x nicht typisiert werden (es gibt also kein τ so daß λx : τ . x x wohletypt ist).

Betrachten Sie nun folgende Variante dieses Terms:

λx : ∀X.X → X . x [∀X. X → X] x

1. Ist dieser Term wohlgetypt in System F?

2. Kann man mit Hilfe dieses Terms eine wohlgetypte Variante von (λx.x x)(λx.x x) schreiben?

Aufgabe 13

In dieser Aufgabe geht es um die Curry-Howard-Korrespondenz.

Beachten Sie, daß die Negation ¬A aus der Logik dem Typ ∀X. A → X entspricht.

1. Beweisen Sie (P ∧ Q) ⇒ (P ∨ Q).

2. Beweisen Sie (P ∧ Q) ⇒ ¬(¬P ∨ ¬Q)

3. Beweisen Sie (P ∨ Q) ⇒ ¬(¬P ∧ ¬Q)

Geben Sie jeweils einen Term des der Formel entsprechenden Typs an und skizzieren Sie auch den Typableitungsbaum.