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 : a2+b2= c2 ? 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.
Envoyer un commentaire (par mail).