Si les symboles sont mal affichés sur votre navigateur voyez cette version: en texte pur.

Introduction

L’étude des fondements des mathématiques a-t-elle une autre utilité qu’occuper l’esprit de quelques mathématiciens philosophes? Autant l’intérêt pratique des mathématiques est une évidence depuis des millénaires, autant celui de la méta-mathématique n’est quant à lui apparu que récemment. Quel besoin en effet l’ingénieur a-t-il de se soucier de la justification mathématique des différentes théories qu’il utilise? La seule chose importante est que ces outils mathématiques lui permettent de construire des ponts solides. « Pourquoi n’ai-je jamais pu tirer deux déductions contradictoires dans cette théorie? » est une question concernant plus le mathématicien logicien que l’ingénieur, même si une contradiction manifeste gênerait finalement plus le second que le premier.

Loin de nous l’idée de critiquer un tel point de vue: ce n’est pas avec de la logique méta-mathématique que l’on conçoit un pont!

Cependant il est des conceptions humaines plus récentes dont la fabrication requiert des méthodes frôlant de si près la démonstration mathématique¹ que la question méta-mathématique est à son tour devenue un enjeu économique et donc, paradoxalement, pratique. Il s’agit bien entendu des conceptions informatiques. Plus généralement nous parlons des ouvrages mettant en œuvre des procédures automatiques; l’électronique est donc par exemple aussi concernée.

Ne minimisons pas les difficultés qu’affronte le programmeur ou l’électronicien: les processeurs et logiciels actuels sont d’une complexité qu’aucun ingénieur ne risquerait sur un chantier! On peut même s’effrayer de la confiance placée dans ces programmes censés effectuer des tâches aussi critiques que piloter un train ou une fusée. Nombreux sont d’ailleurs les exemples où cette confiance s’est soldée par de coûteux ou tragiques accidents.

Comment alors s’assurer de manière rigoureuse de la correction d’un programme? De nombreux éléments de réponse ont été donnés à cette question éminemment pratique, mais l’un des plus élégants est probablement l’isomorphisme de Curry-Howard [], qui constate en substance qu’écrire un programme et faire une démonstration procèdent fondamentalement de la même activité. Écrire un programme correct revient donc à écrire une démonstration juste. Or c’est là la préoccupation du logicien: qu’est-ce qu’une démonstration? Comment en démontrer la justesse? Quelles théories sont cohérentes et peuvent donc servir de base à des démonstrations?

Cette préoccupation méta-mathématique s’est donc subrepticement étendue au-delà de la sphère du logicien pour pénétrer celle de l’ingénieur. Les buts de la recherche ont changé lors de ce transfert. Dans notre cas, là où il s’agissait de prouver ou de réfuter la cohérence de telle ou telle théorie, il faut maintenant démontrer que le programme de 100 000 lignes de code pilotant un métro ne provoquera pas d’accident. Un changement pour le moins radical! Devant cette constatation, les observations suivantes s’imposent:

1. Sans outil automatique (informatique) puissant pour l’aider à concevoir ses démonstrations, l’ingénieur-logicien ne viendra pas à bout de ce travail et commettra certainement des erreurs ;
2. La question de cohérence des théories utilisées reste entière, elle est même exacerbée par l’utilisation d’un outil automatique ;
3. L’outil devra être lui-même vérifié préalablement pour que le travail effectué avec son aide soit réellement convaincant.

On voit ici apparaître les grandes lignes d’une branche de la recherche se situant à la frontière de la logique et de l’informatique. Elle consiste à concevoir les outils, théoriques et pratiques, qui assisteront l’utilisateur de manière rigoureuse lors des démonstrations mathématiques. L’utilisateur peut être l’ingénieur-logicien dont nous avons parlé, mais aussi l’étudiant dans le cadre de l’enseignement des mathématiques et on peut même espérer – même s’il reste un long chemin à parcourir – qu’à terme les mathématiciens utiliseront de tels outils pour les assister dans leur travail. Les logiciels conçus dans le cadre de cette recherche s’appellent «outil d’aide à la démonstration», «assistant de preuve»... En anglais le terme «theorem prover» semble s’imposer. Citons quelques noms de tels programmes: l’atelier B, PVS, Coq, Isabelle, NUPrl... Précisons que ces outils, bien qu’encore inadaptés à des développements de très grande taille, sont utilisés aujourd’hui dans l’industrie.

