domanda idiota sul lambda calcolo

[jegger]

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.