Decidibilidade da inferência e verificação de tipo no MLTT

1. Na Teoria Intuicionista de Tipos: Parte Predicativa de Martin-Löf , está provado que a verificação de tipo é decidível, sujeita a um tipo de letra em primeiro lugar, provando um teorema de normalização para termos tipificados fechados. Por outro lado, eu já vi escrito em vários lugares (Wikipedia, Nördstrom etc.) que a verificação de tipo no MLTT (intensional) é decidível; eles estão implicitamente restringindo a termos tipificáveis?$a \colon A$$a$

2. Sabe-se algo sobre a decidibilidade da inferência ou verificação de tipo no MLTT intensional se não restringirmos os termos tipificáveis? Por exemplo, talvez exista um processo de decisão que reconheça termos não tipáveis, digamos, normalizando para um formulário que não corresponda a nenhum dos construtores, ou mostrando que não há uma sequência não periódica de reduções para qualquer termo não tipável.

   Não pude encontrar muita coisa na literatura.

Certamente o problema de decisão

Dado um (pré-) termo Existe um tipo A tal que ⊢ a : A é derivável no MLTT?$a$$A$$\vdash a :A$

Às vezes escrito (e chamado de problema de inferência de tipo ) é decidível, ou seja, não importa se um é bem digitado ou não para obter uma resposta. De fato, todos os verificadores de prova baseados no MLTT implementam alguma versão desse algoritmo de decisão!$\vdash a\ :\ ?$$a$

Obviamente, o problema em um contexto não-vazio ( ) É decidível, bem como, normalmente você precisa resolver o último para resolver o antigo.$\Gamma\vdash a\ :\ ?$

Isso deve responder às perguntas 1 e 2. O algoritmo não envolve a normalização de , o que em geral seria uma má notícia, pois é indecidível se um termo não digitado se normaliza para algo. No entanto, a verificação de tipo algoritmo que envolvem normalizando tipos , que são por construção bem-digitado si.$a$

Como resultado, a normalização de termos bem digitados é uma condição necessária para que o problema de inferência de tipo seja decidido.

Você pode consultar Nordström, Petersson e Smith para obter uma introdução.

Não conheço nenhuma descrição genérica de um algoritmo de inferência de tipos para normalizar teorias de tipos, embora Pollack dê uma boa visão geral (embora o estado da arte tenha melhorado) em Tipechecking em Pure Type Systems .

Gostaria de complementar a resposta por cody através de uma observação geral que transmita minha compreensão do porquê os algoritmos de verificação de tipo funcionam.

Para uma ampla classe de teorias de tipos, a verificação ou inferência de tipos é realizada de tal maneira que nunca tentamos normalizar um termo, a menos que tenhamos estabelecido previamente que ele é bem digitado. Da mesma forma, nunca tentamos normalizar um tipo, a menos que já tenhamos estabelecido que é um tipo. Por esse motivo, podemos ter certeza de que a normalização será encerrada (o que requer uma prova separada).

É preciso olhar para algoritmos específicos e ver se eles realmente funcionam dessa maneira, mas funcionam. Eu só queria dizer o que os faz funcionar. Ou melhor, é por isso que eles param de funcionar.