Variável Livre de Cálculo Lambda

5

Aqui está algo da "Sintaxe e semântica de linguagens de programação" de 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.

Eu assumo que a variável livre é y logo após o λx. e os y's encadernados são os yyy que eu posso entender intuitivamente. Então ((λx.yλy.yx) a) b) reduziria para (yλy.ya) b) depois para bba? Alguém pode explicar como isso aconteceu? No final, é a expressão b duas vezes. Alguém pode, talvez, fornecer mais exemplos de variáveis vinculadas e livres?

    
por user2054900 02.03.2013 / 15:55
fonte

1 resposta

3

Você identificou corretamente o primeiro y como a variável livre. Basicamente, as abstrações lambda definem um escopo para suas variáveis vinculadas. O escopo substitui quaisquer outros usos dos mesmos nomes de variáveis, portanto, o mesmo nome de variável pode ser usado várias vezes em diferentes abstrações ou como variável livre.

(y (λy.ya)) b não pode ser mais reduzido. Variáveis não ligadas nunca serão substituídas em uma redução beta.

Se fosse (y (λy.ya) b) você poderia reduzir para y (ba).

    
por 02.03.2013 / 16:15
fonte

Tags