Electrons prisonniers

Quand je dis intuitivement, c'est très formel. Moralement, ça veut dire que les programmes sont les duaux des environnements.

J'adore Paul-André Melliès et son cours sur les catégories, mais je dois dire que son usage des adverbes est parfois déroutant : que vient diable faire la morale dans un cours d'informatique théorique ?

Que ça dure ou pas, ce soir, on est heureux. Et ça, c'est précieux.

Extrait de Jésus de Montréal.

Je recommande chaudement ce film québecois, par les réalisateurs du déclin de l'empire américain et des invasions barbares. Il s'agit d'une transposition moderne de la vie de Jésus, drôle et subtile (Jésus devient un comédien qui joue le rôle de Jésus). La présence de quelqu'un connaissant bien les évangiles à vos côtés est absolument indispensable si vous voulez comprendre toutes les références (à moins que vous ne rentriez vous-même dans cette catégorie). Un complément intéressant à ma note récente sur la religion.

Le texte suivant est une transcription de la conférence donnée par Alexandre Miquel à l'occasion de la fête de la science le 12 octobre 2007. Il n'a pas été relu par l'orateur ; en conséquence, je suis seul responsable des erreurs ou inexactitudes qu'il pourrait comporter. Il est d'ailleurs probable qu'il y en ait, ces notes n'ayant été que relues rapidement après la conférence. Merci de me signaler tout passage obscur.

Les mathématiques sont de plus en plus utilisées en sciences : physique, informatique, biologie, économie. Est-ce bien raisonable ? En effet, les méthodologies sont assez différentes. Dans les sciences expérimentales, on utilise une méthode empirique ; en mathématiques, une méthode axiomatique. Comment les deux peuvent-ils fonctionner ensemble ?

Il se trouve qu'en sciences expérimentales, on commence toujours par modéliser le problème. On se trouve alors dans un monde abstrait, mathématique, dans lequel on est franchement déconnecté de la réalité. Mais après avoir bien suivi les délires des mathématiciens, on obtient des résultats qu'on va appliquer : on les interprète pour obtenir des prédictions sur le monde réel, physique. Pourquoi fait-on confiance à ce point aux mathématiques ? On part d'un problème concret, on revient à un problème concret, mais on est passé par un monde totalement abstrait : comment savoir si notre problème de départ et notre problème d'arrivé ont un rapport ? Comment être certain que les mathématiques n'ont pas fait n'importe quoi dans l'intervalle ? C'est un problème philosophique mais aussi scientifique très sérieux, que les physiciens, les biologistes, les économistes, etc. sont obligés de se poser.

