Lambda Nr. 6 SS17

Question

Comments

Ist das so richtig? bin ich bei der b) schon fertig?

Answer 1

Ich denke, dass beide Lösungen korrekt sind. Bei a) würde ich auch alles so machen, bei b) meine ich, geht das auch etwas kürzer:

(fun x y -> (fun x y -> a x y) y x)
= (fun x y -> (fun y -> a y y) x)
= (fun x y -> a x x)

Comments

Die erste Gleichheit gilt nicht, weil sich die Bindung von "y" ändert. Ein Beispiel mit konkreten Werten:

> let a = (+);;
val a : (int -> int -> int)

> (fun x y -> (fun x y -> a x y) y x) 1 2;;
val it : int = 3

> (fun x y -> (fun y -> a y y) x) 1 2;;
val it : int = 2

---

Oh natürlich! Da müsste man vorher umbenennen:

(fun x y -> (fun x y -> a x y) y x)
= (fun x y -> (fun x z -> a x z) y x)
= (fun x y -> (fun z -> a y z) x)
= (fun x y -> a y x)

Answer 2

Bei Teil a) ist das Ergebnis korrekt, die Zwischenschritte entsprechen aber nicht der formalen Definition aus der Vorlesung. In der vorletzten Zeile sollte auf der linken Seite zuerst die Definition auf (y x) angewendet werden und dann erst auf die einzelnen Variablen. Auf der rechten Seite in der vorletzten Zeile sagt die Definition, dass die Substitution gar nicht erst in den Lambda-Ausdruck hineingezogen wird, wenn der Parameter und die zu ersetzende Variable gleich sind.

In Teil b) haben Sie richtig erkannt, dass eine Umbenennung nötig ist. Allerdings hätte man hier y und nicht x umbenennen müssen. Beim Aufschreiben der Substitution würde ich noch Klammern setzen, damit klar ist auf welchen Teilausdruck die Substitution angewendet wird.