jegger
02-09-2008, 17:40
Ciao a tutti, sto iniziando a studiare il lambda calcolo ma non riesco a capire bene come funziona la beta-riduzione con strategia call-by-value.
Da quanto ho capito, Call-by-value dice che bisogna prima ridurre con beta-riduzione la parte + esterna del termine se però la parte destra è un valore. Quindi con un esempio small step di questo tipo cosa dovrei ottenere?
(lambda t.lambda f.t) (lambda t. lambda f.f) (lambda x.x)
in teoria con l'associatività a sinistra x le applicazioni dovrei avere una cosa di questo tipo:
((lambda t.lambda f.t) (lambda t. lambda f.f)) (lambda x.x)
x cui essendo (lambda x.x) la parte + esterna già in forma di valore, dovrei andare a sostituire le occorrenze di t con lambda x.x ottenendo:
(lambda f. (lambda x.x)) (lambda f.f)
è giusto? son molto dubbioso.
Da quanto ho capito, Call-by-value dice che bisogna prima ridurre con beta-riduzione la parte + esterna del termine se però la parte destra è un valore. Quindi con un esempio small step di questo tipo cosa dovrei ottenere?
(lambda t.lambda f.t) (lambda t. lambda f.f) (lambda x.x)
in teoria con l'associatività a sinistra x le applicazioni dovrei avere una cosa di questo tipo:
((lambda t.lambda f.t) (lambda t. lambda f.f)) (lambda x.x)
x cui essendo (lambda x.x) la parte + esterna già in forma di valore, dovrei andare a sostituire le occorrenze di t con lambda x.x ottenendo:
(lambda f. (lambda x.x)) (lambda f.f)
è giusto? son molto dubbioso.