Lambda Calculus Free Variable

Question

Lambda Calculus Free Variable

#1 da (3 voti)

5

Ecco qualcosa della "Sintassi e semantica dei linguaggi di programmazione" di Slonneger:

A variable may occur both bound and free in the same lambda expression: for example, in λx.yλy.yx the first occurrence of y is free and the other two are bound.

Suppongo che la variabile libera sia y subito dopo λx. e le y vincolate sono le λy.y che posso in qualche modo comprendere intuitivamente. Quindi ((λx.yλy.yx) a) b) ridurrebbe a (yλy.ya) b) quindi a bba? Qualcuno può spiegare come è stato? Alla fine è l'espressione b due volte. Qualcuno può forse fornire più esempi di variabili vincolate e libere?

lambda

posta user2054900 02.03.2013 - 15:55

fonte

1 risposta

Leggi altre domande sui tag lambda

Implementazione e riflessione fluide dell'interfaccia. Argomento di studio NoSQL e BIG DATA

score 3 · Answer 1

Hai identificato correttamente il primo y come variabile libera. Fondamentalmente le astrazioni lambda definiscono uno scope per le loro variabili associate. Lo scope sovrascrive qualsiasi altro uso degli stessi nomi di variabili, quindi lo stesso nome di variabile può essere usato più volte in diverse astrazioni o come variabile libera.

(y (λy.ya)) b non può essere ulteriormente ridotto. Le variabili non associate non saranno mai sostituite in una riduzione beta.

Se fosse (y (λy.ya) b) potresti ridurre a y (ba).