El combinador de punto fijo FIX (también conocido como el combinador Y) en el cálculo lambda ( tipo) ( ) se define como:
FIX
Entiendo su propósito y puedo rastrear la ejecución de su aplicación perfectamente bien; Me gustaría entender cómo derivar FIX de los primeros principios .
Aquí es lo más lejos que puedo llegar cuando intento derivarlo yo mismo:
- FIX es una función: FIX
- FIX toma otra función, , para hacerla recursiva: FIX
- El primer argumento de la función es el "nombre" de la función, utilizada donde se pretende una aplicación recursiva. Por lo tanto, todas las apariencias del primer argumento de deberían ser reemplazadas por una función, y esta función debería esperar el resto de los argumentos de (supongamos que toma un argumento): FIX
Aquí es donde no sé cómo "dar un paso" en mi razonamiento. Las pequeñas elipses indican dónde falta algo en mi FIX (aunque solo puedo saberlo comparándolo con el FIX "real").
Ya he leído Tipos y lenguajes de programación , que no intenta derivarlo directamente, y en su lugar refiere al lector a The Little Schemer para una derivación. También lo he leído, y su "derivación" no fue tan útil. Además, es menos una derivación directa y más un uso de un ejemplo muy específico y un intento ad-hoc de escribir una función recursiva adecuada en .
Respuestas:
No he leído esto en ninguna parte, pero así es como creo que podría haberse derivado:Y
Tengamos una función recursiva , quizás un factorial o algo así. Informalmente, definimos f como término pseudo-lambda donde f aparece en su propia definición:F F F
Primero, nos damos cuenta de que la llamada recursiva se puede factorizar como un parámetro:
Ahora podríamos definir si solo tuviéramos una manera de pasarlo como un argumento para sí mismo. Esto no es posible, por supuesto, porque no tenemos f a mano. Lo que tenemos a la mano es M . Como M contiene todo lo que necesitamos para definir f , podemos tratar de pasar M como argumento en lugar de f e intentar reconstruir f a partir de él más adelante. Nuestro primer intento se ve así:F F METRO METRO f M f f
Sin embargo, esto no es completamente correcto. Antes, consiguió sustituido por r dentro de M . Pero ahora pasamos M en su lugar. Tenemos que arreglar de alguna manera todos los lugares en los que usamos r para que reconstruyen f de M . En realidad, esto no es nada difícil: ahora que sabemos que f = M M , en todas partes donde usamos r simplemente lo reemplazamos por ( r r ) .f r M M r f M f=MM r (rr)
Esta solución es buena, pero tuvimos que alterar dentro. Esto no es muy conveniente. Podemos hacer esto de manera más elegante sin tener que modificar M introduciendo otro λ que envía a M su argumento aplicado a sí mismo: Expresando M ′ como λ x . M ( x x ) obtenemosM M λ M M′ λx.M(xx)
De esta manera, cuando se sustituye por x , M M se sustituye por r , que es, por definición, igual a f . ¡Esto nos da una definición no recursiva de f , expresada como un término lambda válido!M x MM r f f
La transición a ahora es fácil. Podemos tomar un término lambda arbitrario en lugar de M y realizar este procedimiento en él. Entonces podemos factorizar M y definirY M M
De hecho, reduce a f como lo definimos.YM f
Nota: He derivado como se define en la literatura. El combinador que has descrito es una variante de Y de llamada por valor de idiomas, a veces también llamado Z . Ver este artículo de Wikipedia .Y Y Z
fuente
Como Yuval ha señalado, no hay un solo operador de punto fijo. Hay muchos de ellos. En otras palabras, la ecuación para el teorema del punto fijo no tiene una respuesta única. Por lo tanto, no puede derivar el operador de ellos.
Es como preguntar cómo las personas derivan como una solución para x = y . Ellos no! La ecuación no tiene una solución única.(x,y)=(0,0) x=y
En caso de que lo que quieras saber sea cómo se descubrió el primer teorema de punto fijo. Permítanme decir que también me pregunté cómo surgieron los teoremas de punto fijo / recursividad cuando los vi por primera vez. Parece muy ingenioso. Particularmente en la forma de la teoría de la computabilidad. A diferencia de lo que dice Yuval, no es el caso que la gente jugara hasta encontrar algo. Esto es lo que he encontrado:
Hasta donde recuerdo, el teorema se debe originalmente a SC Kleene. A Kleene se le ocurrió el teorema original de punto fijo al rescatar la prueba de inconsistencia del cálculo lambda original de Church. El cálculo lambda original de Church sufrió una paradoja tipo Russel. El cálculo lambda modificado evitó el problema. Kleene estudió la prueba de inconsistencia probablemente para ver cómo si el cálculo lambda modificado sufriría un problema similar y convirtió la prueba de inconsistencia en un teorema útil del cálculo lambda modificado. A través de su trabajo sobre la equivalencia del cálculo lambada con otros modelos de computación (máquinas de Turing, funciones recursivas, etc.) lo transfirió a otros modelos de computación.
¿Cómo derivar el operador que podría preguntar? Así es como lo tengo en cuenta. El teorema del punto fijo se trata de eliminar la autorreferencia.
Todos conocen la paradoja del mentiroso:
O en la forma más lingüística:
Ahora, la mayoría de las personas piensan que el problema con esta oración es con la autorreferencia. ¡No lo es! La autorreferencia puede eliminarse (el problema es con la verdad, un lenguaje no puede hablar sobre la verdad de sus propias oraciones en general, ver el teorema de la indefinibilidad de la verdad de Tarski ). La forma en que se elimina la autorreferencia es la siguiente:
fuente
Por lo tanto, debe definir un combinador de punto fijo
pero sin recursividad explícita. Comencemos con el combinador irreducible más simple.
El
x
en el primer lambda se sustituye repetidamente por el segundo lambda. La conversión alfa simple aclara este proceso:Es decir, la variable en la primera lambda siempre desaparece. Entonces, si agregamos una
f
a la primera lambdala
f
voluntad subeTenemos nuestra
omega
espalda. Ahora debería quedar claro que si agregamos unf
a la segunda lambda, entoncesf
aparecerá en la primera lambda y luego se disparará:Ya que
podemos reescribir la expresión como
que es solo
y tenemos nuestra ecuación
Y f = f (Y f)
. Entonces elY
combinador es esencialmentef
f
movimientofuente
Es posible que haya visto el ejemplo clásico de una ecuación sin una forma normal:
Se sugiere una ecuación similar para la recursividad general:
fuente