Existe uma boa noção de provas de não terminação e interrupção na teoria dos tipos?

A teoria do tipo construtivo, com sua interpretação básica sob a correspondência curry howard, consiste apenas de funções computáveis ​​totais. Na literatura, alguns foram mencionados sobre o uso da "teoria dos tipos computacionais" para representar a não terminação em programas funcionais; no entanto, nos artigos que encontrei, essa não parece ser a principal motivação da teoria (por exemplo, Benton menciona não-determinismo, continuações e exceções, sem entrar em muitos detalhes sobre a não-terminação), então ainda não encontrei um artigo que ofereça uma interpretação robusta da não-terminação usando a teoria computacional dos tipos.

Especificamente, o que estou procurando é uma maneira que, dado um tipo que representa um cálculo possivelmente não terminante do tipo , , deve haver alguma noção de provas de que termina do tipo , de tal modo que dadas e , pode-se construir um termo .t ( A ) x : T ( A ) H ( X ) x : T ( A ) p : H ( x ) ~ x : $A$$T(A)$$x : T(A)$$H(x)$$x:T(A)$$p:H(x)$$\tilde x : A$

Minha motivação para isso é que eu gostaria de, eventualmente, ser capaz de relacionar formalmente noções na teoria da complexidade computacional à teoria do tipo construtivo. Especificamente, estou interessado em saber quanto poder os tipos construtivos de teoria formal ganham com o acesso a um oráculo de parada, e para isso, é claro que preciso ter uma noção formal de possível não terminação e provas de interrupção. ir junto com ele dentro de uma estrutura teórica do tipo.

Como uma das principais aplicações da Teoria dos Tipos nas formalizações tem sido o estudo de linguagens de programação e computação em geral, muito se pensou em maneiras de representar programas possivelmente não termináveis.

Não farei uma pesquisa completa aqui, mas tentarei dar dicas sobre os principais impulsos de diferentes direções.

• A abordagem "relacional": você pode definir seus programas hipotéticos como as relações dizer, que detém sse é definida em e . Este é geralmente o que é feito com a T-predicado Kleene . Isso funciona tão bem nas formalizações da teoria dos tipos quanto na lógica clássica (embora é claro que você não pode provar ).f x f ( x ) = y ∀ x ( ∃ y , F x y ) ∨ ( ¬ ∃ y , F x y $F\ x\ y$$f$$x$$f(x)=y$$\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$

  Uma maneira mais sofisticada de fazer isso é o método "Bove-Capretta" (consulte Modelando a recursão na teoria dos tipos , que para cada função recursiva, define um "predicado acessível" que codifica o fato de que uma determinada computação é finita. A definição da função leva um argumento extra que comprova que as entradas fornecidas são acessíveis.Para definir a função sem esse predicado extra, você precisa provar que todas as combinações possíveis de entradas são acessíveis.

• A abordagem "coindutora": essa é possivelmente a abordagem mais explorada e a que os comentários de Andrej se referem. Um cálculo do tipo é definido como o tipo indutivo (a partir do link de Andrej , por Capretta, Altenkirch & Uustalu:$A$

  codata Delay A =
  | Now : A -> Delay A
  | Later (Delay A)
  

  Isso codifica um fluxo possivelmente infinito de Latertokens ("ticks" de computação) que pode terminar com um resultado Now a. A não rescisão é equivalente a ser bisimilar com o programa

  loop = O loop e a terminação posteriores podem ser definidos por um predicado indutivo sobre Delay A:

  data Terminates : Data A -> Prop =
  | Term_now : forall x, Terminates (Now x)
  | Term_later : forall d, Terminates d -> Terminates (Later d)
  

  Eu acho que os agda-istas têm muito a dizer sobre isso, que eles chamam de mônada de parcialidade (veja, por exemplo, Danielsson ).

• A abordagem da "teoria dos tipos parciais" : isso é um pouco mais experimental (a teoria ainda está sendo elaborada), mas existem algumas teorias de tipos que estão sendo desenvolvidas para lidar com o fato de que existem essencialmente dois tipos de funções que queremos escreva na teoria dos tipos: os termos da prova e os programas. É difícil obter uma teoria razoável dessas coisas (e manter a consistência da teoria), mas uma tentativa séria é feita aqui por Casinghino et al. , E um esforço semelhante por Kimmel et al .

Tenho certeza de que existem outras abordagens das quais não conheço e ficaria feliz se alguém quiser concluir esta lista.

Provavelmente, devo observar que adicionar um oráculo de terminação a uma teoria de tipo (consistente) é muito parecido com adicionar um oráculo de verdade para sentenças , com conseqüências relativamente bem compreendidas.$\Pi^0_1$

Existem outras interações bastante proveitosas entre a teoria dos tipos e a teoria da complexidade, geralmente sob a égide da complexidade computacional implícita .