Les systèmes d’aide à la preuve

Les systèmes d’aide à la preuve

Il existe actuellement un grand nombre d’Assistants de Preuve (AP), certains étant pourvus d’une importante communauté d’utilisateurs (académiques et industriels), d’autres expérimentaux et restant à l’intérieur d’un cercle restreint d’utilisateurs. Mais dans tous les cas, l’utilisation en est réservée de fait aux spécialistes, c’est-à-dire à des personnes possédant un bagage mathématique suffisant — qui plus est, dans le domaine des mathématiques formelles et de la logique — et, lorsqu’il s’agit de faire de la preuve de programmes, d’un bagage informatique (algorithmique et parfois sémantique des langages de programmation).

Qu’est-ce qu’un assistant de preuve ?

Notions préliminaires
Les assistants de preuve reposant sur les mathématiques formelles, il est utile de présenter succinctement quelques notions nécessaires. Les travaux de formalisation des mathématiques ont deux aspects, d’un côté formaliser le raisonnement et le langage mathématique, d’un autre formaliser les briques de base sur lesquelles faire reposer les mathématiques (fondements des mathématiques). Ces deux niveaux apparaissent dès l’antiquité, avec notamment du côté de la formalisation du langage, les travaux d’Aristote, et du point de vue des objets manipulés, les travaux d’Euclide.

Variables et fonctions
Les notions de variables et de fonctions prennent de l’importance au dix-huitième siècle, avec Leibniz et Newton. Une variable est susceptible de dénoter une inconnue, que l’on cherche à calculer, une valeur générique (“soit x un entier, montrons que x est pair ou x est impair”), ou encore un paramètre d’une fonction. Les fonctions peuvent être considérées selon deux points de vue : le point de vue intentionnel, c’est-à-dire le procédé “comment calcule-t-on une valeur à partir des arguments” et le point de vue extensionnel (qui ne se préoccupe pas du calcul, mais uniquement du graphe de la fonction).

Prédicats et types
On distinguera deux notions a priori assez proches, les notions de prédicats et de types. Un prédicat dénote une propriété sur un objet (“être pair”). Les types dénotent la classe d’objets vérifiant une propriété. A chaque valeur du langage, on associera un type : 3 est de type nat (le type des entiers naturels), et l’addition sur les entiers naturels est de type nat ∗ nat → nat (prend deux entiers et renvoie un entier comme résultat). Les types permettent de restreindre les formules “légales” : on ne peut donc pas additionner un entier et une fonction. La théorie des types de Russell-Whitehead qui essaie de pallier au paradoxe de Russell a pour but d’empêcher d’écrire dans un langage mathématique formel certaines expressions amenant une incohérence, comme par exemple “x est élément de x” .

Termes et formules

On peut diviser le langage mathématiques en quatre parties (la quatrième, les preuves sont traitées dans la section suivante) :
– les termes, qui dénotent les objets manipulés (entiers, fonctions, variables d’individus) ;
– les formules qui permettent d’exprimer les propriétés sur ces termes, à l’aide de connecteurs (et, ou, implique. . .) et de quantificateurs (pour tout, il existe) ;
– le langage vernaculaire, permettant d’exprimer que telle formule est un théorème, de poser des définitions, des axiomes et de déclarer une variable.

Preuves

La preuve d’une proposition est une justification de celle-ci, sous la forme d’un raisonnement dont chaque étape est irréfutable, permettant de convaincre de la véracité de la proposition. Une preuve formelle est une preuve exprimée dans un langage formel (c’est-à-dire dont la syntaxe est complètement définie, et ne permet aucune ambiguïté) et où l’irréfutabilité des étapes de cette preuve repose sur le fait que chaque étape de cette preuve peut être vérifiée syntaxiquement. On utilise un ensemble de règles de déduction établissant quelles sont les étapes admises dans la preuve. Cela passe donc par une formalisation du raisonnement mathématique .

Lorsqu’un énoncé mathématique est prouvé formellement, il est donc possible de remonter en suivant la ou les preuves jusqu’aux “bases” de la théorie dans laquelle on travaille.

Lambda-calcul 

Le lambda-calcul, inventé par Church, est avant tout une formalisation de l’écriture des fonctions. On écrira par exemple λx.λy.x la fonction qui prend deux arguments (x et y) et qui renvoie comme résultat le premier (la valeur de x). Un terme du lambda calcul est soit une variable, soit l’application de deux termes (notée par la juxtaposition) f x signifiant “f appliqué à x”, et l’abstraction d’une variable λx.t signifiant “la fonction qui à x associe t”, où x peut apparaître dans t. On ajoute à cela des parenthèses pour lever les ambiguïtés.

Cette notation ne serait pas très utile sans la règle de calcul qui lui est associée : la bêta-réduction. Cette règle de calcul est purement syntaxique. Elle exprime qu’un terme de la forme (λx.t) u (la fonction qui à x associe t, appliquée à u), se calcule en t, dans lequel on aura substitué u à chaque occurrence de x. Par exemple, (λx.λy.x) t1 t2 donne d’abord (λy.t1) t2, puis t1 (si y n’apparaît pas dans t1).

À travers des codages, il est possible d’exprimer des données et les opérations sur ces données. Par exemple, on codera le 0 par λx.λf.x, le 1 par λx.λf.(f x), le 2 par λx.λf.(f(f x)), etc.

Le lambda-calcul étant en fait “trop expressif” (on peut appliquer n’importe quelle fonction, voire quelque chose qui n’est pas une fonction, à n’importe quoi), il est possible de le typer, c’està-dire de déterminer le type d’un terme de façon à savoir d’une part s’il est correct, d’autre part dans quel contexte l’utiliser. Cela permet de restreindre le langage à une certaine classe de fonctions (par exemple les fonctions totales). On écrira par exemple λ(f : ι → ι)λ(x : ι).(f x) (où ι est un type arbitraire) est une fonction prenant en argument f (une valeur fonctionnelle) et x et renvoyant le résultat de l’application f x, lui même de type ι. On ne pourra par plus écrire x x (x appliqué à lui-même), car on ne saura pas le typer. Deux grandes familles de méthodes existent pour typer le lambda-calcul : à la Church, en contraignant les variables par un type (comme ci-dessus), ou à la Curry, en cherchant à déterminer le type sans que le terme soit annoté.

Il est courant d’ajouter des extensions au lambda-calcul, que cela soit des types (entiers, booléens, listes), ou des combinateurs (récurseurs, analyse par cas, point fixe) avec leurs règles de calcul. Par rapport à la vision habituelle des fonctions en mathématiques, le lambda-calcul offre l’avantage de mettre en évidence le “procédé” de calcul. La fonction est donc définie par son algorithme. C’est pour cette raison que ce langage est adapté à la représentation de programmes informatiques. Plusieurs langages informatiques dérivent directement du lambda-calcul : tout d’abord LISP et Scheme (lambda-calcul non typé), mais aussi les langages de la famille ML (lambda-calcul typé) qui nous intéressent particulièrement .

Isomorphisme de Curry-Howard

L’isomorphisme de Curry-Howard met en évidence la similarité entre les preuves et les lambda-termes, notamment il est possible de “calculer” avec des preuves comme avec des lambda-termes. Par exemple une preuve de A → B est considérée comme une fonction qui à toute preuve de A associe une preuve de B. De plus, on peut noter les preuves de la même façon que les fonctions en utilisant les termes du lambda-calcul.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela rapport-gratuit.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

Introduction
1 Les systèmes d’aide à la preuve
1.1 Qu’est-ce qu’un assistant de preuve ?
1.1.1 Notions préliminaires
1.1.1.1 Variables et fonctions
1.1.1.2 Prédicats et types
1.1.1.3 Termes et formules
1.1.1.4 Preuves
1.1.1.5 Lambda-calcul
1.1.1.6 Isomorphisme de Curry-Howard
1.1.2 Généralités
1.1.3 Interaction
1.1.4 Ingrédients
1.2 Pour l’informatique
1.2.1 Spécification
1.2.2 Implémentation
1.2.2.1 Extraction
1.2.2.2 Raffinement
1.2.3 Vérification
1.3 Tour d’horizon de quelques systèmes
1.3.1 Coq
1.3.1.1 Exemple
1.3.1.2 Interface
1.3.1.3 Program
1.3.2 Agda et Alfa
1.3.3 Isabelle/HOL
1.3.4 PhoX
1.3.5 PVS
1.3.6 ACL2
1.3.6.1 Exemple
1.4 Synthèse
1.5 Conclusion
2 Motivations de ce travail
2.1 ML comme langage cible
2.2 Pourquoi et pour qui ?
2.3 Vérification de programme
2.4 Une logique simple
2.5 Un système extensible, mais sûr
2.6 Un système ergonomique
2.7 Objectifs
3 Formalisation
3.1 Quelques notations
3.2 Définition du langage miML
3.2.1 Syntaxe
3.2.2 Langage de types
3.2.3 Typage des termes
3.2.4 Évaluation
3.3 Langage de spécification
3.3.1 Formules
3.3.2 Typage des formules
3.3.3 Système de preuve
3.4 Théorie
3.4.1 Compléments sur les types
3.4.2 Égalité
3.5 Langage Vernaculaire
3.5.1 Déclaration
3.5.2 Définition
3.5.3 Axiome
3.5.4 Théorème
3.5.5 Let
3.5.6 Type
3.5.7 Session
3.6 Conclusion
4 Spécification
4.1 Modèle client-serveur
4.2 Protocole de communication
4.2.1 Classe Protocol
4.2.1.1 Requêtes
4.2.1.2 Réponses
4.2.2 Classe Session
4.2.2.1 Requêtes
4.2.2.2 Réponses
4.2.3 Classe Proof
4.2.3.1 Requêtes
4.2.3.2 Réponses
4.3 Spécification du moteur de preuves
4.3.1 Environnement
4.3.2 Preuves
4.3.3 Niveau session
4.3.4 Niveau preuve
4.4 Spécification de l’interface
4.4.1 Niveau session, événements utilisateur
4.4.2 Niveau session, événements moteur
4.4.3 Niveau preuve, événements utilisateurs
4.4.4 Niveau preuve, événements moteur
Conclusion

Rapport PFE, mémoire et thèse PDFTélécharger le rapport complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée.