estoy aprendiendo cálculo lambda, pero me parece que no puede entender la codificación para el número 0.Números de iglesia: cómo codificar cero en cálculo lambda?
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 de" una ¿cero? ¿Hay alguna otra forma de codificar cero? ¿Podría alguien aquí ayudarme a codificar 0?
"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 que codifica de cero. Cuando trabajas con cálculo lambda simple, tienes que codificar números (así como otros tipos primitivos) de alguna manera, y hay algunos requisitos dictados para cada uno de estos tipos. Por ejemplo, un requisito para los números naturales es poder agregar 1 a un número dado, y otro es poder distinguir cero de números más grandes (si quiere saber más, busque "Aritmética de Peano"). La popular codificación que Dario citó le da estas dos cosas, y también representa un número entero N por una función que hace algo (codificado como el argumento f) N veces, que es una especie de forma natural de usar elementos naturales.
Existen otras codificaciones que son posibles; por ejemplo, una vez que puede representar listas, puede representar N como una lista de N elementos. Estas codificaciones tienen sus pros y sus contras, pero la de arriba es de lejos la más popular.
Ver 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
¿Por qué los votos a favor? – Dario
Estoy de acuerdo, he votado a favor su respuesta. ¡Responde la pregunta! –
No responde la pregunta, simplemente repite la codificación que el OP ya sabe claramente. Simplemente no entiende CÓMO o POR QUÉ 0 ≡ λf.λx. x (y yo tampoco, por eso estoy aquí jaja) – Ryan
Si se entera de cálculo lambda, que probablemente ya sabe que λxy.y arg1 arg2 * * reducirá a arg2, ya que la x se sustituye por nada, y el resto (λy.y) es la identidad función.
Puede escribir cero de muchas otras maneras (es decir, presentar una convención diferente), pero hay buenas razones para usar λxy.y. Por ejemplo, quiere que cero sea el primer número natural, de modo que si aplica la función sucesora a él, obtiene 1, 2, 3 etc. Con la función λabc.b (abc), obtiene λxy.x (y), λxy.x (x (y)), λxy.x (x (x (y))) etc., en otras palabras, obtienes un sistema de números enteros.
Además, desea que cero sea el elemento neutral con respecto a la suma. 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. Nuestro cero λxy.y satisface esto, tanto 0 S m y m S 0 reducen a m.
Esta es una pregunta relacionada que hice en grupos de google: decir que tengo una función f. ¿Cómo muestro que esto se traduce en un número natural 0? ¿Qué otras funciones necesito para deducir que mi función f se comporta como un 0? – unj2
Si desea probar que una función 'f' es cero con la codificación habitual, debe mostrar eso para todo' g' (f g x) == x. No necesitas saber nada más allá de esto. –