Variáveis livres e ligadas no Cálculo Lambda

---

No cálculo lambda, as variáveis são os blocos básicos que usamos para construir expressões e funções.

Mas nem todas as variáveis têm o mesmo “status”. Algumas estão “amarradas” a uma definição específica, enquanto outras “flutuam” livremente, sem uma ligação clara.

Esses conceitos (variáveis ligadas e variáveis livres) são fundamentais para entender como as expressões funcionam e como as substituições ocorrem.

Definição

No cálculo lambda, as variáveis podem ser classificadas em dois tipos com base em sua relação com o símbolo $\lambda$:

• Variável ligada: Uma variável $x$ é considerada ligada se todas as suas ocorrências no corpo de uma expressão são precedidas por um $\lambda x$, que a define como um parâmetro. O $\lambda$ (função) “liga” a variável ao seu escopo.
• Variável livre: Uma variável é livre se ela aparece em uma expressão sem estar associada a um $\lambda$ que a preceda diretamente na mesma sub-expressão.

Formalmente:

• Em $\lambda x.e$, todas as ocorrências de $x$ no corpo $e$ são ligadas por $\lambda x$.
• Qualquer variável em $e$ que não seja precedida por um $\lambda$ correspondente é livre.

Todos os nomes no cálculo lambda são locais às suas definições, ou seja, o escopo de uma variável ligada é restrito à expressão onde ela é definida pelo $\lambda$.

O Papel do $\lambda$ como “ligador”

O símbolo $\lambda$ atua como um marcador que “captura” uma variável e define seu escopo. Quando escrevemos $\lambda x.e$, estamos dizendo que $x$ é um parâmetro da função, e qualquer $x$ que apareça em $e$ está vinculado a esse $\lambda$.

Isso é semelhante a como parâmetros funcionam em linguagens de programação: o escopo da variável é limitado à função onde ela é declarada.

Variáveis livres e o contexto externo

Uma variável livre, por outro lado, não tem um $\lambda$ que a “prenda” dentro da expressão em que aparece. Ela depende de um contexto externo para ter significado.

Escopo e Sub-expressões

Em expressões maiores, o mesmo nome pode aparecer em diferentes contextos. Cada $\lambda$ cria um novo escopo, e uma variável só é ligada ao $\lambda$ mais próximo que a define.

Exemplos

Exemplo 1: Variável ligada e livre em uma expressão simples

Considere a expressão:

$$\lambda x.(xy)$$

Aqui, $x$ é ligado porque aparece no corpo da função e é precedido por $\lambda x$.

Já $y$ é livre, pois não há um $\lambda y$ que o defina nesta expressão. O valor de $y$ dependeria de um contexto externo.

Exemplo 2: Múltiplos escopos

Agora, analise esta expressão mais complexa:

$$(\lambda x.x)(\lambda y.(yx))$$

Na sub-expressão $\lambda x.x$:

• $x$ é ligado pelo primeiro $\lambda x$.

Na sub-expressão $\lambda y.(yx)$:

• $y$ é ligado pelo segundo $\lambda y$.
• $x$ é livre, pois não há um $\lambda x$ nesta sub-expressão que o ligue. O $x$ aqui não está conectado ao $\lambda x$ da primeira parte, porque os escopos são separados.

Quando avaliamos essa aplicação, o $x$ livre em $\lambda y.(yx)$ permanece livre, indicando que seu valor viria de fora da expressão.

Referências

---

Aula 1 - Cálculo Lambda