Le début de cette thèse (parties ?? et ??) s’inscrit dans l’effort actuel de conception et d’amélioration de ces outils et propose une extension du calcul des constructions inductives (CCI ou CIC), le formalisme sous-jacent du système Coq []. Cette extension a pour but de permettre un traitement plus agréable et plus puissant de la notion de quotient, très utilisée en mathématiques. Pour comprendre ce qui se cache derrière les mots «formalisme sous-jacent», il est nécessaire d’introduire les quelques concepts fondamentaux de la logique formelle, c’est l’objet de la fin de cette introduction. Le néophyte intéressé pourra lire l’ouvrage très pédagogique de Gilles Dowek [], duquel sont tirés quelques faits historiques cités dans la suite.

La dernière partie présente le développement dans l’assistant Coq d’une preuve d’algorithme auto-stabilisant. Un algorithme auto-stabilisant est un algorithme s’exécutant sur un réseau² et ayant la propriété suivante: à partir d’une configuration initiale quelconque du réseau, l’algorithme fait revenir celui-ci dans une configuration correcte au bout d’un temps fini et ne quitte plus les configurations correctes ensuite. On entend par configuration correcte une configuration correspondant à un déroulement valide de l’algorithme.

La méta-mathématique

L’étude du raisonnement remonte probablement plus loin, mais les philosophes grecs sont les premiers à nous en avoir laissé trace. Aristote, face à l’évidente observation qu’il existe des raisonnements faux, s’interroge sur la nature et les mécanismes de la déduction. Il constate déjà que pour déduire, il faut en premier lieu admettre des faits préalables, comme par exemple dans le raisonnement suivant: "Si on admet que tous les hommes sont mortels et que les Grecs sont des hommes, alors les Grecs sont mortels". Cette pré-admission mène à la notion de théorie.

Théorie

Le mot théorie désigne un ensemble de faits admis³, appelés axiomes. Ici les deux axiomes "tous les hommes sont mortels" et "les Grecs sont des hommes" permettent de déduire que les Grecs sont mortels.

Au risque d’enfoncer une porte ouverte, précisons qu’il n’est absolument pas correct d’en déduire que les Grecs sont mortels! On a montré qu’ils sont mortels SI on admet les deux axiomes, rien de moins, rien de plus. On reformule cet énoncé de manière plus logicienne en: «   "les Grecs sont mortels" est démontrable dans la théorie { "tous les hommes sont mortels", "les Grecs sont des hommes" }   »⁴. On peut également exprimer ce raisonnement lui-même sous la forme d’une propriété: "(tous les hommes sont mortels ET les Grecs sont des hommes) IMPLIQUE que les Grecs sont mortels". Cette propriété est elle-même démontrable à partir d’un ensemble d’axiomes vide: c’est une tautologie. On remarque d’ailleurs que comme dans toute tautologie, les propriétés élémentaires peuvent être remplacées par n’importe quelles autres propriétés, par exemple: "(tous les éléphants sont bleus et les poissons sont des éléphants) implique que les poissons sont bleus" est en fait la même tautologie, elle est tout aussi correcte.

Déduction

Pourtant, là encore quelque chose a été admis: la notion de raisonnement correct, autrement dit le mécanisme de déduction. En effet, sans un mécanisme pour reconnaître un raisonnement correct, comment différencier une déduction fausse d’une déduction valide? De la même manière qu’en cinétique la notion de vitesse n’a de sens qu’à l’intérieur d’un référentiel, une proposition en logique n’est donc démontrée qu’à l’intérieur d’une théorie (éventuellement vide pour les tautologies) et d’un système de déduction permettant de déduire des propriétés à partir des axiomes de la théorie. Si ce dernier est vide, alors rien n’est démontrable, pas même les axiomes. Un abus de langage autorise parfois à appeler théorie ce couple <théorie,système>.