Prenons un petit exemple : les principes de la mécanique de Newton. Newton a posé deux lois très simples, l'une liant la force au mouvement (c'est le principe fondamental de la dynamique) et l'autre liant les forces à la présence de masses dans l'univers (c'est la loi de la gravitation universelle). Ce qui est remarquable, c'est qu'avec ces deux lois, on retrouve trois autres lois qui étaient connues bien longtemps avant celles de Newton : les lois de Kepler. Les lois de Kepler décrivent le mouvement des planètes du système solaire ; celles de Newton sont beaucoup plus générales, elles traitent de tous les corps en mouvement. Pour passer des unes aux autres, il est nécessaire de passer par des mathématiques assez compliquées (ou qui, du moins, font très peur quand on les regarde de loin). Ce qui est incroyable, c'est que ce passage par les mathématiques ne parlent absolument pas de forces, ni de planètes. Ce sont des opérations purement mathématiques. Et encore, pour ce qui est de Newton, ça reste assez simple. Depuis, Einstein est passé par là, et il a eu besoin pour sa théorie d'utiliser une partie des maths qui s'appelle les espaces de Minkowski, et qui font vraiment très très peur. De même pour la mécanique quantique, qui utilise les espaces de Hilbert.

C'est un problème général : il n'y a pas de rapport immédiat entre les mathématiques utilisées et le phénomène modélisé. En d'autres termes, les maths sont toujours hors-sujet. Elles le font même presque exprès : en maths, on ne s'intéresse qu'aux arguments logiques, pas au rapport avec le monde réel.

Un autre problème : les objets mathématiques abstraits n'ont souvent aucun équivalent dans le monde sensible. Finalement, les maths, c'est quasiment de la métaphysique. Ne serait-ce que lorsque vous dites « 2 + 2 = 4 » : avez-vous déjà vu le nombre 2 ? et le nombre 4 ? Non. Vous avez déjà vu deux pommes, ou deux yeux ; mais jamais « le nombre 2 ».

Les mathématiciens délirent totalement. Emmenez un mathématicien chez un psychiatre qui n'a jamais fait de maths, il pourrait le faire hospitaliser. Alors, pourquoi ça marche, les mathématiques ? Nous allons tenter de répondre à cette question, posée par E. Wigner dans un célèbre article, « La déraisonnable efficacité des mathématiques dans les sciences de la Nature. »

Il faut se rendre à l'évidence : on ne sait pas ce que sont les objets mathématiques. Par contre, ce que l'on sait, c'est calculer et raisonner avec ces objets. Le chef de file de cette école de pensée est David Hilbert, qui pensait que les mathématiques ne sont que des symboles, dont le sens n'a aucune importance. A la même époque, au début du XXe siècle, on commença ainsi à s'intéresser à la grammaire des mathématiques.

En mathématiques, il y a des objets, qu'on appelle les termes : 2, pi, la fonction racine carrée en sont des exemples. Il y a également des faits, que l'on appelle formules : « 2 + 2 = 4 », « 1 = 3 » (oui, des formules peuvent être vraies ou fausses), etc. Enfin, il y a des raisonnements, que l'on appelle preuves : ce sont les règles de la logique qui disent ce qu'on a le droit de faire avec les termes et les formules. Par exemple si A est vrai et que A implique B, alors B vrai (en remplaçant A et B par n'importe quelles formules). Dès lors, certains mathématiciens ont commencé à étudier les démonstrations, dans les années 1930 : c'étaient des mathématiciens qui se penchaient sur le fonctionnement même des mathématiques.

Quelques résultats découverts à cette époque : * les preuves peuvent être vérifiées par un objet : aujourd'hui, cet objet est un ordinateur ; * la vérité n'est pas calculable : les ordinateurs peuvent vérifier qu'une preuve est correcte, mais ils ne peuvent pas les inventer (sauf pour quelques preuves très simples) ; * tous les problèmes de maths n'ont pas forcément une solution (voir mon billet sur Turing, Church et l'addition).

Un problème fondamental, c'est la cohérence des mathématiques : est-ce que lorsque je fais un calcul, je suis sûr que je ne vais pas retrouver avec une contradiction. Par exemple, j'ai démontré que a^2 + b^2 + 2ab = (a + b)^2. Mais lorsque je vais remplacer a par 5 et b par 7, vais-je bien obtenir 144 = 144, et non pas 144 = 145 ? Deux résultats de l'époque : * la cohérence des mathématiques n'est pas démontrable avec les mathématiques ; * la cohérence des mathématiques n'est pas certaine. Finalement, il faut avoir confiance dans la cohérence des mathématiques, de même qu'on a confiance dans les lois de Newton. Mais on se rendre peut-être compte un jour que ça ne fonctionnera pas (comme lorsqu'Einstein est arrivé en physique) ; il faudra alors les modifier, pour garder la cohérence.

Dans les années 1970, on a découvert des résulats plus rassurants. Notamment, on s'est rendu compte qu'il y avait une étrange ressemblance entre les programmes informatiques et les règles de la logique : la correspondance de Curry-Howard (voir mon billet sur Curry, Howard, de Bruijn et Pythagore).

Intéressons-nous à la théorie de Popper : pour lui, ce qui caractérise une science, c'est son caractère falsifiable. C'est le critère de démarcation. En d'autres termes, est-ce que la science fournit elle-même les outils pour vérifier qu'elle est vraie ou fausse ? Est-ce qu'elle énonce des choses précises et testables ? Une propriété est falsifiée si l'on fait une prédiction et qu'on se rend compte par l'expérience que notre prédiction était erronée.

Attention : le critère de démarcation n'est pas un critère de signification. On peut avoir une théorie qui n'est pas falsifiable mais qui a du sens quand même (et inversement). Une théorie sera d'autant plus scientifique qu'elle énonce des interdictions,

Finalement, une vérité scientifique n'a rien à voir avec la certitude. Pour avoir des certitudes, il vaut mieux aller voir du côté de la religion.

Mais quel rapport avec l'efficacité des mathématiques ? Prenons deux théories A et B, telles que A implique B mathématiquement. Supposons alors que B est falsifiable expérimentalement : pourra-t-on en déduire que A est aussi falsifiable expérimentalement ?

Utilisons l'isomorphisme de Curry-Howard : on peut transformer une preuve de A implique B en un programme (informatique) qui transforme une preuve de A en preuve de B, mais également une falsification expérimentale de A en falsification expérimentale de B ! C'est un résultat assez récent, datant de 2006, découvert par Alexandre Miquel.

Reprenons l'idée de départ : je pars du monde concret, je le modélise, je fais une preuve p sur le modèle, et je réinterprète dans le monde concret. Maintenant, si je trouve un contre-exemple expérimental à mon résultat, je pourrai transformer ma preuve p en un programme (informatique, donc concret) qui produit un contre-exemple à mon problème de départ.

Le passage par le modèle mathématique est alors justifié, raisonnable. Même si l'on est passé par un monde abstrait, ce n'était qu'une étape temporaire, utile pour stimuler l'imagination, pour étendre les conséquences d'une théorie. Mais en aucun cas on ne perd le rapport à la réalité, car on a toujours un moyen de revenir en arrière, via le monde réel. Si les conséquences de ce qu'on a déduit par les mathématiques ne se vérifient pas expérimentalement, on est certain que le problème n'était pas dans le passage abstrait, mais bien dans les hypothèses de départ (à condition que la modélisation et la preuve soient correctes, bien sûr).

Des transparents sur le même sujet (mais issus d'une conférence plus technique) sont disponibles sur le site d'Alexandre Miquel.

Mise à jour : les transparents de la conférence sont disponibles. Un brouillon d'article (technique) est également disponible sur demande auprès de l'auteur.

Entendu tout à l'heure :

Ce n'est pas Dieu qui a besoin de vous, c'est vous qui avez besoin de lui. Ceux qui font la guerre pour Dieu... Mais c'est lui le Tout-Puissant ! S'il a besoin de faire la guerre, il la fait lui-même.

Georges Montgenoty, professeur de kung-fu se définissant lui-même comme taoïste et croyant, et n'hésitant pas à écouter l'émission anticléricale de Radio Libertaire pour se confronter à d'autres points de vue.

Peu après, il ajouta :

C'est à chacun de décider s'il veut croire ; tant qu'il ne dérange pas son voisin. La foi, c'est quelque chose de personnel. Ceux qui s'énervent, pour les caricatures par exemple, ils ont peut-être un problème avec leur foi.

Commentaires

Krazy Kitty me signale que au contraire, d'autres se lancent dans un djihad laïc... (et ils ont bien raison à mon avis). Quant à Jaina, elle me met en garde :

C'est délicat ce que tu fais là. Mon expérience m'a appris qu'il est souvent délicat d'aborder ce genre de questions, et toujours impossible de les résumer en quelques lignes...

Pour éviter tout malentendu (et une attaque d'intégristes judéo-islamo-chrétiens sur mon blog), une petite précision : je rapporte ces paroles parce que je les ai trouvées pertinentes, et que cette idée de se substituer à Dieu quand on prétend faire la guerre en son nom me semble rarement relevée, alors qu'elle montre un orgueil assez peu religieux à mes yeux. Libre à chacun d'y adhérer ou pas ; la seule intolérance, la vraie, serait de ne pas accepter l'expression d'une opinion différente (tant qu'elle reste raisonable, et je ne pense pas verser ici dans l'excès).
Quant à la réflexion finale sur les caricatures, j'insiste sur le peut-être et invite chacun à se poser la question en son âme (religieuse ou pas) et conscience.

J'ai mis en place des commentaires. Si vous avez javascript désactivé, cela devrait vous afficher un lien vers mon adresse email. Sinon, vous aurez un joli cadre clinquant Web 2.0. Sauf que... sauf que le service que j'utilise n'a pas l'air d'être très respectueux des standards. Et apparemment, ça hérisse le poil de Firefox quand il doit exécuter le script alors que la page est servie en mode application/xhtml+xml.

Je n'ai qu'à la servir en mode text/html me direz-vous (*). C'est ce que je fais déjà pour les utilisateurs d'Internet Explorer (qui peuvent donc poster des commentaires). Mais je crois plutôt que je vais virer ce système rapidement, surtout que ça spamme à mort et qu'ils se font du blé en faisant des statistiques sur votre dos. Bon, bref, c'était un test, mais ce n'est pas hyper-concluant. Et puis en plus, ils utilisent des attributs qui cassent la validation.

Si quelqu'un arrive à voir un commentaire d'une manière ou d'une autre, je serais curieux qu'il en laisse un (avec une fausse adresse email sauf s'il aime le spam) me disant quel est son navigateur.

C'est pas demain la veille que je pourrai écrire "Lâchez vos coms !!!!" sur ce blog.

Mise à jour : c'est fait, ils sont partis comme ils étaient venus. Vous pouvez m'envoyer des commentaires par mail. Ils seront intégrés au billet le cas échéant.

(*) ou pas, selon votre niveau de compréhension de ce que je suis en train de raconter.

Je souhaite que les élèves se découvrent lorsqu'ils sont à l'école et qu'ils se lèvent lorsque le professeur entre dans la classe, parce que c'est une marque de respect.

Nicolas Sarkozy, Lettre aux éducateurs, ISBN 978-11-006893-4

Monsieur le Président de la République, je ne saurais vous recommander trop chaudement la lecture du Respect et le mépris, de Brigitte Labbé et Michel Puech (éditions Milan, collection « Les goûters philo », ISBN 2-7459-0713-1). Vous y apprendriez la différence entre respect et obéissance, et notamment comment toute marque de respect ne peut être par essence qu'individuelle et spontanée. Cela n'empêche pas d'obéir à quelqu'un qu'on respecte ; mais obéir n'est en rien une marque de respect en soi : ce n'est qu'une marque de soumission à une autorité, légitime ou pas.

Il ne vous en coûtera que 6 euros, pour 56 pages de bon sens, accessibles dès 8 ans. Bonne lecture, monsieur le Président.

Rappel de l'épisode précédent : Turing et Church ont chacun leur définition de ce que l'on peut calculer. Le premier utilise de petites machines à états qui écrivent sur des bouts de papier, le second des équations mathématiques qui font peur (un peu). Aucun des deux n'a de preuve. Lequel a raison ?

Comprenez bien pourquoi ni l'un ni l'autre n'avait de preuve de ce qu'ils avançaient : une fonction calculable, ça ne se trouve pas dans la rue. On ne peut pas dire ce que c'est avant de l'avoir définie. En fait, leur vrai problème, c'était de savoir si leur définition correspondait à l'intuition que nous avons des fonctions que l'on sait calculer.

Comment être sûr qu'il ne manquait pas un petit truc dans leur définition ? C'est là qu'est venue l'idée de génie : les deux définitions, celle de Turing et celle de Church, sont exactement équivalentes. Les machines de Turing, avec leur bout de papier infini et leurs états, sont capables de calculer exactement les même fonctions que les équations de Church qui font des noeuds dans la tête.

Qu'est-ce que ça change ? Imaginez qu'ils se soient trompés : cela voudrait dire qu'ils se sont trompés tous les deux exactement de la même manière. Alors même que leurs définitions n'ont rien, mais alors rien à voir ! (D'ailleurs, ce n'est pas facile de montrer qu'elles sont équivalentes.)

C'est ce que l'on appelle la thèse de Church-Turing. Notez bien que ce n'est pas un théorème, ni une propriété. C'est une thèse, une théorie si vous préférez. Comme ces deux définitions traduisent chacune une intuition des fonctions calculables (Turing, l'intuition des opérations faites sur un bout de papier par un humain ; Church, celle des mathématiciens), et comme elles sont équivalente, on a décidé de les prendre comme une définition de ce qui est calculable.

Et les ordinateurs dans tout ça ? Eh bien, croyez-le ou non, mais vos bêtes de courses technologiques tétracore quadricanaux ne sont rien de plus que des machines de Turing. Elles ont une mémoire (la RAM) à la place du papier, un processeur à la place des états, mais elles ne font rien de plus.

Et il y a des fonctions non calculables, alors ? Oui. Par exemple, donnez à un ordinateur le code d'une programme informatique en entrée, et demandez-lui de vous répondre 0 si le programme s'arrête, et 1 si le programme ne s'arrête jamais. Le mieux qu'il pourra faire, c'est lancer le programme et voir s'il s'arrête. Donc, si la réponse est 0, il la donnera un jour (peut-être dans longtemps). Par contre, si la réponse est 1, il n'a aucun moyen de le savoir (pour être plus précis, il peut le savoir parfois, mais en général, il n'a pas de moyen de répondre). C'est ce qu'on appelle une fonction semi-calculable, ou un problème semi-décidable (parce qu'on peut répondre dans la moitié des cas seulement).

Vous remarquerez que le fait qu'un programme ne s'arrête jamais peut être considéré comme un bug. Il faut donc se résigner : il est impossible de décider mécaniquement si un programme informatique quelconque contient des bugs, aussi simplement qu'on ferait une addition. C'est pour cela que les chercheurs en informatique essayent de développer d'autres techniques pour s'assurer que les programmes n'ont pas de bugs (par exemple, démontrer mathématiquement que les programmes sont corrects, comme j'en ai parlé dans un billet précédent, mais cela ne peut donc pas être fait totalement automatiquement).

On voit souvent les ordinateurs comme de super-calculateurs. Qu'entend-on exactement par là ? Un ordinateur est-il capable de calculer plus de choses qu'un être humain, ou simplement plus vite et avec moins d'erreurs ? Y a-t-il des choses qu'un ordinateur ne peut pas calculer ? Ne pourra jamais calculer ?

Répondre à cette question n'a rien d'évident. Les mathématiciens inventent régulièrement, depuis plusieurs siècles, des objets plus ou moins barbares, aux noms aussi doux qu'endomorphismes, cohomologies, fonction zêta. Peut-être les mots de sinus ou racine carrée vous seront-ils plus familiers. Descendons encore plus simplement vers l'addition. Tout le monde sait faire une addition.

En quoi cela consiste-t-il ? Prendre une feuille de papier, écrire les deux nombres à ajouter en haut du papier, et puis appliquer une suite de règles apprises à l'école primaire jusqu'à aboutir au résultat. Si on veut ajouter plus de nombres, ou des nombres plus grands, il suffit de prendre plus de papier. Y a-t-il une limite à la taille des nombres que l'on peut ajouter ? En pratique, bien sûr. Essayez d'ajouter dix mille nombres de dix mille chiffres si vous ne me croyez pas. Mais en théorie, il n'y a pas de limite.

En fait, il serait assez étrange de poser une limite a priori : si on décide de n'ajouter que des nombres de 100 chiffres au maximum, ça ne coûte presque rien d'ajouter des nombres de 101 chiffres. C'est pareil si on décide de mettre la limite à 1000, ou à 10000. On le voit bien avec les ordinateurs : ils sont capables d'ajouter des nombres très grands, et de plus en plus grands au fil des ans. On va donc décider que pour définir ce qu'on peut calculer, la taille ne va pas être un problème. Si on a besoin d'une feuille de papier en plus, on la prend. On s'intéresse à ce que l'on pourrait calculer en théorie, si l'on avait une quantité de papier illimitée.

Pour les ordinateurs, le papier s'appelle la mémoire ; ça ne change absolument rien. Mais alors, à part être infatiguable et avoir plus de mémoire, un ordinateur peut-il calculer plus de choses qu'un être humain ? La réponse est non.

Dans les années 1940, le mathématicien Alan Turing inventa une machine, baptisée logiquement machine de Turing. Cette machine n'était pas une vraie machine (même si Turing passa une bonne partie de sa courte vie à construire les ancêtres des ordinateurs pour le gouvernement anglais). C'était une machine imaginaire, très simple. Elle dispose de feuilles de papier, en nombre illimité. Sur chacune de ces feuilles, elle peut écrire des nombres, et lire ceux qu'elle a écrit. Au démarrage, on lui donne une feuille avec les nombres à additionner (si c'est une machine de Turing qui sert à additionner, bien sûr). Elle lit alors ces nombres, ce qui la fait changer d'état. A chaque étape du calcul, elle lit un nombre, change d'état, écrit un nombre sur une feuille de papier, et passe à l'étape suivante. Quand elle arrive dans un état qu'on appelle final, elle rend la dernière feuille de papier, sur laquelle figure le résultat.

Cette notion d'état peut sembler assez vague ; elle correspond pourtant à ce que nous faisons nous mêmes quand nous ajoutons deux nombres. Souvenez-vous : si la somme des deux chiffres que je suis en train d'additionner est plus grande que dix, je note une retenue. Cette retenue, qu'il faut justement retenir, avant de passer à l'étape suivante, c'est un changement d'état : vous passez de l'état "j'additionne deux chiffres normalement" à l'état "j'additionne deux chiffres mais il ne faut pas que j'oublie la retenue". Cette analogie fonctionne tellement bien, on la retrouve tellement dans tous les domaines du calcul (et de la vie en général), que Turing était sûr et certain que ses machines étaient capables de calculer tout ce qu'un être humain pouvait calculer, et rien de plus.

Mais être certain ne suffit pas. Un autre mathématicien, Alonzo Church, s'intéressa à la même question, d'un point de vue nettement plus formel. Il écrivit des équations, posa des hypothèses, fit de nombreuses démonstrations fort compliquées et finit par arriver à une définition de ce qui était (selon lui) calculable et de ce qui ne l'était pas. Attention, ce n'est pas parce qu'il avait fait plus de calculs que son résultat avait plus de valeur que celui de Turing : tous les deux disaient « ceci est ma définition de ce qu'un être humain est capable de calculer. » Sans preuve, juste avec des exemples montrant que les choses simples pouvaient effectivement être calculées par leur système. Alors, lequel avait raison ? Comment même savoir si l'un des deux avait raison ?

J'ai horreur de laisser planer le suspense comme ça, mais je n'ai pas le temps de finir ce billet maintenant - la suite est disponible

Here is a quick test for a txt2tags plugin for nanoblogger. The code is pretty straightforward:

  # NanoBlogger plugin to render txt2tags format entries
  # /usr/share/nanoblogger/plugins/entry/format/txt2tags.sh
  # Released in the public domain - Gabriel Kerneis
  
  TXT2TAGS="/usr/bin/txt2tags"
  TXT2TAGS_OPTS="-i - -o - --mask-email -H -q -t xhtml "
  
  # nb_msg "$plugins_textformataction `basename $nb_plugin` ..."
  NB_EntryBody=$(echo "$NB_EntryBody" | ${TXT2TAGS} ${TXT2TAGS_OPTS})

Lovely, n'est-ce pas ?

Any comment? Send an email to <blog (a) kerneis info> (obsfuscated by txt2tags).

La leçon qu'il nous faut retenir de toutes les extinctions, résume Doug Erwin, c'est qu'il est impossible de prédire ce que sera le monde d'ici cinq millions d'années en s'intéressant aux rescapés.

« Des suprises, il va y en avoir à la pelle. Regardons les choses en face : qui aurait pu prévoir l'existence des tortues ? Qui aurait imaginé qu'un organime allait se retourner comme un gant, puis tirer sa ceinture scapulaire entre ses côtes pour se forger une carapace ? Si les tortues n'existaient pas, aucun biologiste vertébré n'aurait osé prétendre qu'une créature accomplirait cette performance : le monde entier lui aurait ri au nez. La seule prédiction qu'on puisse faire consiste à dire que la vie continuera. Et que ce sera intéressant. »

Extrait de Homo Disparitus, d'Alain Weisman, traduit par Christophe Rosson (édition Flammarion). Un livre passionnant, documenté et poussant à la réflexion sur notre impact environnemental, que je vous recommande chaudement.

Dis, Gabriel, c'est quoi la recherche en informatique ? Ça parle des ordinateurs ? Pourquoi tu dis que ça ressemble à des maths ? Et à quoi ça sert ? Petit aperçu d'un des thèmes qui m'intéressent.

Qu'est-ce qu'un programme informatique ? Rien d'autre qu'une machine qui accepte des données en entrée et renvoie un résultat en sortie. Qu'est-ce qu'une démonstration de mathématiques ? Rien d'autre qu'une suite de propositions, s'enchaînant logiquement. Mais quel est donc le rapport entre les deux ?

Rappelez-vous. Vous êtes au collège. On vous demande de prouver qu'un triangle est rectangle, en vous donnant la longueur de ses côtés. Vous utilisez alors le théorème de Pythagore : a²+b²= c² ? votre triangle est donc rectangle. Opération mécanique, qu'un ordinateur ferait aussi bien que vous. Et d'ailleurs, pourquoi pas ? Imaginez un programme : nous avonc que c'est une machine, qui accepte des données en entrée (ici, les longueurs des côtés) et renvoie un résultat en sortie (ici, si le triangle est rectangle ou pas). Quel rapport entre ce programme et le théorème de Pythagore ?

Pythagore a fait la démonstration de son théorème dans le cas général ; c'est d'ailleurs pourquoi on l'appelle théorème : pour tout triangle, si les côtés vérifient l'égalité suivane, alors ce triangle est rectangle. La démonstration de ce théorème part des axiomes de la géométrie (les règles fondamentales, définies par Euclide) et, en enchaînant des déductions logiques, arrive à la conclusion. Pour n'importe quel triangle.

Et si maintenant je choisissais un triangle particulier ? Un bon vieux triangle dont je connais les dimensions. Et si je refaisais exactement la même preuve que ce bon vieux Pythagore, mais en remplaçant partout a par la taille du premier côté, b par celle du deuxième et c par celle du troisième ? Alors j'obtiendrais une démonstration dans le cas particulier de mon triangle. C'est tout à fait idiot : si j'ai démontré mon théorème, c'est pour pouvoir l'utiliser une bonne fois pour toute. Si je refais la démonstration pour chaque particulier, à quoi bon avoir démontré le théorème ? A quoi bon ?

En étudiant ces questions, messieurs Curry, de Bruijn et Howard se rendirent compte qu'il y avait un rapport étonnant entre un programme informatique et une démonstration mathématique. En réalité, ils réalisèrent (chacun dans leur coin) qu'on peut passer de l'un à l'autre, à tel point qu'on peut (presque) aller jusqu'à dire qu'un programme informatique est la démonstration d'un théorème.

Reprenons notre exemple : le programme qui nous dit si un triangle est rectangle peut être écrit dans un langage (qu'on appelle le lambda calcul) qui traduit exactement la démonstration du théorème de Pythagore. Que se passe-t-il quand j'exécute mon programme ? Je lui donne en entrée des valeurs particulières, correspondant au triangle que je veux tester. A ce moment-là, mon programme refait toute la démonstration du théorème dans le cas particulier que je lui fournis, comme tout à l'heure. Le programme, c'est la preuve du théorème. L'exécution du programme, c'est son application.

Certains penseront sans doute que ce programme est inefficace : quoi ! refaire toute la démonstration pour chaque triangle ? Il y a deux avantages à souligner : d'abord, avec cette méthode, on est absolument certain que notre programme est correct. Il ne s'agit pas d'un bout de code écrit au hasard, qui coïnciderait peut-être par hasard avec le théorème de Pythagore : c'en est la démonstration, donc la preuve irréfutable et vérifiable. Ensuite, une fois que l'on dispose de la preuve, l'écriture du programme est totalement automatique. Nul besoin de traduire quoi que ce soit : en démontrant le théorème, j'ai créé le programme. Et chaque exécution de mon programme sera une preuve de sa propre validité.

Pour revenir sur l'efficacité, il est évidemment possible de simplifier le programme résultant, au moment de l'extraire du théorème. Plus généralement, j'ai présenté ici ce que l'on appelle l'isomorphisme de Curry-de Bruijn-Howard sous une forme très simplifiée, afin de donner une idée des mécanismes qui entrent en jeu. Dans la vraie vie, c'est à la fois plus évolué, plus efficace, mais aussi beaucoup plus compliqué. Parce que j'ai oublié de vous dire, c'est qu'il existe des théorèmes qui parlent d'objets qu'on ne peut pas calculer, de propriétés qui ne sont ni vraies ni fausses, ou encore des programmes qui ne s'arrêtent jamais... Ce sera pour une prochaine fois.

Tout commentaire ou question pour améliorer cette présentation est le bienvenu : blog@kerneis.info.