Geben Sie diese Hausauf­gabe bis 27. Juli 2015 ab. En­tweder bis 14:00 per Email an Till­mann Ren­del
AlumniTill­mann Ren­del (schreiben Sie “pl2” in den Be­tr­eff!) oder zu Be­ginn der Übung (!) auf Pa­pier.

Grup­pen

Sie können in Grup­pen von bis zu 3 Per­so­nen ar­beiten. Schreiben Sie in jedem Fall die Namen und Ma­trikel­num­mern aller Grup­pen­mit­glieder mit auf die Hausauf­gabe / in die Email. Wenn Sie in einer Gruppe ar­beiten, achten Sie da­rauf, daß alle Mit­glieder der Gruppe den Stoff ver­ste­hen. Nur dann sind die Hausauf­gaben eine gute Vor­bere­itung auf die Prüfung.

Auf­gabe 12

In dieser Auf­gabe geht es um para­metrische Poly­mor­phie.

Im ungetypten λ-Kalkül ter­miniert die Mul­ti­step-Re­duk­tion von (λx.x x) (λx.x x) nicht, aber im ein­fach getypten λ-Kalkül kann schon der Term λx.x x nicht typ­isiert wer­den (es gibt also kein τ so daß λx : τ . x x wohle­typt ist).

Be­tra­chten Sie nun fol­gende Vari­ante dieses Terms:

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

1. Ist dieser Term wohlgetypt in Sys­tem F?

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

Auf­gabe 13

In dieser Auf­gabe geht es um die Curry-Howard-Ko­r­re­spon­denz.

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

1. Be­weisen Sie (P ∧ Q) ⇒ (P ∨ Q).

2. Be­weisen Sie (P ∧ Q) ⇒ ¬(¬P ∨ ¬Q)

3. Be­weisen Sie (P ∨ Q) ⇒ ¬(¬P ∧ ¬Q)

Geben Sie jew­eils einen Term des der Formel entsprechen­den Typs an und skizzieren Sie auch den Ty­pableitungs­baum.