Un système est aujourd’hui généralement présenté sous la forme d’un ensemble de règles formelles. Par exemple une règle communément admise dans tout système logique est la suivante:

On lit une telle règle de la manière suivante:

• si les prémisses (les propriétés énoncées au-dessus de la barre horizontale, ici il n’y en a pas) sont démontrables,
• alors la conclusion (en dessous de la barre) l’est aussi.

On voit bien ici le mécanisme de déduction défini: la règle permet de démontrer une propriété A à condition qu’elle soit un axiome. D’autres exemples classiques de règles de déduction sont le modus ponens et la règle du "et" logique:

qui se lisent respectivement: "si A est démontrable et si A implique B (noté A => B) est démontrable, alors B est démontrable", et "si A et B sont chacun démontrable, alors A et B (notée A AND B) est démontrable". Précisons ici que nous ne sommes pas en train d’énoncer une propriété mais bien une définition. En écrivant un ensemble de règles de déduction, on donne son sens au mot "démontrable" dans le contexte que nous avons choisi. Une démonstration se présente sous la forme d’un ensemble d’instances de règles imbriquées, formant un arbre. Par exemple, voici la preuve de a < c dans la théorie constituée des trois axiomes { a < b, b < c, (a < b AND b < c) => a < c }:

On voit que: 1) Toutes les feuilles de l’arbre contiennent des axiomes et 2) Les règles sont correctement appliquées. C’est avec ces deux critères facilement vérifiables qu’on reconnaît une déduction complète et valide. Loin d’être anodin, le besoin d’un mécanisme simple pour la vérification est au contraire primordial. En effet, si la vérification de la validité d’un raisonnement nécessite elle-même un raisonnement, alors il faut aussi s’assurer de la validité de ce dernier, ce qui demandera encore un raisonnement, etc. En fait, depuis l’apparition de la notion de machine programmable (notamment la célèbre machine théorique de Turing) et l’avènement des ordinateurs et de leur capacité à traiter des données symboliques, on a pu à la fois relâcher et préciser ce principe: il suffit que la vérification soit décidable⁵, c’est-à-dire qu’il soit possible d’écrire un programme (au sens programme de machine de Turing) capable de l’effectuer.

Le travail des logiciens

Le travail des logiciens consiste à définir des systèmes de déduction et des théories, et d’en étudier:

• L’expressivité, c’est-à-dire la quantité de propriétés exprimables et/ou démontrables à partir des axiomes de la théorie en utilisant les règles du système de déduction. Plus une théorie est expressive, plus elle permettra d’étudier de problèmes.
• La cohérence, c’est-à-dire l’impossibilité de démontrer une propriété et son contraire à partir des axiomes de la théorie en utilisant les règles du système de déduction (une telle propriété est appelée paradoxe de la théorie). Si c’était possible, la théorie, dite contradictoire, deviendrait inintéressante puisque permettant de démontrer n’importe quelle propriété. Un problème sur lequel nous reviendrons plus loin est que pour prouver la cohérence d’une théorie, il faut nécessairement se placer dans une autre théorie.

On s’est vite aperçu que plus une théorie est expressive, plus il est délicat de se convaincre puis de démontrer qu’elle est cohérente. L’exemple le plus célèbre de cette difficulté nous vient des théories des ensembles de Frege et Cantor, prouvées contradictoires par Cesare Burali-Forti puis Bertrand Russel en 1897 et 1902. Russel a pour cela exhibé la propriété suivante: "L’ensemble des ensembles qui ne se contiennent pas eux-mêmes se contient lui-même", qui est un paradoxe dans ces théories. Redéfinies par Ernst Zermelo en 1908 et par Alfred North Whithead et Russel en 1910 de manière à rendre cet énoncé impossible à formuler, ces théories n’ont finalement pas vu leur avenir remis en question et servent toujours de base aux mathématiques actuelles.

"Le" siècle de la logique

De nombreuses découvertes fondamentales, et parfois surprenantes, ont été faites dans le domaine de la logique au cours du vingtième siècle. Nous en donnons ici une petite chronologie afin de présenter brièvement les évolutions majeures de la logique récente.

