Solo quiero conocer algunos ejemplos de las funciones que pueden calcularse con el cálculo lambda sin tipo pero no con los cálculos lambda con tipo.
Como soy un principiante, agradecería cierta reiteración de la información de fondo.
Gracias.
Editar: por cálculos lambda mecanografiados, tenía la intención de saber sobre el Sistema F y el cálculo lambda simplemente mecanografiado. Por función, me refiero a cualquier función computable de Turing.
pl.programming-languages
type-theory
lambda-calculus
computable-analysis
Timothy Zacchari
fuente
fuente
Respuestas:
Godelization da un buen ejemplo: en el cálculo lambda, lo único que puede hacer con una función es aplicarlo. Como resultado, no hay forma de escribir una función cerrada de tipo , que toma un argumento de función y le devuelve un código Godel.( N → N ) → N
Agregar esto como un axioma a la aritmética de Heyting generalmente se llama "la tesis constructiva de la Iglesia", y es un axioma fuertemente anticlásico. Es decir, es consistente agregarlo a HA, ¡pero no a la aritmética de Peano! (Básicamente, es un hecho clásico que cada máquina de Turing se detiene o no, y no hay una función computable que pueda presenciar este hecho).
fuente
La respuesta más simple viene dada por el hecho de que los cálculos lambda mecanografiados corresponden a lógicas (simplemente cálculo lambda mecanografiado -> lógica predicada; sistema f -> lógica de segundo orden) y las lógicas consistentes no pueden probar su propia consistencia.
Entonces, digamos que tiene números naturales (o una codificación de números naturales de la Iglesia) en su cálculo lambda escrito. Es posible hacer una numeración de Gödel que asigna cada término en el Sistema F a un número natural único. Luego, hay una función que toma cualquier número natural (que corresponde a un término bien tipado en el Sistema F) a otro número natural (que corresponde a la forma normal de ese término bien tipado del Sistema F) y hace algo más para cualquier número natural que no corresponde a un término bien tipado en el Sistema F (por ejemplo, devuelve cero). La función f es computable, por lo que puede ser calculada por el cálculo lambda sin tipo, pero no por el cálculo lambda con tipo (porque este último sería una prueba de la coherencia de la lógica de segundo orden enf f lógica de segundo orden, lo que implicaría que la lógica de segundo orden es inconsistente).
Advertencia 1: Si la lógica de segundo orden es inconsistente, podría ser posible escribir en el Sistema F ... y / o podría no ser posible escribir f en el cálculo lambda sin tipo; podría escribir algo, pero podría no siempre termina, que es un criterio para "computable".f f
Advertencia 2: a veces, por "cálculo lambda simplemente escrito", la gente quiere decir "cálculo lambda simplemente escrito con un operador de punto fijo o funciones recursivas". Esto sería más o menos PCF , que puede calcular cualquier función computable, al igual que el cálculo lambda sin tipo.
fuente
El cálculo tipo posee recursividad general en forma de combinador Y. El cálculo simple de λ no lo hace. Por lo tanto, cualquier función que requiera recursividad general es candidata, por ejemplo, la función de Ackermann. (Estoy omitiendo algunos detalles sobre cuán precisamente representamos los números naturales en cada sistema, pero esencialmente cualquier enfoque razonable servirá).λ Y λ
Por supuesto, siempre puedes extender el cálculo tipo simple para que coincida con el poder de Y , pero luego estás cambiando las reglas del juego.λ Y
fuente
fuente
Una visión de los límites de los cálculos fuertemente normalizados que me gustan es el ángulo de computabilidad. En un cálculo tipado fuertemente normalizado, como el cálculo lambda de tipo simple, el Sistema F o el Cálculo de construcciones, tiene una prueba de que todos los términos terminan finalmente.
Si esta prueba es constructiva, obtienes un algoritmo fijo para evaluar todos los términos con un límite superior garantizado en el tiempo de cálculo. O también puede estudiar la prueba (no necesariamente constructiva) y extraer un límite superior, que probablemente sea enorme , porque esos cálculos son expresivos.
Este límite le ofrece ejemplos "naturales" de funciones que no se pueden escribir en este cálculo lambda fijo: todas las funciones aritméticas que son asintóticamente superiores a este límite.
Si no recuerdo mal, los términos escritos en el cálculo lambda de tipo simple se pueden evaluar en torres exponenciales
O(2^(2^(...(2^n)..)
:; una función que crece más rápido que todas esas torres no será expresable en este cálculo. El sistema F corresponde a la lógica intuitiva de segundo orden, por lo que el poder de computación es simplemente enorme. Para aprovechar la fuerza de computabilidad de teorías aún más poderosas, generalmente razonamos en términos de teoría de conjuntos y teoría de modelos (por ejemplo, qué ordinales se pueden construir) en lugar de la teoría de computabilidad.fuente
fuente
A
tal queA \ident A \rightarrow A
no sea extraño? Me parece absurdo, ¿qué estoy pasando por alto?