Une nouvelle plume, un nouveau talent, un nouvel esprit curieux et passionné rejoint notre équipe de WUKALI, ainsi avons-nous le plaisir d’accueillir Loïc Colson, scientifique et mathématicien, professeur à l’université de Lorraine.
La vérité en mathématiques et en informatique: la perte des certitudes, tel est bien le titre de son premier opus dans notre magazine, un sujet qui bien au-delà du champ de la connaissance abstraite et des raisonnements logiques qui définissent le champ mathématique, interpelle notre confort philosophique.
PAL
Avec l’apparition de l’informatique et de la mécanisation du travail dans les cent dernières années, l’humanité dans son ensemble a entamé sa libération des nombreux jougs engendrés par des tâches routinières et pénibles, pour les remplacer par des activités plus créatrices et ludiques comme l’écriture de programmes informatiques réalisant cette mécanisation.
Il reste cependant un gros problème potentiel, à savoir la possibilité de l’existence de bugs ou d’erreurs dans les programmes qui font que la sémantique du programme (c’est à dire ce que le programme fait) peut ne pas correspondre à sa spécification (c’est à dire ce qu’il est censé faire). Ceci est particulièrement apparent dans l’utilisation des systèmes d’exploitation des ordinateurs qui réalisent l’indispensable pont entre l’architecture matérielle des très puissants ordinateurs (ou machines) d’aujourd’hui et l’utilisateur, qui en général ne connait pas cette architecture et souhaite utiliser ces machines à ses fins. Il arrive par exemple fréquemment que le système d’exploitation « parte » dans une boucle infinie ou se mette à « grossir indéfiniment » et que l’utilisateur perde le contrôle de la machine. Il s’agit alors d’un phénomène de non-terminaison.
Ces phénomènes gênants ne sont pas prévisibles à l’avance car un résultat de base d’informatique théorique établit qu’il n’existe aucun programme qui prendrait en entrée un autre programme informatique et saurait prédire s’il va terminer ou non. Ce résultat (appelé indécidabilité du problème de l’arrêt), très décevant pour les apprentis-informaticiens, est pourtant une réalité enseignée dans la plupart des Master d’Informatique du monde occidental dans les cours de « Calculabilité » ou « Modèles de Calcul ».
Presque dès le début de l’Informatique des techniques ont été développées pour s’assurer de la correction des programmes (c’est à dire de l’adéquation entre leur spécification et leur sémantique). Comme l’ensemble des configurations possibles envisagées par un programme est en général infini (à cause par exemple du caractère infini de l’ensemble des entiers naturels), il n’est pas possible de faire un test exhaustif du programme dans toutes les configurations possibles (ceci engendrerait un calcul qui serait lui aussi infini). Le seul moyen connu de maîtriser cet infini est d’écrire des preuves ou démonstrations comme les mathématiciens savent en produire depuis les Grecs Anciens (voir [1] pour la naissance de la forme moderne de la notion de démonstration).
document Futura
On aboutit ainsi à la notion de preuve de correction de programme. Une des principales techniques de preuve utilisée est celle de démonstration par récurrence qui permet d’établir une propriété mathématique « pour tous les entiers naturels ». Comme exemple (élémentaire mais utilisé très fréquemment dans toutes les sciences exactes) on peut citer la preuve de « commutativité de l’addition » qui établit que x+y est toujours égal à y+xquels que soient x et y . Ce résultat (à peu prés évident) nécessite malgré tout une petite preuve par récurrence, enseignée souvent en France au lycée dans les classes de Terminale Scientifique. Signalons que l’activité démonstratrice, qui semble être l’apanage des scientifiques, laisse en fait une trace dans le langage courant: on dit par exemple en français « c’est aussi sûr que 2 et 2 font 4 » ou « je lui ai démontré par a+b qu’il avait tort et que j’avais raison ».
Il reste à définir de façon définitive et parfaitement précise la notion de preuve pour fixer les règles de cet immense jeu qu’est la recherche de preuves mathématiques. C’est là un des objets principaux de la branche des Mathématiques appelée Logique Mathématique, plus précisément de sa division nommée Théorie de la Démonstration, (Proof Theory en anglais). Le résultat de cette approche est ce que l’on appelle un système formel ou plus familièrement une logique. Il n’est pas question ici de donner un exemple de tel système formel, disons simplement qu’il s’agit en général d’une définition parfaitement précise de quelques pages, qui explicite entièrement les règles de base de la pensée rationnelle occidentale.
Une fois défini un système, formel, on dispose d’une méthode apparement définitive pour établir la correction d’un programme informatique. Restent toutefois deux problèmes de taille pour valider cette méthodologie.
Premier problème avec un système formel
Depuis Euclide et les Grecs Anciens et jusqu’à une époque récente les démonstrations étaient conçues et vérifiées par les humains à l’aide de leur propre esprit. Pour les démonstrations longues (comme celle découverte en 1993 du Théorème de Fermat, qui nécessite une centaine de pages) un risque considérable d’erreur non détectée par les mathématiciens qui vérifient la conformité de la preuve avec le système formel existe. Comme exemple d’erreur célèbre on peut citer la démonstration d’un des Problèmes de Hilbert posés par David Hilbert (le mathématicien leader mondial à cette époque là) au Congrès International des Mathématiciens de 1900. Cette démonstration était fausse. Il a fallu des années avant que l’on s’en aperçoive.
De nos jours avec l’apparition des ordinateurs il était naturel d’essayer d’écrire des programmes permettant de vérifier mécaniquement des preuves. Cela peut paraître impossible car, intuitivement, pour vérifier une preuve il faut la comprendre ce qui peut sembler irréalisable par un ordinateur. C’est là que le travail effectué par les Logiciens du 19ème-20ème siècle prend toute sa valeur. En effet quand on a rédigé complètement une preuve en respectant à la lettre la définition du système formel (on dit alors que l’on a atteint la « rigueur absolue »), chaque étape élémentaire de la démonstration est aisément vérifiable par une machine: on dit alors que l’on a formalisé complètement la preuve.
Basés sur cette constatation sont apparus dans les années 1960 les premiers « proof assistants » sous l’impulsion de Nicolas de Bruijn à l’Université d’Eindhoven. Un livre entier de fondements de l’Analyse Mathématique a été vérifié par ces systèmes. Depuis de nombreux proof assistants ont été implémentés dont le système Coq développé par l’INRIA, le CNRS et l’Université Paris-Diderot (entre autres). Le système formel sous-jacent et l’implémentation ont été créés initialement par T. Coquand (Université de Göteborg, Suède) et Gérard Huet (Académie des Sciences). Comme application informatique de ce système on peut citer la production d’un compilateur C entièrement certifié dans l’équipe de X. Leroy (professeur au Collège de France). Autre système français développé dans l’industrie à la même période: la méthode B de J.-R. Abrial qui a permis de vérifier un logiciel de pilotage de métros parisiens (la ligne 14 notamment): il n’y a pas de pilote humain dans ces rames de métro qui sont conduites par un ordinateur embarqué. Quand on sait que la vie des passagers est confiée à cette machine on comprend aisément la nécessité d’un programme 100% sans erreur.
Deuxième problème avec un système formel
Il existe un problème potentiel encore plus grave que celui de la correction des preuves dans un système formel: celui de l’existence d’une incohérence dans le système. On dit qu’un système formel est incohérent si l’on peut démontrer « n’importe quoi » dans ce système (n’importe quel énoncé mathématique). En particulier on peut alors démontrer des résultats faux comme 0=1 ou l’énoncé absurde. Cela peut paraitre impossible mais il faut savoir que historiquement le premier système en vraie grandeur, créé par G. Frege en Allemagne à la fin du 19ème siècle, était incohérent. Des preuves de l’absurde sans hypothèse (qu’on appelle des paradoxes) sont apparues en 1899 dans ce système (paradoxe de C. Burali-Forti) puis en 1903 (paradoxe de B. Russell). Le paradoxe de Russell est facilement éliminable pour une raison de « type »: on considère dans la preuve les ensembles x qui n’appartiennent pas à eux même, ce qui n’est pas « typable » car on ne voit pas très bien comment un tel objet x pourrait être à la fois du type ensemble et du type élément. Le paradoxe de Burali-Forti est plus difficile à évacuer.
En 1908 est apparu un système moins fort que celui de Frege (et à partir de là ayant plus de chances d’être cohérent): la théorie des ensemble de Zermelo. C’est une version étendue de ce système, connue sous le nom de théorie des ensembles de Zermelo-Fraenkel (ZF), qui est encore de nos jours adoptée par la majorité des mathématiciens. La méthode B est basée sur ce système.
Parallèlement aux théories des ensembles, la « théorie des Types » a été inventée par B. Russell à la même époque, qui exploitait la notion de type évoquée ci-dessus. Le « Calcul des Constructions » sous-jacent au système Coq et inventé par T. Coquand dans sa thèse en 1985 n’est rien d’autre que la plus puissante théorie des Types connue actuellement. Signalons que ce système a été récompensé récemment par deux Prix de l’ACM (le premier pour « génie logiciel » et le second pour « langage de programmation ») voir la vidéo [2].
Dès que le système ZF a été inventé, des mathématiciens comme David Hilbert, troublé par les paradoxes récents, ont cherché a déterminer s’il était cohérent. Alors très courageusement Hilbert a entrepris de prouver mathématiquement sa cohérence, démarche normale pour un scientifique [3]. Bien entendu pour qu’une telle preuve ait quelque valeur il était nécessaire que cette preuve soit conduite dans un système suffisamment « petit » (c’est à dire ne faisant intervenir que de façon élémentaire des objets concrets comme des entiers par exemple, par opposition à des objets abstraits comme des ensembles infinis) pour être complètement sûr.
Après une dizaine d’années de tentatives infructueuses dans ce sens, le verdict est tombé en 1934 comme un couperet: aucun système formel comme ZF ne peut prouver sa propre cohérence, ni bien sûr aucun système plus petit, sous peine d’être lui même incohérent. C’est le célèbre second théorème d’incomplétude de Gödel. On peut souvent réussir à prouver la cohérence d’un système de fondements mais dans un système plus fort, qui nécessitera lui même un système encore plus fort pour être justifié, etc… Il n’y a donc pas de système formel « à tout faire » qui pourrait être utilisé pour formaliser toutes les mathématiques et l’informatique. Les preuves de cohérence connues actuellement ne sont donc que des preuves relatives, aucune preuve absolue n’étant possible.
Voilà où en sont actuellement (90 ans plus tard) les fondements communs des Mathématiques et de l’Informatique.
Conclusion
A cause du second théorème d’incomplétude on ne peut en aucun cas prouver la cohérence des Mathématiques. Morris Kline à l’Université de New-York a donc intitulé son livre sur ce sujet Mathématiques: la perte des certitudes [4]. Il paraît ainsi indispensable de garder l’esprit ouvert sur ce thème et de continuer à chercher de nouveaux paradoxes, car si on n’en cherche pas, on n’en trouvera probablement aucun : d’une façon générale pour trouver quelque chose il peut être utile d’être en train de le chercher.
Signalons pour finir qu’Henri Poincaré (qui se battait avec Hilbert pour le leadership mondial) a « conjecturé » (c’est à dire pronostiqué) en 1912 avec humour et discrétion que la Théorie des Ensembles de Zermelo était incohérente: il a écrit dans [5] « mais si monsieur Zermelo a bien fermé sa bergerie, je ne suis pas sûr qu’il n’y ait pas enfermé le loup ». Et dans [6] chez la plupart d’entre nous ces préventions s’étaient dissipées, mais il est arrivé qu’on s’est heurté à certains paradoxes, à certaines contradictions apparentes, qui auraient comblé de joie Zénon d’Elée et l’école de Mégare. Et alors chacun de chercher le remède». Je pense pour mon compte, et je ne suis pas le seul, que l’important c’est de ne jamais introduire que des êtres que l’on peut définir complètement en un nombre fini de mots. Quel que soit le remède adopté, nous pouvons nous promettre la joie du médecin appelé à suivre un beau cas pathologique ».
Références
[1] Euclide, Eléments de géométrie. Presses Universitaires de France.
[2] ACM Software System Award 2013 – Coq, vidéo réalisée à l’occasion de la remise des prix de l’ACM. Chercher à « coq ACM » sur la toile.
[3] David Hilbert, On the infinite (1925). Traduction anglaise dans « From Frege to Gödel », ed. van Heijenoort, Harvard University Press, 1967.
[4] Morris Kline. Mathematics, the loss of certainty. Oxford University Press.
[5] Henri Poincaré. Dernières pensées. Flammarion, Paris.
[6] Henri Poincaré. Science et méthode. Flammarion, Paris.
Illustration de l’entête: oeuvre de Salvador Dali, Montre molle au moment de la première explosion (1954)
Lithographie couleur Signée, numérotée
Dimensions de la feuille 50 x 65 cm
Image 32 x 40 cm
Vous souhaitez réagir à cet article
Peut-être même nous proposer des textes et d’écrire dans WUKALI
Vous voudriez nous faire connaître votre actualité
N’hésitez pas, écrivez-nous : redaction@wukali.com
Notre meilleure publicité c’est VOUS !
Alors merci de relayer l’article auprès de vos amis et sur vos réseaux sociaux 😇…
