Y a-t-il des programmes pour tout faire ? Que peut-on calculer ? Que ne pourra-t-on jamais calculer ? C’est à ces questions théoriques que des pionniers de l’informatique comme Turing et Church ont répondu au milieu des années 1930 en bénéficiant des apports du logicien Kurt Gödel.
I. Les problèmes de Hilbert
En 1900, un des plus grands mathématiciens de l’époque, David Hilbert (1862-1943) énonce ce que l’on appellera plus tard le « Programme de Hilbert », à savoir une liste des 23 plus grands problèmes qui, selon lui, restaient à résoudre en mathématiques.
Le programme de Hilbert adopte une démarche formaliste qui postule que toute théorie mathématique est fondée sur des axiomes considérés comme vrais a priori et que toutes les vérités de la théorie, les théorèmes, doivent être démontrés en un nombre fini d’étapes de manière mécaniquement vérifiable (par un algorithme).
II. La logique implacable de Gödel
En 1930, un jeune mathématicien autrichien, Kurt Gödel (1906-1978), met fin au rêve formaliste de Hilbert et démontre son premier théorème d’incomplétude qui stipule que dans toute axiomatique des mathématiques contenant au moins les axiomes de l’arithmétique, il existe des propositions vraies mais qui sont indémontrables dans la théorie.
Ce théorème fait l’effet d’un coup de tonnerre dans le petit cercle des mathématiciens mais dépasse rapidement ce cadre et affecte aussi grandement l’informatique naissante, influençant notamment des mathématiciens comme Alonzo Church et Alan Turing.
Kurt Gödel
De manière très schématique, la preuve de Gödel consiste – à travers un codage numérique des propositions et de la véracité mathématique – à construire, au sein de la théorie, une proposition P du style « Je ne suis pas démontrable ».
Cette proposition mène à une conclusion inattendue. En effet, si nous supposons P fausse, alors cela signifierait « Je suis démontrable » et donc P serait vraie ! C’est impossible, donc P est à la fois vraie et indémontrable.
III. Le problème de la décision et celui de l’arrêt
David Hilbert formula un nouveau problème en 1928 : le problème de la décision ou Entscheidungsproblem en allemand. La question est « Y a-t-il un algorithme qui, étant donné un système formel et une proposition logique dans ce système, pourra décider sans ambiguïté si cette proposition est vraie ou fausse dans le système formel ? »
En 1936, Alonzo Church (1903-1995) et Alan Turing montrent de manière indépendante que la réponse à cette question est négative.
Alan Turing (1912-1954) est un mathématicien anglais. Il présente sa machine en 1936, rebaptisée « machine de Turing » par son directeur de thèse Alonzo Church. Cette machine n’a pas de finalité pratique bien qu’elle ait été réellement fabriquée et que de nombreux simulateurs existent. C’est plutôt une machine conceptuelle qui permet d’expliciter de manière précise ce qu’est un programme et de présenter de manière rigoureuse des algorithmes de tous genres, de trouver des limites à ce qui est calculable et de permettre l’exploration systématique de la complexité algorithmique à travers un modèle simple et non ambigu de calcul.
Alan Turing
Turing pose alors le problème suivant : « Existe-t-il un programme qui, prenant en entrée un autre programme et son entrée, determine si ce programme finit par s’arrêter avec cette entrée ou boucle indéfiniment ? »
Il répond par la négative et montre que ce problème de l’arrêt répond aussi au problème de la décision. Church propose une preuve indépendante du même résultat grâce à son formalisme du λ-calcul.
Turing participe ensuite au décodage des messages allemands envoyés notamment à leur flotte sous-marine et codé avec l’Enigma, puis à la conception et la programmation des premiers ordinateurs anglais fondés sur l’architecture de von Neumann. Il propose aussi les premières méthodes de preuve de correction de programme. Il s’intéresse ensuite à l’IA en proposant notamment le Test de Turing puis à la morphogenèse en expliquant l’origine de certaines formes chez l’animal ou le végétal.