Quelle est la relation et la différence entre le calcul des constructions inductives et la théorie des types intuitionnistes?

25

Comme indiqué dans le titre, je me demande quelle relation et différence entre CIC et ITT. Quelqu'un pourrait-il m'expliquer ou m'indiquer une littérature qui compare ces deux systèmes? Merci.

journée
la source
3
Pour moi, ITT signifie "Théorie du type intuitionniste", ce qui pourrait signifier un certain nombre de choses. En particulier, il existe un grand nombre de variations subtiles par rapport aux descriptions originales de Martin-Lof, et cela aiderait la discussion si vous donniez la référence qui décrit l'ITT auquel vous pensez. La réponse courte est la suivante: l'ITT au sens Martin-Lof sans univers est une sous-théorie du CoC. En présence d'univers mais pas de types inductifs, vous pouvez écraser tous les univers dans le seul univers imprédicatif du CoC. Avec de grands types inductifs et une grande élimination, les choses sont plus complexes.
cody
1
Ah et une bonne discussion de certaines de ces choses peut être trouvée dans Geuvers: cs.ru.nl/~herman/PUBS/CC_CHiso.ps.gz
cody
Merci pour les commentaires et l'article lié, cody. Il ressemble à ce que je cherche.
jour
1
Une version pdf du document mentionné par @cody: cs.ru.nl/~herman/PUBS/CC_CHiso.pdf
Steven Shaw

Réponses:

24

J'ai déjà répondu un peu, mais je vais essayer de donner un aperçu plus détaillé de l'horizon théorique type, si vous voulez.

Je suis un peu flou sur les détails historiques, donc les lecteurs plus avertis devront me pardonner (et me corriger!). L'histoire de base est que Curry avait découvert la correspondance de base entre les combinateurs simplement typés (ou -terms) et la logique propositionnelle, qui a été étendue par Howard pour couvrir la logique du premier ordre, et l'IIRC découvert de manière indépendante par de Bruijn dans des enquêtes autour de la système Automath extrêmement influent .λ

Le système Automath était un raffinement de la théorie des types simples de Church qui était elle-même une simplification dramatique de la théorie des types de Russel et Whitehead avec des univers et l' axiome de la réductibilité . C'était un terrain logique relativement bien connu dans les années 1960.

Cependant, donner un système fondamental cohérent, simple, qui englobait à la fois les systèmes de preuve et de terme était encore une question très ouverte en 1970, et une première réponse a été donnée par Per Martin-Löf. Il donne un aperçu très philosophique de la signification des constantes logiques et de la justification des lois logiques . Il raisonne qu'en logique et en mathématiques, le sens des constructions peut être donné en examinant les règles d'introduction qui permettent la formation de ces constructions en tant que jugements, par exemple pour la conjonction

UNEBUNEB

Détermine la règle d'élimination correspondante. Il a ensuite donné un système fondamental très puissant basé sur de tels jugements, lui permettant de donner un système fondamental similaire à Automath utilisant très peu de constructions syntaxiques. Girard a trouvé que ce système était contradictoire, incitant Martin-Löf à adopter des univers prédicatifs "à la Russel" , limitant sévèrement l'expressivité de la théorie (en supprimant efficacement l'axiome de réductibilité) et la rendant légèrement plus complexe (mais avait l'avantage de le rendant cohérent).

Les constructions élégantes permettant la définition des symboles logiques ne fonctionnaient plus cependant, ce qui a incité ML à les présenter sous une forme différente, en tant que familles définies par induction . C'est une idée très puissante, car elle permet de tout définir, de l'égalité de jugement et des opérateurs logiques aux nombres naturels et aux types de données fonctionnels tels qu'ils apparaissent en informatique. Notez que chaque famille que nous ajoutons s'apparente à l'ajout d'un certain nombre d'axiomes, qui doivent être justifiés comme cohérents dans chaque cas. Ce système (types dépendants + univers + familles inductives) est généralement appelé ITT .

Cependant, il y avait une frustration persistante, car le système fondamental puissant mais simple était incohérent, et le système résultant était plus complexe et quelque peu faible (dans le sens où il était difficile de développer une grande partie du cadre mathématique moderne). Entrez Thierry Coquand, qui, avec son superviseur Gerard Huet, a présenté le calcul des constructions (CoC) , qui a principalement résolu ces problèmes: une approche unifiée des preuves et des types de données, un système fondamental puissant (imprédicatif) et la capacité de définir des «constructions "de la variété logique ou mathématique. Cela a finalement évolué vers une mise en œuvre réelle d'un système conçu comme une alternative moderne à Automath, aboutissant au système Coq que nous connaissons et aimons.

Je suggère fortement cet article de base sur le CoC, car Thierry en sait beaucoup sur le développement historique de la théorie des types, et l'explique probablement beaucoup mieux que moi. Vous pouvez également consulter son article sur la théorie des types, bien qu'il ne le fasse pas expliquer la correspondance CH en détail.

cody
la source
5
Il convient de noter que le CoC, malgré toute la puissance de sa construction imprédivative des types de données, ne peut pas prouver l'induction, et les auteurs ultérieurs (par exemple Paulin-Mohring) ont étendu le CoC avec des constructions inductives à la Martin-Löf, donnant le calcul des constructions inductives, qui est utilisé dans Coq.
Martin Berger
1
Oui, j'ai oublié de commenter cela. Cependant, l'ajout de l'axiome simple suffit (pour un encodage approprié des concepts impliqués). 10
cody
1
Des types inductifs ont été ajoutés pour améliorer le comportement de calcul en plus de cela.
cody
1
Eh bien, la fonction précédente ne peut pas être calculée en temps constant en utilisant la définition imprédicative des nombres naturels. Voir par exemple ici ou ici .
cody
1
Oui, les chiffres de l'Église, mais un résultat similaire va tenir pour les types de données plus sensibles comme les listes chaînées. L'exemple de la machine de Turing tend à suggérer que les machines de Turing ne sont pas non plus bien adaptées au calcul pratique! :)
cody