1900

Gottlob Frege pose les bases de la logique formelle []; son approche rigoureuse de la notion de preuve l’amène à définir les notions de formule et de propriété comme elles le sont encore aujourd’hui. Frege est à l’origine de la notion de système de preuve évoquée à la section précédente.

1900

La théorie naïve des ensembles est prouvée contradictoire au tout début du siècle, comme nous l’avons dit plus haut, ainsi que la théorie logique de Frege. C’est la première fois que le problème de la cohérence et sa difficulté se posent de manière si directe à l’ensemble des mathématiciens. Nous avons vu que ce problème n’a pas vraiment eu de conséquence et qu’il a été corrigé quelques années plus tard.

En fait plusieurs solutions ont été proposées, dont les suivantes:

• Russel propose sa théorie des types⁶, une version de la théorie des ensembles enrichie d’une notion de hiérarchie permettant d’éviter le paradoxe en cloisonnant les différents niveaux du discours.
• Luitzen Brouwer propose une vision intuitionniste des mathématiques [], dans laquelle on ne peut prouver l’existence d’un objet qu’en exhibant, sinon l’objet lui-même, au moins un mécanisme pour le construire. L’intuitionnisme est à la base de la théorie des types intuitionniste de Martin-Löf (voir plus bas), qui est considérée aujourd’hui comme la mathématique des concepts décidables. En particulier, cette notion de mécanisme permettant de construire des objets, autrement dit d’algorithme, s’adapte parfaitement aux raisonnements nécessaires à la programmation.
• Ernst Zermelo en 1908 propose une axiomatisation de la théorie des ensembles. Le schéma de compréhension, qui permettait de construire le paradoxe de Russel, y est restreint de manière à le rendre impossible à formuler. Cette théorie, modifiée par Abraham Fraenkel, ZF, sert de base à la plupart des développements mathématiques actuels.

1931

Gödel surprend la communauté mathématique en démontrant le théorème d’incomplétude [, ], qui stipule que dans toute théorie permettant d’exprimer des propriétés arithmétiques (ce qui est assez minimal), il existe des propriétés qui ne sont pas démontrables et dont la négation n’est pas démontrable non plus. Par la suite, quelques problèmes ouverts bien connus sont prouvés indéterminés, c’est-à-dire appartenant à cette catégorie⁷ (par exemple l’hypothèse du continu est indéterminée dans la théorie des ensembles).

Ce résultat semble contrarier l’intuition mathématique: une propriété peut être soit prouvable, soit réfutable, soit ni l’un ni l’autre.

1931

Gödel ne s’arrête pas là. Puisque toute démonstration doit se faire dans une théorie, une démonstration de cohérence d’une théorie s’appuie nécessairement sur une autre théorie. Une telle démonstration est dite relative: on prouve la cohérence sous la condition que la théorie utilisée pour faire cette preuve est elle-même cohérente. Il est évident que cet exercice n’est complètement convaincant que si cette cascade s’arrête sur une théorie dont on sait qu’elle est cohérente absolument. Gödel élimine tout espoir d’un tel rêve avec son second théorème d’incomplétude: la théorie utilisée est nécessairement plus expressive que la théorie dont on cherche à prouver la cohérence. Par conséquent, on ne pourra pas arrêter la cascade.

Devant cette incapacité de la mathématique à se justifier elle-même, il ne reste plus qu’à faire acte de profession de foi, comme le fait Bourbaki à la fin de son introduction []:

«En résumé, nous croyons que la mathématique est destinée à survivre, et qu’on ne verra jamais les parties essentielles de ce majestueux édifice s’écrouler du fait d’une contradiction soudain manifestée; mais nous ne prétendons pas que cette opinion repose sur autre chose que l’expérience. C’est peu diront certains. Mais voilà vingt-cinq siècles que les mathématiques ont l’habitude de corriger leurs erreurs et d’en voir leur science enrichie, non appauvrie; cela leur donne le droit d’envisager l’avenir avec sérénité.»

1934

