Decidabilidad de inferencia de tipos y verificación de tipos en MLTT

1. En una teoría intuitiva de tipos: parte predictiva de Martin-Löf, se demuestra que la comprobación de tipo es decidible sujeto a ser escribible en primer lugar, demostrando un teorema de normalización para términos de tipo cerrado. Por otro lado, lo he visto escrito en varios lugares (Wikipedia, Nördstrom, etc.) que la verificación de tipos en MLTT (intensional) es decidible; ¿están restringiendo implícitamente a términos que se pueden escribir?$a \colon A$$a$

2. ¿Se sabe algo acerca de la capacidad de decisión de inferencia de tipos o verificación de tipos en MLTT intensivo si no nos limitamos a los términos que se pueden escribir? Por ejemplo, tal vez hay un proceso de decisión que reconoce términos no tipificables, por ejemplo, normalizando a una forma que no corresponde a ninguno de los constructores, o mostrando que no hay una secuencia no periódica de reducciones para ningún término no tipificable.

   No he podido encontrar mucho en la literatura.

Ciertamente el problema de decisión

Dado un (pre) término ¿Existe un tipo A tal que ⊢ a : A sea ​​derivable en MLTT?$a$$A$$\vdash a :A$

A veces escrito (y llamado el problema de inferencia de tipos ) es decidible, lo que quiere decir que no importa si un está bien escrito o no para obtener una respuesta. De hecho, ¡todos los verificadores de pruebas basados ​​en MLTT implementan alguna versión de este algoritmo de decisión!$\vdash a\ :\ ?$$a$

Obviamente, el problema en un contexto que no esté vacía ( ) Es decidible, así, por lo general que necesita para resolver este último para resolver el anterior.$\Gamma\vdash a\ :\ ?$

Esto debería responder a las preguntas 1 y 2. El algoritmo no implica normalizar , lo que en general sería una mala noticia, ya que es indecidible si un término sin tipo se normaliza a algo. Sin embargo, el algoritmo de comprobación de tipos no involucrar a la normalización de los tipos , que son de construcción bien-escrito ellos mismos.$a$

Como resultado, la normalización de términos bien tipados es una condición necesaria para que el problema de inferencia de tipo sea decidible.

Es posible que desee consultar Nordström, Petersson y Smith para una introducción.

No conozco ninguna descripción genérica de un algoritmo de inferencia de tipos para normalizar las teorías de tipos, aunque Pollack ofrece una descripción bastante buena (aunque el estado del arte ha mejorado) en Typechecking en Pure Type Systems .

Me gustaría complementar la respuesta con cody mediante una observación general que transmita mi comprensión de por qué funcionan los algoritmos de verificación de tipo.

Para una amplia clase de teorías de tipo, la verificación de tipo o inferencia se realiza de tal manera que nunca intentemos normalizar un término, a menos que hayamos establecido de antemano que está bien escrito. Del mismo modo, nunca intentamos normalizar un tipo, a menos que ya hayamos establecido que es un tipo. Debido a esto, podemos estar seguros de que la normalización terminará (lo que requiere una prueba por separado).

Uno tiene que mirar algoritmos específicos y ver que realmente funcionan de esta manera, pero lo hacen. Solo quería decir qué los hace funcionar. O mejor, esa es la razón por la que dejan de funcionar.