Cloisonnement des contenus calculatoire et logique du filtrage
dépendant en théorie des types et application aux coupures commutatives
Encadrant: Hugo Herbelin (INRIA-Futurs -- LIX)
Lieu: PPS, annexe parisienne de l'INRIA, 23 avenue d'Italie, Paris
Le filtrage dépendant est une des constructions les plus expressives
des théories des types modernes (typiquement le « logical framework »
de Martin-Löf qu'implémente Agda ou le Calcul des Constructions
Inductives qu'implémente Coq). Ainsi et par exemple, le filtrage
dépendant permet tout à la fois de « construire » (sans axiome) des
preuves calculatoires d'énoncés logiques tels que la discrimination
des entiers (0≠1), l'induction de Peano (∀n P(0) → (∀m P(m)→P(m+1)) →
P(n)) ou la substitutivité de l'égalité (t=u → ∀P P(t)→P(u)), que de
construire de manière naturelle (à la ML) des fonctions par cas, sans
compter toutes les possibilités de combinaisons permettant, domaine en
essor, la programmation à type dépendant, c'est-à-dire la
programmation sur des structures de données équipées d'invariants
forts tels que je suis un arbre dont la taille des sous-arbres est
équilibrée, je suis une paire d'entiers dont la seconde composante est
strictement plus grande que la première, etc.
Pourtant, le filtrage à types dépendants figurent parmi les
constructions logico-calculatoires parmi les moins biens étudiées à ce
jour. Si l'on regarde Agda, on constate que c'est à ce jour le système
qui implémente la forme la plus épurée de filtrage dépendant en termes
de séparation entre la partie calculatoire et la partie logique, mais
cette capacité à séparer le côté logique est limitée à une classe de
propriétés pour laquelle existe une théorie de l'unification premier
ordre. De son côté, Coq fournit des primitives de haut niveau pour
offrir à l'utilisateur une vision séparée des aspects logiques et
calculatoires des programmes à types dépendants (les commandes
« Program », « Function » et « Equations ») mais dans la pratique, les
programmes obtenus restent encombrés d'informations logiques freinant
leur évaluation.
Le but de ce stage est d'implanter un nouveau modèle de filtrage
dépendant pour le Calcul des Constructions Inductives qui sépare
explitement les parties logiques et calculatoires d'une expression de
filtrage, permettant ainsi à l'utilisateur d'utiliser des contraintes
de typage dépendant arbitrairement complexes sans affecter
l'efficacité et la pureté du comportement calculatoire sous-jacent.
Un des aspects de ce nouveau modèle de filtrage (dont une des briques
de base est la conversion de contextes de la forme « x:A, x=t » pour t
ne contenant pas x en contextes de la forme « x:=t:A ») est aussi
qu'il se prête bien à l'ajout de coupures dépendantes (règles de la
forme « E[case t of ... ⇒ u] → case t of ... ⇒ E[u] »), offrant par là
de nouvelles perspectives dans l'automatisation du raisonnement
égalitaire dans le Calcul des Constructions Inductives.
Bibliographie
Bruno Barras, Pierre Corbineau, Hugo Herbelin, Benjamin Grégoire,
Jorge-Luis Sacchini: A new elimination rule for the Calculus of
Inductive Constructions. Types 2008.
Healfdene Goguen, Conor McBride, James McKinna: Eliminating Dependent
Pattern Matching. Essays Dedicated to Joseph A. Goguen, 2006.
Thorsten Altenkirch, Nicolas Oury: Pi-Sigma. Manuscrit disponible à
l'adresse www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf.
Ulf Norell: Towards a practical programming language based on
dependent type theory. PhD, 2007.
Matthieu Sozeau: Equations. Manuscrit disponible à l'adresse
github.com/mattam82/Coq-Equations.git/paper/ITP.