Résumé:
Une démonstration mathématique est generalement constituée de
raisonnements ingénieux et de calculs mécanisables. Or les systèmes de
développement de preuves actuels (Coq, Lego, Nuprl, HOL, etc.) ont un
mécanisme de calcul assez rudimentaire. Bien qu'ils permettent d'exprimer
de très nombreuses fonctions (toute fonction dont l'existence est
prouvable en arithmétique intuitionniste d'ordre supérieur), les
définitions peuvent être malaisées et parfois inefficaces (celles-ci
doivent suivre un schéma très restrictif semblable à la récursion
primitive). Ces systèmes ne permettent donc pas de définir fonctions et
prédicats de la manière que l'on veut, ce qui les rend difficiles à
utiliser par des non-spécialistes et limite l'aspect ``calcul'': des
propositions qui pourraient être prouvées de manière automatique, par un
simple calcul, nécessitent des déductions compliquées. Inversement, avec
une notion de calcul plus riche mais telle que l'égalité de deux termes
soit décidable, il n'est pas nécessaire de mémoriser les étapes de calcul.
Les preuves se trouvent ainsi réduites aux ``raisonnements''. Or,
actuellement, la taille des preuves est un problème critique dans les
systèmes de développement de preuves.
Les définitions à l'aide de règles de récriture sont à la fois plus
générales, plus aisées et peuvent être plus efficaces. Mais considérer des
fonctions ou des prédicats définis par un ensemble de règles de récriture
a priori quelconques pose un problème essentiel: peut-on vérifier si une
preuve est correcte ? C'est la ``décidabilité du typage''.
Dans cet expose, je presenterais l'interet d'etendre le Calcul des
Constructions avec de la recriture aussi bien au niveau objet qu'au niveau
predicat. Ensuite, je donnerais des conditions generales assurant la
decidabilite du typage. Ces conditions s'appliquent aussi bien au Calcul
des Constructions Inductives avec elimination forte a la base du systeme
Coq qu'a la Deduction Naturelle Modulo.
Retour au sommaire / Back to schedule