Função de sucessor no cálculo lambda §

---

Abstract

A função de sucessor no cálculo lambda, definida como , mostrando como ela transforma um numeral de Church no próximo número natural..

No cálculo lambda, números são representados como funções (os chamados numerais de Church), e operações aritméticas, como “somar um”, também são expressas como funções puras.

A função de sucessor é uma dessas operações fundamentais: ela pega um número e retorna .

Definição §

A função de sucessor () no cálculo lambda é definida como:

Essa função toma um numeral de Church e produz o numeral correspondente a . Para recordar, os numerais de Church representam números naturais assim:

• (zero aplicações de ),
• (uma aplicação de ),
• (duas aplicações de ), e assim por diante.

O papel de é adicionar uma aplicação extra de , transformando em .

Detalhando a Função de Sucessor §

A expressão pode parecer complicada à primeira vista, mas ela é uma função de três argumentos:

• : Representa o numeral de Church que queremos incrementar (por exemplo, , , etc.).
• : Será a função “sucessor” () do numeral resultante.
• : Será o valor base () do numeral resultante.

O corpo aplica (o número original) aos argumentos e , e então aplica mais uma vez ao resultado. Isso efetivamente “acrescenta uma camada” ao número original.

Exemplo §

Exemplo: Calculando §

Dado:

• ,
• ,

Queremos computar :

1. Substituição Inicial:

2. Aplicação do Argumento :

   • Substituímos por na expressão:

3. Avaliação de :

   • Aplicamos aos argumentos e :
     • Substituímos por e por em :
   • Então:

4. Simplificação Final:

   • Note que é o mesmo que (apenas renomeando variáveis):

Resultado: , que é o numeral de Church para 1.

Referências §

---

Aula 1 - Cálculo Lambda