Qu'est-ce qui rend un langage (et son système de types) capable de prouver des théorèmes sur ses propres termes?

12

J'ai récemment tenté d'implémenter le Cedille-Core d' Aaron , un langage de programmation minimaliste capable de prouver des théorèmes mathématiques sur ses propres termes. J'ai également prouvé l'induction de types de données codés λ dessus, ce qui a permis de comprendre pourquoi ses extensions seraient nécessaires.

Nether Nether, je me demande toujours d'où viennent ces extensions. Pourquoi sont-ils ce qu'ils sont? Qu'est-ce qui les justifie? Je sais, par exemple, que certaines extensions, comme la récursivité, ruinent le langage comme système de preuves. Si je décidais d'étendre également CoC avec d'autres primitives, comment pourrais-je justifier? Je comprends qu'une preuve de normalisation est nécessaire, mais cela ne prouve pas que ces primitives "ont du sens".

Bref, qu'est-ce qui qualifie précisément une langue (et son système de types) comme un système capable de prouver des théorèmes sur ses propres termes?

type-theory functional-programming constructive-mathematics MaiaVictor
la source
J'ai lu un blog qui était lié à cette question, mais je ne peux pas le trouver maintenant :( Il contenait la phrase "Le système T suffit!" Ou quelque chose comme ça et il parlait de systèmes de type dépendants.
Labbekak
2
Je l'ai trouvé: queueea9.wordpress.com/2010/01/17/… Il est en fait écrit par Aaron Stump donc vous le savez peut-être déjà.
Labbekak
La récursion non gardée "ruine" la langue comme système de preuve, la récursion gardée ne le fait pas. Pour prouver que les primitives ont du sens, je dirais que vous construisez un modèle. Et pour prouver les théorèmes sur ses propres termes, il a besoin d'une sorte d'isomorphisme de Curry-Howard et d'un type dépendant pour que les choses que vous prouvez (types) puissent parler de vos termes.
xavierm02

Réponses:

5

[L'auto-publicité suit, mais je pense que cela est pertinent.]

tut≡utu∀v,(λx.x)v≡v

Bien sûr, vous pouvez également supposer des équivalences, et il existe plusieurs formes différentes de quantificateurs (typés / non typés, universels / existentiels). Ce mécanisme peut être utilisé pour raisonner sur n'importe quel programme (il n'est pas nécessaire de prouver qu'il se termine ou même de le taper). La seule contrainte est que les programmes utilisés comme preuves doivent être prouvés se terminant par le système (une récursion générale arbitraire entraîne une incohérence).

Voici quelques références si vous souhaitez vérifier cela:

Rodolphe Lepigre
la source