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.
Delta-Reduktionen bei applikativer Reduktion
Hi, ich hätte eine Frage zum Umgang mit delta-Reduktionen bei applikativer Reduktion.
Wenn z.B. pair so definiert ist:
pair a b = λ select. select a b
und ich einen Term t habe mit
t = pair x y
Dann kann ich t doch in einer einzelnen Delta-Reduktion auf
λ select . select x y
reduzieren, oder? Zumindest verstehe ich so die Erklärungen zu Delta-Reduktionen auf Blatt 4, Übung 2.2.
Wenn ich nun einen Term habe wie
pair (pair x y) z
und diesen applikativ reduzieren möchte, muss ich dann zuerst das innere oder das äußere pair auflösen?
Und wäre es anders, wenn pair so definiert wäre?
pair = λ a b select . select a b
Vielen Dank schonmal 
1 „Gefällt mir“
Hi,
pair (pair x y) z = (pair (pair x y)) zMan kann also einfach ganz normal den Regeln für applikative Reduktion folgen. Da (pair (pair x y)) nicht normal ist, muss man also zuerst in diesen Teilterm absteigen mit der Reduktion.
In der Tat wäre es also anders, wenn pair ohne Parameter definiert wäre. Denn dann ist zwar (pair (pair x y)) immer noch keine Normalform, aber ‘pair’ selbst nicht mehr, weshalb dann das äußerste ‘pair’ zuerst reduziert wird.