Los números de la iglesia: cómo codificar cero en el cálculo lambda?

Question

Estoy aprendiendo cálculo lambda, pero me parece que no puede entender la codificación para el número 0.

¿Cómo es " función que toma en una función y un segundo valor y aplica la función cero veces en el argumento " un cero? ¿Hay alguna otra forma de codificar cero? Podría alguien aquí me ayudará a codificar 0?

Answer 1

"función que toma en una función y un segundo valor y se aplica la función cero veces en el argumento de" A es, por supuesto, no es cero. Es un codificación de cero. Cuando tratas con el cálculo lambda llano, usted tiene que codificar los números (así como otros tipos primitivos) en alguna manera, y hay algunos requisitos dictados para cada uno de estos tipos. Por ejemplo, uno de los requisitos para los números naturales es ser capaz de añadir 1 a un número dado, y otra es ser capaz de distinguir cero a partir de los números más grandes (si usted quiere saber más, busque "Aritmética de Peano"). La codificación popular que Darío citó le da estas dos cosas, y también se representa un entero N por una función que hace algo (codificada como argumento f) - N veces. Que es una especie de una forma natural de utilizar productos naturales

Hay otras codificaciones que son posibles - por ejemplo, una vez que se puede representar listas, puede representar a N como una lista de N elementos. Estas codificaciones tienen sus pros y contras, pero el de arriba es de lejos el más popular.

Answer 2

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

Si se entera de cálculo lambda, es probable que ya saben que λxy.y arg1 * * arg2 reducirá a arg2 , ya que la x se sustituye por nada, y el resto (λy.y) es la función identidad.

Se podría escribir cero en muchas otras maneras (es decir, llegar a una convención diferente), pero hay buenas razones para utilizar λxy.y. Por ejemplo, desea cero para ser el primer número natural, de manera que si se aplica la función sucesor, se obtiene 1, 2, 3, etc. Con la función λabc.b (abc), se obtiene λxy.x (y ), λxy.x (x (y)), λxy.x (x (x (y))), etc., en otras palabras, se obtiene un sistema de número entero.

Además, desea cero para ser el elemento neutro con respecto a la adición. Con nuestra función sucesor S: = λabc.b (abc), podemos definir n + * m * como n S m , es decir, n veces la aplicación de la función sucesor m . Nuestros satisface cero λxy.y esto, tanto 0 S m y m S 0 se reducen a m .