¿Cómo hacer que el cálculo Lambda se normalice fuertemente sin un sistema de tipos?

Se me ocurren algunas respuestas posibles que provienen de la lógica lineal.

El más simple es el cálculo lambda afín: considere solo los términos lambda en los que cada variable aparece como máximo una vez. Esta condición se preserva por reducción y es inmediato ver que el tamaño de los términos afines disminuye estrictamente con cada paso de reducción. Por lo tanto, el cálculo lambda afín sin tipo se está normalizando fuertemente.

Otros ejemplos interesantes (en términos de expresividad) son dados por los llamados cálculos lambda "ligeros", que surgen de los subsistemas de lógica lineal introducidos por Girard en "Light Linear Logic" (Información y Computación 143, 1998), también como "Soft Linear Logic" de Lafont (Theoretical Computer Science 318, 2004). Existen varios cálculos de este tipo en la literatura, quizás una buena referencia es el "Cálculo lambda afín ligero y la normalización fuerte del tiempo polinómico" (Archive for Mathematical Logic 46, 2007). En ese documento, Terui define un cálculo lambda derivado de la lógica afín a la luz y demuestra un fuerte resultado de normalización para él. Aunque los tipos se mencionan en el documento, no se usan en la prueba de normalización. Son útiles para una formulación ordenada de la propiedad principal del cálculo lambda afín ligero, a saber, que los términos de cierto tipo representan exactamente las funciones de Polytime. Se conocen resultados similares para el cálculo elemental, utilizando otros cálculos lambda "ligeros" (el artículo de Terui contiene más referencias).

Como nota al margen, es interesante observar que, en términos de prueba teórica, el cálculo lambda afín corresponde a la lógica intuicionista sin la regla de contracción. Grishin observó (antes de que se introdujera la lógica lineal) que, en ausencia de contracción, la ingenua teoría de conjuntos (es decir, con una comprensión sin restricciones) es coherente (es decir, la paradoja de Russel no da una contradicción). La razón es que la eliminación de cortes para la teoría de conjuntos ingenua sin contracción puede probarse mediante un argumento directo de disminución del tamaño (como el que di anteriormente) que no se basa en la complejidad de las fórmulas. A través de la correspondencia de Curry-Howard, esta es exactamente la normalización del cálculo lambda afín sin tipo. Es traduciendo la paradoja de Russel en lógica lineal y "retocando" las modalidades exponenciales para que no se pueda derivar una contradicción de que Girard ideó una lógica lineal ligera. Como mencioné anteriormente, en términos computacionales, la lógica lineal ligera da una caracterización de las funciones computables de tiempo polinomial. En términos de teoría de la prueba, una teoría de conjuntos ingenua consistente puede definirse en una lógica lineal ligera de modo que las funciones probables totales sean exactamente las funciones computables de tiempo polinomial (hay otro artículo de Terui sobre esto, "Teoría de conjuntos afín ligera: un ingenuo teoría de conjuntos del tiempo polinomial ", Studia Logica 77, 2004).

Damiano Mazza
fuente

Yo diría que el Cálculo Lambda Afín Ligero de Terui está escrito, dadas las restricciones sobre el uso de variables afines, la estratificación de los operadores y la monoidalidad del operador! Es solo que estas restricciones se introducen informalmente. El LLL de Girard también está escrito.

Martin Berger

@ Martin: No estoy de acuerdo. Las restricciones estructurales impuestas en términos afines ligeros son de una naturaleza diferente a las de un sistema de mecanografía. La mayor diferencia es que la tipificación es necesariamente inductiva, mientras que la formación de pozos (es decir, estratificación, uso afín, etc.) puede definirse como una propiedad combinatoria de un término. Entonces, por ejemplo, cuando escribe un término, generalmente tiene que escribir sus subterms, mientras que un subterm de un término estratificado no necesita ser estratificado.

Damiano Mazza

Lo siento, una cosa más sobre el LLL de Girard: el sistema obviamente está escrito porque involucra fórmulas. Sin embargo, como mencioné en mi respuesta, las fórmulas no juegan ningún papel en la eliminación de cortes LLL. De hecho, pueden agregarse puntos de fijación arbitrarios de fórmulas (¡incluida la fórmula paradójica de Russel, que es equivalente a su propia negación!) Sin que LLL se vuelva inconsistente. Esto se debe a que la eliminación de corte se cumple por razones "puramente estructurales", independientemente del hecho de que puede adjuntar tipos a sus pruebas (técnicamente, el teorema de eliminación de cortes para LLL puede probarse en redes de prueba sin tipo).

Damiano Mazza

OK, si haces de la inductividad una condición de que algo sea un sistema de mecanografía. Ese es un punto de vista interesante que no había visto antes.

Martin Berger

... y diría que es un punto de vista equivocado. Por ejemplo, en sistemas que involucran subtipificación (más generalmente, cuando se considera una interpretación extrínseca de los tipos en el sentido de Reynolds) es muy natural tener una visión coinductiva de la tipificación. Hay bastantes ejemplos en la literatura (aunque creo que esto se subestima).

Noam Zeilberger

El documento original de Church y Rosser, "Algunas propiedades de conversión", describe algo que puede ser un ejemplo de lo que está buscando.

$\lambda x.M$ $x$ $M$

$B$ $A$ $m$ $A$ $B$ $m$

Por lo tanto, aunque puede escribir términos sin terminación en el cálculo lambda estricto (sin tipo), cada término con una forma normal se normaliza fuertemente; es decir, cada secuencia de reducciones alcanzará esa forma normal única.

Rob Simmons
fuente

m

$m$

Esta vez terminé la declaración del teorema, gracias. La parte que escribí como [equivalencia de módulo alfa] era originalmente "(dentro de las aplicaciones de la Regla I)", lo que significa lo mismo a menos que no recuerde la Regla I correctamente.

Rob Simmons el

¿Cómo hacer que el cálculo Lambda se normalice fuertemente sin un sistema de tipos?

Respuestas: