¿El combinador Y contradice la correspondencia Curry-Howard?

El combinador Y tiene el tipo . Según la correspondencia de Curry-Howard, debido a que el tipo ( a → a ) → a está habitado, debe corresponder a un verdadero teorema. Sin embargo, a → a siempre es cierto, por lo que parece que el tipo del combinador Y corresponde al teorema a , que no siempre es cierto. ¿Cómo puede ser esto?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

La correspondencia original de Curry-Howard es un isomorfismo entre la lógica proposicional intuicionista y el cálculo lambda de tipo simple.

Existen, por supuesto, otros isomorfismos similares a Curry-Howard; Phil Wadler señaló que el nombre de dos cañones "Curry-Howard" predice otros nombres de dos cañones como "Hindley-Milner" y "Girard-Reynolds". Sería divertido si "Martin-Löf" fuera uno de ellos, pero no lo es. Pero yo divago.

El combinador Y no contradice esto, por una razón clave: no se puede expresar en el cálculo lambda de tipo simple.

De hecho, ese era todo el punto. Haskell Curry descubrió el combinador de punto fijo en el cálculo lambda sin tipo, y lo usó para demostrar que el cálculo lambda sin tipo no es un sistema de deducción de sonido.

Curiosamente, el tipo de Y corresponde a una paradoja lógica que no es tan conocida como debería ser, llamada la paradoja de Curry. Considera esta oración:

Si esta oración es verdadera, entonces Santa Claus existe.

Supongamos que la oración fuera cierta. Entonces, claramente, Santa Claus existiría. Pero esto es precisamente lo que dice la oración, por lo que la oración es verdadera. Por lo tanto, Santa Claus existe. QED

El Curry-Howard relaciona los sistemas de tipos con los sistemas de deducción lógica. Entre otras cosas, mapea:

• programas para pruebas
• programa de evaluación para transformaciones en pruebas
• tipos habitados a proposiciones verdaderas
• sistemas de tipo a sistemas de deducción lógica

Si el sistema de tipos admite un combinador Y, eso significa que el sistema de deducción lógica correspondiente es inconsistente : todo teorema es verdadero. En el lado del programa, el combinador Y permite cualquier función de tipo$a \to b$ para ser definido, para cualquier $a$ y $b$: $Y (\lambda x. x) \to Y (\lambda x.M)$. La regla de deducción correspondiente permite que cualquier proposición se derive de cualquier otra proposición. Por lo tanto, el sistema lógico es inconsistente.

La correspondencia de Curry-Howard es solo eso: una correspondencia. En sí mismo, no dice que ciertos teoremas sean ciertos. Dice que la tipificabilidad / demostrabilidad se lleva de un lado a otro.

La correspondencia de Curry-Howard es útil como herramienta de prueba con muchos sistemas de tipos: cálculo lambda simplemente tipado, sistema F, cálculo de construcciones, etc. Todos estos sistemas de tipo tienen la propiedad de que la lógica correspondiente es consistente (si las matemáticas habituales son consistentes) ) También tienen la propiedad de no permitir la recurrencia arbitraria. La correspondencia de Curry-Howard muestra que estas dos propiedades están relacionadas.

El Curry-Howard todavía se aplica a los cálculos tipados sin terminación y los sistemas de deducción inconsistentes. Simplemente no es particularmente útil allí.