Relação entre decisão de verificação de tipo, decisão de tipabilidade e forte normalização

Ei! Esta é provavelmente uma pergunta estúpida, mas nunca a vi explicitamente anotada se, por exemplo, a decidibilidade da verificação de tipo for equivalente à forte propriedade de normalização. Portanto, estou fazendo esta pergunta para esclarecer todas as relações possíveis entre verificação de tipo, tipabilidade e forte normalização.

Deixe-me explicar minha motivação. Para teorias de tipos (estou sendo intencionalmente vago aqui, mas estou interessado principalmente em teorias de tipos dependentes), uma forte normalização é usada para provar a decidibilidade da verificação de tipos. Por outro lado, qualquer sistema digitado que eu conheça e que tenha uma dessas propriedades também tem a outra. No entanto, nunca vi explicitamente declarar que uma normalização forte é equivalente à decidibilidade da verificação de tipo.

Analogamente, para provar a tipabilidade, geralmente (talvez sempre), reduz um termo para uma forma normal. No entanto, sabe-se que a tipabilidade não é verdadeira para as teorias de tipos dependentes, enquanto uma forte normalização pode se manter.

Pela decidibilidade da verificação de tipo, quero dizer que para qualquer tipo $A$contexto $\Gamma$ e termo não digitado $a$, é possível decidir em um número finito de etapas se $\Gamma \vdash a: A$ é verdade ou não.

Por decidibilidade da tipabilidade, quero dizer que, para qualquer termo não digitado $a$, é possível decidir em um número finito de etapas se existe um contexto $\Gamma$ e um tipo $A$ de tal modo que $\Gamma \vdash a: A$ é verdade.

1) É verdade que a decidibilidade da verificação de tipo é equivalente a todos os termos serem fortemente normalizáveis?

2) De maneira mais geral, qual a relação entre a decidibilidade da verificação do tipo, a tipabilidade e a forte normalização? Qual implica o outro?

Desde já, obrigado.

EDITAR

Dada a insatisfação com relação ao nível de generalidade da minha pergunta (da qual eu desconhecia), gostaria de delimitá-la apenas para Pure Type Systems. Obviamente, comentários adicionais ou contra-exemplos sobre outras teorias de tipos serão de grande utilidade.

Vou dar uma resposta mais focada e técnica à de Martin. Se estamos interessados ​​em teorias de tipos dependentes, nenhuma direção é óbvia, mas geralmente se supõe que ambas sejam válidas. No entanto, a direção Decidable$\Rightarrow$Normalizar é aberto, acredito, mesmo para sistemas relativamente bem compreendidos, embora tenhamos resultados parciais. Esta pergunta explora alguns dos mesmos problemas.

Mais tecnicamente: um bom quadro técnico para estas perguntas é a configuração de Sistemas de tipo puro em que a normalização não implica decidibilidade de verificação de tipo. O resultado é folclore, mas não trivial, pois é necessário encontrar uma estratégia para quando aplicar a regra de conversão. A estratégia óbvia é normalizar tipos inferidos antes de todos os aplicativos da regra de aplicativo. Existem algumas sutilezas até aqui, onde a correção de uma estratégia natural (mais eficiente) chamada adiamento da expansão ficou aberta por um tempo, mas foi resolvida desde então.

Existem sistemas de tipos que estão normalizando, mas são indecidíveis, principalmente o sistema com tipos de interseção que digita exatamente os termos de normalização e, portanto, devem ser indecidíveis (caso contrário, poderiam ser usados ​​para identificar termos de normalização). Seria tentador dizer aqui que o sistema está com defeito no sentido de que não é direcionado ao tipo , ou seja, os termos não contêm informações suficientes para descobrir o tipo.

Agora, o inverso, que sugeriria que sistemas não normalizantes são indecidíveis, está longe de ser óbvio: ficou aberto por um tempo até os famosos $Type:Type$sistema de Martin-Löf! Este caso foi resolvido dando um exemplo de um combinador de loop, que permite escrever cálculos arbitrários.

No entanto, o problema geral ainda está aberto para sistemas gerais de tipo puro, embora se acredite que seja verdade, e alguns resultados parciais foram mostrados nessa direção, por exemplo, aqui .

(1) falso. Exemplo de contador: Java, Scala, Haskell, ...

(2) Nenhuma relação geral é válida, depende realmente dos detalhes do idioma / sistema de digitação. Há uma exceção: para idiomas sãos e sistemas de digitação, imagino que a decidibilidade da inferência de tipos (que eu assumo ser o que você quer dizer com "tipabilidade") implica trivialmente a verificação de tipos. Mas eu não ficaria surpreso se alguém pudesse inventar um sistema louco onde nem mesmo essa implicação se aplica.