¿Cómo exactamente el cálculo lambda captura la noción intuitiva de computabilidad?

12

He estado tratando de entender qué, por qué y cómo del cálculo pero no puedo entender "¿por qué funciona?"λ

"Intuitivamente" obtengo el modelo de computabilidad de Turing Machines (TM). Pero esta abstracción me deja confundido.λ

Supongamos que las TM no existen; entonces, ¿cómo puede uno estar "intuitivamente" convencido de la capacidad del cálculo para capturar esta noción de computabilidad. ¿De qué manera tener un montón de funciones para todo y su composobilidad implica computabilidad? ¿Que me estoy perdiendo aqui? Leí el artículo de Alonzo Church sobre eso, pero todavía estoy confundido y busco una comprensión más "tonta" de lo mismo.λ

soft-question computability lambda-calculus ho.history-overview intuition Doctor
fuente
¿Tiene el mismo problema con la reescritura de sistemas y gramáticas? En el cálculo lambda, las operaciones básicas son bastante simples: abstracción de funciones, aplicación de funciones por sustitución y cálculo es normalización beta. En otras palabras, no veo cuál es su problema con que sea un modelo razonable de cálculo.
Kaveh
2
No he visto a nadie dudar de que las funciones definibles de cálculo lambda son computables. Históricamente, la pregunta era si estas son las únicas funciones intuitivamente computables, lo cual es un problema completamente diferente de lo que parece preguntar.
Kaveh
1
Una cosa que encontré útil fue el libro de Raymond M Smullyan, "To Mock a Mockingbird", que reemplaza las funciones con pájaros en un bosque mágico (y es una buena lectura)
dspyz
1
El libro de Smullyans trata sobre la lógica combinatoria
Trismegistos

Respuestas:

21

λ

λλ

Andrej Bauer
fuente
44
Si caminar es tan divertido como dices, entonces debo probarlo.
Radu GRIGore
Andrej, ¿conoces alguna referencia para esto? Godel no aceptó que el modelo de Chruch capturara todas las funciones conmutables, pero no recuerdo haber visto en ningún lado que criticara el modelo mucho más que eso. Hasta donde yo sé, su crítica al modelo de cálculo lambada de Church estuvo a la par con su crítica a sus propias funciones recursivas generales de Godel-Herbrand.
Kaveh
3
Creo que quiere K. Godel: "Algunas observaciones sobre los resultados indecidibles", en Solomon Feferman, John Dawson y Stephen Kleene (eds.), Kurt Gödel: Collected Works Vol. Ii Prensa de la Universidad de Oxford. 305-306 (1972). Ver books.google.si/…
Andrej Bauer
6

Usted programa en ello! Echa un vistazo a las codificaciones de la iglesia . Puedes ver cómo se puede realizar casi toda la aritmética, lo que probablemente debería convencerte de que es extremadamente potente. Sin embargo, me gusta mirar las operaciones en las listas. Puede definir casi cualquier estructura de datos en términos de una función que realiza la operación más importante sobre ella.

Por ejemplo, una codificación de una lista es la función de plegado que se pliega sobre ella. Tenga en cuenta que esta no es la codificación de Church, sino una que obtuve de los tipos y lenguajes de programación de Percie. Las codificaciones de pares de Church no nos dan recurrencia, tenemos que agregarlo nuevamente en nosotros mismos con algún tipo de combinador de recursión.

entonces una lista toma dos argumentos, una función para hacer el plegado y un valor inicial para enchufarlo en algún momento.

cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a

ahora podemos definir una suma dada una función de agregar (ver codificaciones de la iglesia de arriba)

sum xs = xs add 0

podemos hacer más y definir una función de mapa

consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil

Si todavía no está convencido de que hay un cálculo aquí y desea asegurarse de que puede realizar cualquier cálculo, consulte el combinador de punto fijo . Sin embargo, a veces me duele un poco pensar en eso, así que no estoy seguro de que lo llame intuitivo, pero si lo evalúa manualmente con algunos argumentos, puede ver lo que está sucediendo.

Jake
fuente