O que torna uma linguagem (e seu sistema de tipos) capaz de provar teoremas sobre seus próprios termos?

12

Recentemente, tentei implementar o Cedille-Core de Aaron , uma linguagem de programação minimalista capaz de provar teoremas matemáticos sobre seus próprios termos. Eu também provei a indução para tipos de dados codificados em λ, o que deixou mais claro por que suas extensões seriam necessárias.

Menos ainda, ainda me pergunto de onde vieram essas extensões. Por que eles são o que são? O que os justifica? Eu sei, por exemplo, que algumas extensões, como a recursão, arruinam o idioma como um sistema de provas. Se eu decidisse também estender o CoC com outras primitivas, como justificaria? Entendo que é necessária uma prova de normalização, mas isso não prova que esses primitivos "façam sentido".

Em resumo, o que especificamente qualifica uma linguagem (e seu sistema de tipos) como um sistema capaz de provar teoremas sobre seus próprios termos?

type-theory functional-programming constructive-mathematics MaiaVictor
fonte
Eu li um blog que estava relacionado a essa pergunta, mas não consigo encontrá-lo agora :( Ele continha a frase "O sistema T é suficiente!" Ou algo parecido e falava sobre sistemas de tipos dependentes.
Labbekak
2
Encontrou: queuea9.wordpress.com/2010/01/17/… Na verdade, foi escrito por Aaron Stump, para que você já saiba.
Labbekak
A recursão desprotegida "arruina" o idioma como sistema de prova, a recursão guardada não. Para provar que as primitivas fazem sentido, eu diria que você constrói um modelo. E para provar teoremas sobre seus próprios termos, ele precisa de um tipo de isomorfismo de Curry-Howard e um tipo dependente para que as coisas que você prova (tipos) possam falar sobre seus termos.
xavierm02

Respostas:

5

[A autopublicidade segue, mas acho que isso é relevante.]

Existem várias abordagens possíveis para essas perguntas. Uma das maneiras (que eu explorei durante minha tese de doutorado no contexto de uma linguagem semelhante ao ML) é estender o sistema de tipos com uma camada de primeira ordem, para que os termos da linguagem possam ser manipulados como objetos da lógica subjacente . Obviamente, você também precisa incluir alguns predicados para que haja algo a observar. No caso do meu sistema, esses predicados são equivalências de termos. Em particular, se e são termos da linguagem, então o tipo é habitado apenas se e são de fato (observacionalmente) equivalentes. Você pode usar quantificadores de primeira ordem para codificar propriedades comotut≡utu∀v,(λx.x)v≡v em tipos, e eles são provados através da construção de programas que os habitam.

Obviamente, você também pode assumir equivalências e existem várias formas diferentes de quantificadores (digitados / não tipificados, universais / existenciais). Esse mecanismo pode ser usado para raciocinar sobre qualquer programa (eles não precisam ser provados como encerrados ou mesmo digitados). A única restrição é que os programas usados ​​como provas devem ser provados como encerrados pelo sistema (recursão geral arbitrária leva a inconsistência).

Aqui estão algumas referências, se você quiser verificar isso:

Rodolphe Lepigre
fonte