Substituição no Cálculo Lambda §

---

No cálculo lambda, a substituição é o mecanismo que nos permite aplicar funções aos seus argumentos, substituindo variáveis por valores ou expressões.

É como ” executamos” uma função: pegamos o que ela diz para fazer e colocamos o argumento no lugar certo. Mas esse processo não é tão simples quanto parece — precisamos tomar cuidado para não misturar variáveis que têm significados diferentes.

Definição §

A substituição no cálculo lambda ocorre quando aplicamos uma função a um argumento , substituindo todas as ocorrências ligadas de no corpo por .

Formalmente, isso é escrito como:

onde:

• é o corpo da função,
• é a variável ligada pelo ,
• é a expressão que substitui .

Esse processo é chamado de β-redução, e o desafio está em garantir que a substituição preserve o significado original da expressão, evitando confusões entre variáveis livres (não ligadas por um ) e variáveis ligadas (definidas por um ).

Warning

A substituição exige atenção especial para evitar erros conhecidos como captura de variáveis.

Distinção entre variáveis livres e ligadas §

Como vimos anteriormente, uma variável é ligada se está no escopo de um que a define, e livre se não está.

Durante a substituição, precisamos garantir que uma variável livre no argumento não seja acidentalmente “capturada” por um interno à expressão, mudando seu significado.

Problema da Captura de Variáveis §

Se o argumento contém uma variável livre que coincide com uma variável ligada no corpo da função, uma substituição direta pode gerar um resultado incorreto.

Para corrigir isso, às vezes é necessário renomear as variáveis ligadas antes de substituir.

Técnica de renomeação (α-conversão) §

A renomeação, ou α-conversão, permite trocar o nome de uma variável ligada por outro nome que não aparece na expressão, desde que o significado permaneça o mesmo.

Por exemplo, é equivalente a . Isso é essencial para evitar conflitos na substituição.

Exemplo §

Exemplo 1 §

Considere a expressão:

Queremos aplicar a função externa ao argumento . Vamos passo a passo:

Substituição Direta (Errada) §

Substituímos por no corpo :

Isso está errado. O ligado (do ) se misturou com o livre (do argumento), criando uma expressão que não reflete o significado original. O interno deveria permanecer independente do argumento.

Renomeação (Correta) §

Antes de substituir, renomeamos a variável ligada por na função interna:

Agora, aplicamos a substituição de por :

Resultado: onde o é livre (vindo do argumento), e é ligado, preservando a distinção correta.

Referências §

---

Aula 1 - Cálculo Lambda