Programming Languages

Hausaufgabe 5

Geben Sie diese Hausaufgabe bis 25. Junii 2015 ab. Entweder bis 16:00 per Email an Tillmann Rendel
AlumniTillmann Rendel (schreiben Sie “pl2” in den Betreff!) oder zu Beginn der Vorlesung 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 10

In dieser Übung geht es um die Verwendung der Subtyping-Relation aus der Vorlesung. Betrachten Sie diese Terme:

move = λ p : {x : Nat, y : Nat} . {x = succ (p.x), y = succ (p.y)}

applyToOrigin = λ f : {x : Nat, y: Nat, z : Nat} → {x : Nat} . (f {x = 0, y = 0, z = 0}).x

  1. Ist der Term (move {x = 1, y = 2}) wohlgetypt?

  2. Ist der Term (move {x = 1, y = 2, z = 3}) wohlgetypt?

  3. Ist der Term (move {x = 1, y = 2, z = 3}.z wohlgetypt?

  4. Ist der Term (applyToOrigin move) wohlgetypt?

Skizzieren Sie jeweils einen Ableitungsbaum an oder erklären Sie, wieso es keinen Ableitungsbaum geben kann.

Aufgabe 11

In dieser Aufgabe geht es um die Struktur der Subtyping-Relation aus der Vorlesung.

  1. Wie viele verschiedene Supertypen hat der Typ {a : Top, b : Top}? Geben Sie die Supertypen an.

  2. Gibt es einen Typ mit unendlich vielen Subtypen?

  3. Gibt es einen Typ mit einer unendlichen Kette von Subtypen (also … <: T2 <: T1)?

  4. Gibt es einen Typ mit unendlich vielen Supertypen?

  5. Gibt es einen Typ mit einer unendlichen Kette von Supertypen (also T1 <: T2 <: …)?

Geben Sie bei Teilaufgabe 2 bis 5 jeweils den Typ an und wie die Kette aussieht, oder argumentieren Sie, wieso kein solcher Typ existiert.