A codificação numeral da Igreja de números naturais é desnecessariamente complicada?

Question

O livro Estrutura e Interpretação de Programas de Computador que tenho lido apresenta numerais de Igreja definindo zero e uma função de incremento

zero: λf. λx. x
increment: λf. λx. f ((n f) x)

Isso parecia muito complicado para mim e demorei muito tempo para descobrir e derivar um (λf.λx. f x) e dois (λf.λx. f (f x)).

Não seria muito mais simples codificar números dessa maneira, com zero sendo o lambda vazio?

zero: λ
increment: λf. λ. f

Agora é trivial derivar um (λ. λ) e dois (λ. λ. λ) e assim por diante.

Esta parece ser uma maneira muito mais óbvia e intuitiva de representar números com lambdas.Há algum problema com essa abordagem e, portanto, uma boa razão para os numerais da Igreja funcionarem da maneira que funcionam?Esta abordagem já foi atestada?

Answer 1

Sua codificação (zero: λx.x, um: λx.λx.x, dois: λx.λx.λx.x, etc.) torna mais fácil definir incremento e decremento, mas, além disso, torna-se bastante complicado desenvolver combinadores para sua codificação.Por exemplo, como você definiria isZero?

Uma maneira intuitiva de pensar sobre a codificação Church é que um n numeral é representado pela ação de iterar tempos de n.Isso facilita o desenvolvimento de combinadores como plus usando apenas a iteração codificada no número.Não há necessidade de combinadores sofisticados para recursão.

Na codificação Church, cada número tem a mesma interface: leva dois argumentos.Durante a codificação, cada número é definido pelo número de argumentos que leva, o que torna realmente difícil operar uniformemente.

Outra maneira de codificar numerais seria pensar nos números como n= 0 |S n, e use uma codificação vanilla para uniões.

Answer 2

A sintaxe proposta para os numerais não é válida no cálculo lambda, enquanto os numerais da Igreja são de fato construções válidas no cálculo lambda.Portanto, essa é uma possível razão pela qual os numerais da Igreja são como são - a codificação do número deve seguir o cálculo lambda ' definição de uma forma que também permite outras operações também definidas no cálculo lambda (incremento, por exemplo) para operar sobre os números codificados.