Numerais igreja: como codificar zero no cálculo lambda?

Question

Estou aprendendo cálculo lambda, mas eu não consigo entender a codificação para o número 0.

Como é " função que leva em uma função e um segundo valor e aplica a função de zero vezes no argumento " um zero? Existe alguma outra maneira de codificar de zero? alguém aqui poderia me ajudar a codificar 0?

Answer 1

"Função que leva em uma função e um segundo valor e aplica a função de zero vezes no argumento"

A é, evidentemente, não zero. É um codificação de zero. Quando você lida com cálculo lambda simples, você tem que números codificar (bem como outros tipos primitivos), de alguma forma, e há algumas exigências ditadas por cada um destes tipos. Por exemplo, um requisito para números naturais é ser capaz de adicionar 1 a um determinado número, e outra é ser capaz de distinguir zero a partir números maiores (se você quiser saber mais, procure por "Peano Arithmetic"). A codificação popular que Dario citado lhe dá essas duas coisas, e ele também está representando um inteiro N por uma função que faz algo (codificado como o argumento f) N vezes -. Que é uma espécie de uma maneira natural de naturais de uso

Existem outras codificações que são possíveis - por exemplo, uma vez que você pode representar listas, você pode representar N como uma lista de itens N. Estas codificações têm seus prós e contras, mas o acima é de longe o mais popular.

Answer 2

Consulte wikipedia :

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

Se você aprender Lambda Calculus, você provavelmente já sabe que ?xy.y arg1 * arg2 * irá reduzir a arg2 , uma vez que o x é substituída por nada, eo restante (?y.y) é a função identidade.

Você poderia escrever de zero em muitas outras maneiras (ou seja, chegar a uma convenção diferente), mas há boas razões para usar ?xy.y. Por exemplo, você quer zero a ser o primeiro número natural, de modo que se você aplicar a função sucessor para ele, você ganha 1, 2, 3 etc. Com a ?abc.b função (abc), você começa ?xy.x (y ), ?xy.x (x (y)), ?xy.x (x (x (y))) etc., em outras palavras, você tem um sistema de número inteiro.

Além disso, você quer zero a ser o elemento neutro em relação à adição. Com a função de sucessor S: = ?abc.b (abc), podemos definir n + * m * como n S m , isto é, n vezes a aplicação da função sucessor m . Nossos ?xy.y satisfaz Zero A utilização deste, ambos 0 S m e m S 0 reduzir a m .