Gerhard Gentzen propose le calcul des séquents [, ], un système de déduction exprimant la logique du premier ordre. C’est le premier système dans lequel une propriété est démontrée non pas comme conséquence des axiomes de la théorie de base, mais comme conséquence d’un ensemble de propriétés construit au cours de la déduction. Les règles, toujours sous la forme de fractions comme plus haut, sont constituées de séquents au lieu de formules (propriétés). Un séquent Gamma |- A signifie "A est démontrable sous l’ensemble d’hypothèses Gamma". Par exemple, la règle de déduction du et logique s’exprime de la manière suivante:

On lit cette règle de la manière suivante:

• si sous l’ensemble d’hypothèses Gamma, on peut prouver A,
• et si sous l’ensemble d’hypothèses Gamma, on peut prouver B,
• alors sous l’ensemble d’hypothèses Gamma, on peut prouver "A et B".

On voit que ce système met l’accent sur la notion de conséquence plus que sur celle de vérité. Il permet notamment d’ajouter des hypothèses au cours du raisonnement. Il est clair aujourd’hui que cette vision est plus souple et plus conforme au raisonnement intuitif. Un autre avantage de cette approche est qu’il n’y a plus d’axiome à proprement parler, seulement une règle permettant de déduire une propriété A d’un ensemble d’hypothèses contenant A:

1936

L’opinion de Hilbert, selon laquelle les mécanismes de raisonnement décrits dans les systèmes logiques ne sont que des méthodes de calcul pouvant être automatisées, est réfutée à la fois par Church et Turing. Ils montrent qu’il existe des problèmes qui ne sont pas décidables, c’est-à-dire qu’aucun calcul n’est capable de les résoudre. C’est en particulier le cas du problème consistant à prendre une propriété quelconque P et de répondre à la question «P est-elle démontrable dans la théorie des ensembles⁸?».

Cette découverte décevante nous intéresse particulièrement car elle signifie que le projet d’un programme de démonstrations mathématiques complètement automatique est voué à l’échec.

1930-40

Parallèlement, Alonzo Church développe le lambda-calcul [], un formalisme permettant d’exprimer les fonctions sous la forme d’algorithmes (de termes), accompagné d’une notion de calcul permettant d’évaluer les fonctions lorsqu’elles sont appliquées à leurs arguments. Par exemple, la fonction identité est représentée de la manière suivante:

qui se lit «fonction qui prend un argument auquel on donnera le nom x à l’intérieur de la définition⁹, et qui rend x».

On peut appliquer cette fonction à un terme t:

et le mécanisme de calcul stipule qu’il faut alors faire disparaître l’abstraction et remplacer l’argument abstrait par l’argument réel, ce qui redonne t dans notre cas:

De même le terme lambda z.z+1 est intuitivement la fonction qui rend la valeur de son argument (appelé z à l’intérieur de la définition) incrémentée de un. Il faut ici préciser que 1 et + ne font pas partie du lambda-calcul et doivent être codés de manière assez subtile sous forme de termes. Nous reviendrons sur cet aspect peu pratique pour justifier les dernières évolutions de la théorie des types à la fin de cette section. Nous étudions plus en détail le lambda-calcul et ses versions typées dans la partie ?? de cette thèse.

Cette représentation intentionnelle des fonctions intéresse Church d’une part pour étudier les fonctions et leur comportement calculatoire (cet aspect a donné naissance aux langages de programmation fonctionnels) et d’autre part pour lui adjoindre des règles logiques afin de définir un nouveau système de déduction, appelé "logique d’ordre supérieur" et capable de remplacer la théorie des ensembles¹⁰. L’idée principale est d’utiliser comme brique de base non plus l’ensemble – comme en théorie des ensembles – mais la fonction. Plus explicitement: de même que la définition des entiers (et de tout autre concept) en théorie des ensembles passe par un codage utilisant des ensembles, de même en théorie des types les entiers (dits de Church) sont codés par des fonctions.

