Al leer el documento Una Introducción al Cálculo Lambda , me encontré con un párrafo que realmente no entendía, en la página 34 (mi cursiva):
Dentro de cada uno de los dos paradigmas hay varias versiones de cálculo lambda mecanografiado. En muchos sistemas importantes, especialmente aquellos a la Iglesia, los términos que tienen un tipo siempre poseen una forma normal. Por la insolubilidad del problema de detención, esto implica que no todas las funciones computables pueden ser representadas por un término mecanografiado, ver Barendregt (1990), Teorema 4.2.15. Esto no es tan malo como parece, porque para encontrar funciones computables que no puedan representarse, uno tiene que pararse sobre la cabeza. Por ejemplo, en 2, el cálculo de lambda tipificado de segundo orden, solo aquellas funciones recursivas parciales no pueden representarse como sumas totales, pero no de manera demostrable en el análisis matemático (aritmética de segundo orden).
Estoy familiarizado con la mayoría de estos conceptos, pero no el concepto de una función recursiva parcial, ni el concepto de una función demostrablemente total. Sin embargo, esto no es lo que me interesa aprender.
Estoy buscando una explicación simple de por qué ciertas funciones computables no pueden ser representadas por un término tipeado, así como por qué tales funciones solo se pueden encontrar 'de pie sobre la cabeza'.
fuente
Creo que la respuesta de Merijn maneja la primera parte de su pregunta bastante bien. Trataré de responder la segunda parte: por qué encontrar funciones que son computables pero no representables en el cálculo polimórfico requiere "pararse sobre la cabeza".λ
Me temo que requiere una explicación de los conceptos que no le interesan. Una función recusiva parcial es un -term que representa una función de a . A -term aplica al representante de un número natural es enviado a si y sólo si qué no tener una forma normal. Si no se envía ningún número a , decimos que la función es total . Ahora la idea es que ninguna teoría lógica puede probar que un términoλ N N∪{⊥} λ t n ⊥ t n ⊥ T t representa una función total para cada función total , siempre hay "puntos ciegos" donde termina en todas las entradas , pero la instrucciónt t n
es indecidible en . Si la afirmación anterior es demostrable en , decimos que la función representada por es demostrablemente total . Eso no todas las funciones totales son demostrablemente total en el es una consecuencia de (una variante de) la Godel incompletitud teorema para .T T t T T
Ahora el punto es que el programa de gran mayoría que deseamos escribir concretamente (clasificación de listas, recorrido de gráficos, sistemas operativos) no son solo funciones totales, sino que son demostrablemente totales en sistemas lógicos razonables, como Peano Arithmetic.
Ahora para el cálculo polimórfico . Se puede demostrar que los términos que se pueden escribir en este cálculo son exactamente los términos que representan las funciones demostrablemente totales en la aritmética de Peano de segundo orden. La aritmética de Peano de segundo orden es mucho, mucho más poderosa que la aritmética de Peano ordinaria.λ
Esto significa por las explicaciones anteriores que hay términos que son totales pero no demostrablemente totales, pero tales funciones son extremadamente raras, ya que ya son raras para la Aritmética de Peano (y mucho más raras en la teoría del segundo orden). De ahí la declaración de "pararse de cabeza".
fuente
Me resulta un poco difícil escribir de forma concisa la prueba, pero espero que esta explicación le brinde suficiente intuición para ver por qué los términos simples escritos no pueden representar todos los términos sin tipo.
El cálculo lambda simplemente tipado se está normalizando fuertemente. Cada reducción nos acercará a la forma normal. Cuando la función se aplica a un valor de tipo , reducirá a una función de tipo . Dado un número finito de argumentos, se necesita un número finito de pasos de reducción para alcanzar la forma -normal, en la que no hay más reducciones posibles.β f::α→β→γ α β β→γ β
Para contrastar esto con el cálculo lambda sin tipo. Uno de los combinadores UTLC más famosos es el combinador :Y
Cuando intentamos reducir el combinador sucede lo siguiente:Y
¡No importa qué funciones pasemos, nos quedamos atrapados en una secuencia infinita de reducciones! Si intentamos anclar un tipo STLC en el combinador UTLC, rápidamente lo encontramos imposible, porque la aplicación de función no reduce el tipo como se requiere en el STLC. El combinador es claramente computable (representa, usando la recursividad, el concepto de un bucle infinito), sin embargo, no puede representarse en el STLC, ya que todos los términos de STLC se están normalizando fuertemente.Y Y
fuente