Not logged in. · Lost password · Register

uv35imat
Member since Dec 2016
5 posts
Subject: Delta-Reduktionen bei applikativer Reduktion
+1 honolulu
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 :-)
quaestor
Christoph Rauch, INF8
Avatar
Member since Sep 2007
98 posts
Hi,

pair (pair x y) z = (pair (pair x y)) z

Man 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.
Metal is like an apple, no one likes the core.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen