Action Concertée Incitative
Nouvelles Interfaces des Mathématiques
Projet Mao -- Mathématiques assistées par ordinateur
Nos méthodes et nos choix sont dictés par les expériences que nous avons faites ces dernières années. En particulier, durant l'année écoulée, nous avons implémenté, et même de plusieurs façons, les posets, monoïdes, groupes, anneaux, modules, algèbres sur un anneau, catégories, foncteurs, transformations naturelles, limites et colimites, plongement de Yoneda, topologies de Grothendieck et faisceaux sur un site, avec les principales constructions correspondantes par exemple le radical, le produit tensoriel, la localisation ou encore la catégorie des catégories.
Ces expériences nous ont conduits à deux constats essentiels que nous expliquons ci-dessous.
La démarche naturelle, qui consiste à exploiter librement et sans contraintes les possibilités d'expression offertes par Coq conduit à une impasse: certains mécanismes sophistiqués offert par Coq (plus précisément les types dépendants et les records) doivent n'être utilisés qu'avec le plus grand discernement. Plus généralement nous avons compris qu'il convient d'élaborer un style de preuve qui concilie en quelque sorte le mode de pensée du mathématicien et celui de la machine. A ce stade de notre travail, nous avons mis au point deux styles de preuve que nous allons maintenant décrire rapidement.
Notre premier style repose sur une version axiomatique de la théorie
des ensembles combinée à la théorie des types de Coq. On
commence avec l'introduction d'une classe 
d'ensembles (
)
et un axiome déclarant que chaque type (membre de ) est un
ensemble dont les éléments (ses termes) sont aussi des
ensembles. On introduit aussi des axiomes de choix, d'extensionalité
et de remplacement. Ceci permet l'intégration des types inductifs
avec la logique non-typée et classique de la théorie des
ensembles. C'est dans ce cadre qu'on met en place un mécanisme de
notations pour les objets mathématiques usuels. Ce mécanisme est
conçu pour préserver dans une certaine mesure l'héritage auquel
les mathématiciens sont légitîmement attachés (un anneau est un groupe). Nous avons déjà implémenté dans ce style les
ensembles ordonnés, les ordinaux et cardinaux et prouvé le lemme
de Zorn, l'existence d'un bon ordre sur tout ensemble, le principe de
récurrence transfinie, et le théorème de
Bernstein-Cantor-Schroeder. Nous sommes maintenant prêts à
implémenter des objets mathématiques plus orientés vers la
géométrie algébrique.
Notre second style privilégie deux mots-clefs, typoïde et monade, et prend comme point de départ le constat expérimental suivant: l'enchevêtrement des preuves et des calculs constitue un obstacle majeur à la simplicité des preuves formelles. Après avoir dans un premier temps tiré des conclusions molles de cette observation, nous sommes finalement passés à une conclusion plus radicale. Pour séparer efficacement les calculs des preuves, nous implémentons les ensembles comme des typoïdes (nous préférons ce mot au terme classique, PER, que nous trouvons peu euphonique): un typoïde est un ensemble (il faut penser à un ensemble de formules) muni d'une relation d'équivalence partielle (qui dit quand deux formules sont égales, et donc aussi quand une formule est bien formée, c'est-à-dire égale à elle-même). Ces typoïdes assurent parfaitement la tâche de séparation entre les calculs, qui concernent les formules, et les preuves, qui concernent la relation d'égalité. De plus ils fournissent une solution confortable et uniforme à deux problèmes que Coq ne sait pas bien gérer, celui des sous-types et celui des types quotients. A ce propos, signalons que notre solution prend le contre-pied de la thèse d'Hoffmann, qui trouvait la justification de son axiome du quotient en construisant un modèle dans les typoïdes: nous nous passons de cet axiome du quotient en travaillant directement avec les typoïdes.
C'est pour l'ensemble des formules que nous mettons systématiquement en avant les structures de monade. L'étroite relation entre monade et calcul est bien connue notamment depuis les travaux de Moggi. Dans le calcul des constructions inductives, les manipulations qu'on souhaite faire sur les expressions algébriques constituent une monade, et nous exploitons systématiquement cette structure, qui permet en particulier de programmer facilement des tactiques fondées sur le principe de la réflexion introduit par Samuel Boutin. Nous avons ainsi déjà implémenté la monade pour les groupes et les groupes abéliens et les tactiques correspondantes. Nous projetons maintenant de programmer les autres structures de la géométrie algébrique sur ce modèle.
Nous espérons que les deux styles que nous sommes en train de mettre au point sont complémentaires: les tactiques sont certainement plus faciles à programmer dans le second style, tandis que les démonstrations pourraient être plus faciles dans le premier.
(dernière mise à jour du site : 14 décembre 2004)