La première version de ce système s’avère contradictoire mais les suivantes, grâce à la notion de type associé à un terme, sont prouvées cohérentes (relativement à la théorie des ensembles). Le lambda-calcul et ses avatars servent aujourd’hui de fondement à de nombreux systèmes de preuves actuels, où il est fait un usage intensif de la possibilité de représenter des fonctions intentionnellement (c’est-à-dire en donnant un algorithme pour les calculer). Cet aspect est d’ailleurs souvent présenté comme l’avantage majeur de la théorie des types sur la théorie des ensembles comme fondement des assistants de preuve.

1965

Dag Prawitz propose le système de Déduction naturelle [] (voir également section ?? figure ??), du même genre que celui de Gentzen. On s’aperçoit alors que les règles de ce système sont les mêmes que les règles de typage du lambda-calcul. Cet isomorphisme, dit de Curry-Howard, fait apparaître que les preuves faites dans ce système sont isomorphes aux lambda-termes. De ce fait, un lambda-terme est à la fois un objet mathématique (une fonction de A dans B, un entier...) et une preuve (la preuve que A => B, la preuve que l’ensemble des entiers contient un élément...). De même les types correspondent aux propositions et une proposition (un type) est donc prouvable s’il existe un terme ayant pour type cette proposition. C’est l’idée principale de la théorie des types de Martin-Löf (ci-dessous). Les conséquences de cet isomorphisme sont étonnamment riches et continuent d’être découvertes de nos jours. C’est la pierre angulaire des démonstrateurs tels que Coq ou Lego, qui utilisent les lambda-termes pour représenter les preuves et le typage de ces termes pour vérifier de quoi ils sont la preuve.

1969

Per Martin-Löf décrit la théorie des types intuitionniste [], un système de déduction pour les mathématiques constructives (c’est-à-dire intuitionnistes). Son originalité réside dans l’utilisation de l’isomorphisme de Curry-Howard pour interpréter la notion de démonstration à l’intérieur même du formalisme. Une proposition est interprétée comme un ensemble, dont les éléments représentent les preuves possibles de cette proposition. Une proposition indémontrable est donc représentée par l’ensemble vide et une proposition démontrable par un ensemble non vide.

Remarque: Les systèmes logiques issus de la théorie des types sont en général présentés sous la forme d’un système de typage du type lambda-calcul grâce à l’isomorphisme de Curry-Howard. Nous adopterons aussi cette présentation tout au long de cette thèse.

1970 à nos jours

De nombreux systèmes ont été proposés depuis; un des critères intéressants pour ces systèmes est la réduction des étapes de codage nécessaires pour définir les concepts. On a vu en effet que dans le lambda-calcul et la théorie des types, la définition de notions aussi simples que ℕ passait par des codages lourds et peu adaptés à une implantation sur machine. En plus des critères de cohérence et d’expressivité, le souci grandissant d’une implantation a donc poussé les logiciens vers de nouveaux formalismes plus riches et plus souples que les anciens systèmes jusque là très minimaux. Nous en donnons ici une très courte liste.

• Les systèmes F et F_omega par Jean-Yves Girard (années 1970, []), dont l’expressivité est suffisante (notamment grâce au polymorphisme) pour exprimer à peu près toutes les mathématiques usuelles.
• Le calcul des constructions (CC) par Thierry Coquand et Gérard Huet en 1985 ([]), un système plus puissant mais surtout plus souple, grâce à la possibilité de définir des prédicats de manière directe (à l’aide de types dépendants). Ce calcul est présenté brièvement au chapitre ??.
• Le calcul des constructions inductives (CCI ou CIC) par Thierry Coquand et Christine Paulin-Mohring [, , , ], une extension de CC encore plus souple puisqu’elle permet de définir de nouveaux types, dits inductifs, semblables aux types récursifs des langages de programmation fonctionnels. Ce calcul, dont il est question dans cette thèse, est le système logique sous-jacent de l’assistant de preuve Coq; il sera présenté au chapitre ??.

À chaque nouveau système, des commodités supplémentaires sont introduites dans le formalisme, compliquant son analyse mais facilitant sa mise en œuvre informatique et la création des outils de démonstration.

Le but de cette thèse est

