¿Cómo ejemplifica el combinador Y "inconsistencia de cálculo Lambda"?

En la página de Wikipedia para Fixed Point Combinators está escrito el texto bastante misterioso.

El combinador Y es un ejemplo de lo que hace que el cálculo Lambda sea inconsistente. Por lo tanto, debe considerarse con sospecha. Sin embargo, es seguro considerar el combinador Y cuando se define solo en lógica matemática.

¿He entrado en algún tipo de novela de espías? ¿Qué significan las afirmaciones de que -calculus es "inconsistente" y que debe "considerarse con sospecha" ?$\lambda$

Está inspirado en hechos reales, pero la forma en que se afirma es apenas reconocible y "debe considerarse con sospecha" no tiene sentido.

La coherencia tiene un significado preciso en la lógica: una teoría coherente es aquella en la que no se pueden probar todas las afirmaciones. En la lógica clásica, esto es equivalente a la ausencia de una contradicción, es decir, una teoría es inconsistente si y sólo si hay una declaración detales que la teoría demuestra tantoy su negación.$A$$A$$\neg A$

Entonces, ¿qué significa esto con respecto al cálculo lambda? Nada. El cálculo lambda es un sistema de reescritura, no una teoría lógica.

Es posible ver el cálculo lambda en relación con la lógica. Considere que las variables representan una hipótesis en una prueba, las abstracciones lambda como pruebas bajo una determinada hipótesis (representada por la variable), y la aplicación como una prueba condicional y una prueba de la hipótesis. Entonces la regla beta corresponde a simplificar una prueba aplicando modus ponens , un principio fundamental de la lógica.

Sin embargo, esto solo funciona si la prueba condicional se combina con una prueba de la hipótesis correcta. Si tiene una prueba condicional que asume y también tiene una prueba de , no puede combinarlos. Si desea que esta interpretación del cálculo lambda funcione, debe agregar una restricción que solo las pruebas de la hipótesis adecuada se apliquen a las pruebas condicionales. Esto se llama sistema de tipos , y la restricción es la regla de escritura que dice que cuando pasa un argumento a una función, el tipo del argumento debe coincidir con el tipo de parámetro de la función.$n=3$$n=2$

La correspondencia de Curry-Howard es un paralelo entre los cálculos mecanografiados y los sistemas de prueba.

• los tipos corresponden a declaraciones lógicas;
• los términos corresponden a pruebas;
• los tipos habitados (es decir, los tipos en los que existe un término de ese tipo) corresponden a declaraciones verdaderas (es decir, las declaraciones en las que hay una prueba de esa declaración);
• La evaluación del programa (es decir, reglas como beta) corresponden a transformaciones de pruebas (que mejor transforman las pruebas correctas en pruebas correctas).

Un cálculo tipado que tiene un combinador de punto fijo como permite construir un término de cualquier tipo (intente evaluar ), por lo que si toma la interpretación lógica a través de la correspondencia Curry-Howard, obtendrá una teoría inconsistente. Ver ¿El combinador Y contradice la correspondencia Curry-Howard? para más detalles.$Y$$Y (\lambda x.x)$

Esto no es significativo para el cálculo lambda puro, es decir, para el cálculo lambda sin tipos.

En muchos cálculos mecanografiados, es imposible definir un combinador de punto fijo. Esos cálculos mecanografiados son útiles con respecto a su interpretación lógica, pero no como base para un lenguaje de programación completo de Turing. En algunos cálculos mecanografiados, es posible definir un combinador de punto fijo. Esos cálculos mecanografiados son útiles como base para un lenguaje de programación completo de Turing, pero no con respecto a su interpretación lógica.

En conclusión:

• El cálculo lambda no es "inconsistente", ese concepto no se aplica.
• Un cálculo lambda mecanografiado que asigna un tipo a cada término lambda es inconsistente. Algunos cálculos lambda mecanografiados son así, otros hacen que algunos términos no se puedan escribir y sean consistentes.
• Los cálculos lambda mecanografiados no son la única razón de ser del cálculo lambda, e incluso los cálculos lambda mecanografiados inconsistentes son herramientas muy útiles, simplemente para no probar las cosas.

Me gustaría agregar uno a lo que dijo @Giles.

La correspondencia de Curry-Howard hace un paralelo entre -terms (más específicamente, los tipos de -terms) y los sistemas de prueba.$\lambda$$\lambda$

Por ejemplo, tiene el tipo (donde significa "función de a "), que corresponde a la declaración lógica . La función tiene el tipo , correspondiente a . Podemos convertir cualquier tipo de cálculo lambda a una tautología lógica mediante, en cierto sentido, "coincidencia de patrones" en las funciones.$\lambda x.\lambda y.x$$a \to (b \to a)$$a \to b$$a$$b$$a \implies (b \implies a)$$\lambda x.\lambda y.xy$$(a \to b) \to (a \to b)$$(a \implies b) \implies (a \implies b)$

El problema surge cuando consideramos el combinador Y, definido como . El problema surge porque esperamos que el combinador Y, como un combinador de "punto fijo", tenga un tipo (porque toma una función de un tipo a ese mismo tipo y encuentra un valor fijo- punto para esa función, que tiene ese tipo). La conversión de esto a una declaración lógica produce . Esto es una contradicción:$\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$(a \to a) \to a$$(a \implies a) \implies a$

Aceptar en un sistema de tipos lleva a que el sistema de tipos sea inconsistente. Esto significa que podemos$(a \to a) \to a$

• No permitir tipos como en un sistema de tipo (esto le da la Simplemente mecanografiada -calculus ), o$(a \to a) \to a$$\lambda$
• Vive con el sistema de tipos siendo inconsistente como un sistema de deducción lógica.