Função de sucessor no cálculo lambda

---

Summary

A função de sucessor no cálculo lambda, definida como $S\equiv \lambda wyx.y(wyx)$, 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 $n$ e retorna $n+1$.

Definição

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

$$S\equiv \lambda wyx.y(wyx)$$

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

• $0\equiv \lambda sz.z$ (zero aplicações de $s$),
• $1\equiv \lambda sz.s(z)$ (uma aplicação de $s$),
• $2\equiv \lambda sz.s(s(z))$ (duas aplicações de $s$), e assim por diante.

O papel de $S$ é adicionar uma aplicação extra de $s$, transformando $n$ em $n+1$.

Detalhando a Função de Sucessor

A expressão $\lambda wyx.y(wyx)$ pode parecer complicada à primeira vista, mas ela é uma função de três argumentos:

• $w$: Representa o numeral de Church que queremos incrementar (por exemplo, $0$, $1$, etc.).
• $y$: Será a função “sucessor” ($s$) do numeral resultante.
• $x$: Será o valor base ($z$) do numeral resultante.

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

Exemplo

Exemplo: Calculando $S0$

Dado:

• $S\equiv \lambda wyx.y(wyx)$,
• $0\equiv \lambda sz.z$,

Queremos computar $S0$:

1. Substituição Inicial:

   $$S0=(\lambda wyx.y(wyx))(\lambda sz.z)$$

2. Aplicação do Argumento $w$:

   • Substituímos $w$ por $\lambda sz.z$ na expressão:
   $$\lambda yx.y((\lambda sz.z)yx)$$

3. Avaliação de $(\lambda sz.z)yx$:

   • Aplicamos $\lambda sz.z$ aos argumentos $y$ e $x$:
     • Substituímos $s$ por $y$ e $z$ por $x$ em $z$:
     $$(\lambda sz.z)yx=x$$
   • Então:
   $$\lambda yx.y((\lambda sz.z)yx)=\lambda yx.yx$$

4. Simplificação Final:

   • Note que $\lambda yx.yx$ é o mesmo que $\lambda sz.sz$ (apenas renomeando variáveis):
   $$\lambda yx.yx\equiv \lambda sz.s(z)\equiv 1$$

Resultado: $S0=\lambda sz.s(z)$, que é o numeral de Church para 1.

Referências

---

Aula 1 - Cálculo Lambda