Programming Languages

Hausaufgabe 3

Geben Sie diese Hausaufgabe bis 21. Mai 2015 ab. Entweder bis 16:00 per Email an Yufei Cai
Alumni
Yufei Cai
(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.

Punkte

Sie können für die Aufgaben dieser Woche jeweils zwischen 0 und 3 Punkten bekommen. Insgesamt also zwischen 0 und 6 Punkten. Sie bekommen für die Aufgaben jeweils:

  • 1 Punkt, wenn Ihre Abgabe zeigt, daß Sie sich mit der Aufgabe ernsthaft beschäftigt haben.

  • 2 Punkte, wenn Sie die Aufgabe weitgehend korrekt gelöst haben.

  • 3 Punkte, wenn Sie die Aufgabe vollständig korrekt gelöst und Ihre Lösung gut verständlich dargestellt haben.

Die Punktevergabe für die weiteren Hausaufgaben im Semester wird ähnlich sein.

Aufgabe 5

Diese Aufgabe beziehtsich auf die Sprache mit Zahlen und Wahrheitswerten aus der Vorlesung. In der Vorlesung wurden Preservation und Progress dieser Sprache bewiesen. Gelten diese Eigenschaften weiterhin, wenn wir folgende Regeln hinzufügen?

0 : Bool

if t1 then t2 else t2 → t2

t → 0

t : Bool

Überlegen Sie für jede dieser Regeln einzeln:

  • Gilt Progress noch? Erweitern Sie den Beweis oder zeigen Sie ein Gegenbeispiel.

  • Gilt Preservation noch? Erweitern Sie den Beweis oder zeigen Sie ein Gegenbeispiel.

Aufgabe 6

In dieser Aufgabe geht es um die operationale Semantik (also die Relation →) des ungetypten λ-Kalküls aus der Vorlesung. Hier sind einige Terme dieser Sprache, dabei stehen die Meta-Variablen v1, v2, usw. für beliebige Values entsprechend der Grammatik für v aus der Vorlesung.

t1 = (λa . v2 a) v3
t2 = λa . v2 a v3
t3 = ((λd . d) v5) v6
t4 = v4 ((λ e . e) v6)
t5 = (λg . g g) v8
t6 = (λi . i i) v9
t7 = (λj . j j) (λ j . j j)

  • Welche dieser Terme können noch weiter reduziert werden? Geben Sie jeweils einen Term t′ an, so daß t → t′ gilt.