Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Church-Codierung (Blatt 5 - 5)
Eine Frage zu den Auswertungsstrategien.
Darf man bei der Aufgabe z.b.
twice f = lambda x. f(fx)
zu
twice = lambda f x. f(fx)
umformen?
Anfang der Aufgabe…
twice fst (…
Konkret läuft das für mich in das Problem, ob ich nicht weiß, ob ich, wenn ich twice delta-reduziere, gleichzeitig fst einsetzen muss oder es auch wie oben umformen darf?
Nur um die Begrifflichkeiten zu klären: grundsätzlich werden hier Umformungen von Lambda-Ausdrücken betrachtet. D.h. ein Lambda-Ausdruck wird in einen anderen umgeformt. Die Zeile
jedoch ist kein Lambda-Ausdruck, sondern eine Gleichung von Lambda-Ausdrücken (Rechts ein Lambda-Ausdruck, Links ein Lambda-Ausdruck, und dazwischen ist ein Gleichheitszeichen).
Die δ-Reduktion setzt gleichzeitig das fst für f ein.
Edit: Oder anders gesagt: die zwei von dir angegebenen Gleichungen haben unterschiedliche δ-Reduktions-Schritte.