¿Qué hace que la inferencia de tipos para tipos dependientes sea indecidible?

He visto mencionar que los sistemas de tipo dependiente no son infecciosos, pero son comprobables. Me preguntaba si hay una explicación simple de por qué es así, y si existe o no un límite de "dependencia" donde los tipos pueden ser indexados por valores, ¿debajo de qué inferencia de tipos es posible y por encima de cuál no?

Para una versión bastante simple de la teoría del tipo dependiente, Gilles Dowek dio una prueba de indecidibilidad de la tipificación en un contexto no vacío:

Gilles Dowek, La indecisión de typability en el -calculus$\lambda\Pi$

Que se puede encontrar aquí .

Primero permítanme aclarar lo que se prueba en ese documento: muestra que en un cálculo dependiente sin anotaciones en las abstracciones, es indecidible mostrar la tipificación de un término en un contexto no vacío . Ambas hipótesis son necesarias: en el contexto vacío, la tipificación se reduce a la del cálculo simple (decidible por Hindley-Milner) y con las anotaciones sobre las abstracciones, se aplica el algoritmo habitual de tipo dirigido.$\lambda$

La idea es codificar un problema de correspondencia posterior como un problema de conversión de tipo, y luego construir cuidadosamente un término que sea escribible si los dos tipos específicos son convertibles. Esto utiliza el conocimiento de la forma de las formas normales, que siempre existen en este cálculo. El artículo es breve y está bien escrito, por lo que no entraré en más detalles aquí.

Ahora, en cálculos polimórficos como system-F, sería bueno poder inferir las abstracciones de tipo y las aplicaciones, y omitir las anotaciones en s como se anteriormente. Esto también es indecidible, pero la prueba es mucho más difícil y la pregunta estuvo abierta durante bastante tiempo. El asunto fue resuelto por Wells:$\lambda$

JB Wells, Typability y type check en el Sistema F son equivalentes e indecidibles .

Esto se puede encontrar aquí . Todo lo que sé al respecto es que reduce el problema de la semiunificación (que es la unificación del módulo de instanciación de cuantificadores universales, y es indecidible) a la verificación de tipos en el Sistema F.

Finalmente, es bastante fácil demostrar que la habitación de familias dependientes es indecidible: simplemente codifique un problema de Post en los índices del constructor. Aquí hay algunas diapositivas de Nicolas Oury que esbozan el argumento.

En cuanto a si hay un "límite", depende mucho de lo que intente hacer con sus tipos dependientes, y hay muchas aproximaciones que intentan ser decidibles, o al menos lo suficientemente cercanas como para ser utilizables. Sin embargo, estas preguntas siguen formando parte de una investigación activa.

Una posible vía es el campo de los "tipos de refinamiento" donde el lenguaje de expresión de las dependencias de los tipos está restringido para permitir ver verificaciones decidibles, por ejemplo, Tipos líquidos . Sin embargo, es raro que la inferencia de tipo completo sea decidible incluso en estos sistemas.