• Premièrement, de prolonger cette course à la souplesse des définitions en présentant une extension du calcul des constructions inductives dans laquelle la notion de structure quotient, qui nécessite un codage axiomatique dans CCI, peut être définie de manière interne.

  La définition de structures non libres, c’est-à-dire dans lesquelles deux termes ayant des constructeurs différents peuvent être égaux, pose en effet différents problèmes de cohérence et de simplicité d’utilisation. En particulier dans CCI il est bien connu que l’ajout d’égalité entre constructeurs d’un type inductif mène à une inconsistance (voir ??). Ces problèmes sont de manière générale liés aux interactions existant entre deux notions qui se combinent difficilement: le calcul et la déduction. La connexion entre ces deux activités, toutes deux indispensables au raisonnement, est faite traditionnellement par les schémas d’élimination (voir ??). Un schéma – ou principe – d’élimination permet de caractériser de manière constructive l’ensemble des termes d’un certain type; ce qui permet à la fois de justifier les démonstrations par récurrence sur ce type et de permettre la définition de fonctions sur ce type (puisqu’on sait sur quels éléments il faut définir une fonction ou faire une preuve).

  Notre travail consiste à proposer un calcul dans lequel on peut définir des structures non libres sans introduire d’inconsistance tout en conservant des principes d’élimination utilisables. Pour cela on permet la définition d’un type, dit normalisé, à partir d’un autre type T et d’une fonction nf de T vers T. Dans ce nouveau type, deux termes x et y seront égaux si et seulement si (nf x) et (nf y) sont égaux. Les propriétés de confluence, normalisation forte et stabilité du typage par rapport à la réduction sont démontrées pour ce calcul.

• Deuxièmement, de présenter un nouveau champ d’application des assistants de preuve: la preuve d’algorithmes auto-stabilisants.

Plan de la thèse

La partie ?? est consacrée à la présentation progressive de différents lambda-calculs: les lambda-calculs pur et typé, puis le calcul des constructions et enfin le calcul des constructions inductives. On introduira également quelques notions importantes comme l’isomorphisme de Curry-Howard, la sémantique de Heyting (section ??). Le lecteur familier de ces concepts pourra éviter de lire les premiers chapitres. Le dernier chapitre est une courte présentation de l’assistant de preuve Coq, dans lequel on illustre certains principes expliqués jusque là.

La partie ?? présente le calcul des constructions inductives avec types normalisés ainsi que les preuves de ses différentes propriétés.

Enfin la dernière partie décrit un développement en Coq d’une preuve d’algorithme auto-stabilisant. On y trouvera notamment quelques définitions et résultats concernant la réécriture sur les mots.

1

Nous verrons plus loin que ces méthodes consistent exactement en des démonstrations mathématiques.

2

Un tel algorithme est dit réparti.

3

Le mot théorie désigne aussi parfois l’ensemble des théorèmes démontrables à partir des axiomes.

4

L’ensemble des propriétés démontrables dans une théorie est l’ensemble des propriétés qu’on peut déduire des axiomes. On verra qu’une déduction se fait à l’aide d’un système de règles de déduction, lui-même défini au préalable.

5

Cette notion, la décidabilité, est définie de manière très précise et caractérise tous les problèmes que le calcul sans raisonnement est capable de résoudre. Il est très courant de définir par inadvertance une notion de vérification indécidable, c’est-à-dire qu’aucun programme ne pourra effectuer dans tous les cas.

6

Ce n’est pas la théorie des types dont il est question dans cette thèse; nous y parlerons de la théorie des types de Martin-Löf, laquelle est en effet une reformulation intuitionniste de celle de Russel.

7

On dit aussi qu’une propriété est indépendante d’une théorie.

8

Ainsi que dans toute autre théorie ayant une expressivité comparable, l’indécidabilité réside bien dans la logique exprimée par le système et non dans sa formulation.

9

x est donc un argument abstrait, c’est la signification de la notation lambda x.

10

Ce but ne sera pas atteint de la manière imaginée par Church car le lambda-calcul typé n’est pas assez expressif. C’est la théorie des types de Martin-Löf qui y parviendra, voir plus bas.

Ce document a été traduit de L^AT_EX par H^EV^EA