Vous allez voir aujourd'hui que l'informatique théorique a des liens étroits avec la logique mathématique.
Vous êtes ici dans la partie "programmation avec Python". Que vient donc faire la logique mathématique dans cette partie ?
Nous allons parler aujourd'hui de ce qu'un algorithme (et donc un programme réel) peut faire ... ou pas. L'une des premières choses à faire lorsqu'on vous demande de réaliser quelque chose est de s'assurer que la tâche demandée est réalisable à l'aide d'un algorithme.
Mais, ca veut dire quoi "réalisable algorithmiquement" ?
Comment peut-on savoir qu'on ne pourra pas trouver de solution avant d'avoir cherché ?
Après tout, peut-être qu'en cherchant plus longtemps, on finirait par trouver, non ?
A - Algorithme : une notion vague avant le 19e siècle
La notion d'algorithme est utilisée depuis très longtemps. Nous avons vu en 1er, que dès l'Antiquité, certains résultats et calculs pouvaient être déterminés en utilisant ces fameux algorithmes.
Pourtant la définition d'un algorithme est restée pendant très longtemps assez vague : une sorte de recette de cuisine pour certains, un ensemble d'instructions élémentaires pour d'autres...
Jusqu'au début du siècle dernier, bien peu de personnes soupçonnaient que l'on pourrait réellement préciser la notion d'algorithme.
B - Apparition de la logique mathématique
Avant de voir ce travail de formalisation de l'algorithme aboutir, il a fallu que la logique mathématique soit elle même formalisée à la fin du 19e siècle.
La logique mathématique est la branche des mathématiques qui s'intéresse aux mathématiques en tant que langage : la façon dont on formalise un énoncé mais aussi la façon dont on construit une démonstration.
Ce travail est le résultat d'un ensemble de recherches issues de plusieurs directions différentes :
en 1847, George Boole publie les bases de l'algèbre qu'on nomme maintenant l'algèbre booléen (a ET b revenant à a.b, a OU b revenant à a+b comme vu en première approche en 1er...)
en 1847, Auguste De Morgan publie ses propres travaux (dont les fameuses formules a+b = a . b..., rapidement vues en 1er également...)
leurs travaux vont servir de base à ce qui va devenir une nouvelle branche des mathématiques : la logique mathématique. Gottlob Frege va clarifier et formaliser le raisonnement logique en 1879; notamment la logique des relations.
les mathématiciens Gottlob Frege, Bertrand Arthur William Russell, Giuseppe Peano et David Hilbert vont travailler à donner une fondation axiomatique des mathématiques.
Chaque branche des mathématiques possède son propre sujet d'étude. Ainsi l'arithmétique peut être vue comme la théorie des nombres par exemple. On doit la définir par un ensemble précis de propriétés qu'on décide comme étant des vérités. On les nomme des axiomes. Voici les trois premiers axiomes de l'arithmétique (exprimés en français plutôt que sous forme d'équations) :
L'élément appelé zéro et noté 0 est un entier naturel.
Tout entier naturel n a un unique successeur, noté s(n) ou Sn qui est un entier naturel.
Aucun entier naturel n'a 0 pour successeur.
...
en 1929, Kurt Gödel prouve le théorème de complétude : toute formule d'une théorie mathématique axiomatique qui est vraie est démontrable dans le cadre de cette théorie. On pense alors qu'on va pouvoir un jour trouver la théorie mathématique ultime, celle qui permettra de tout démontrer !
en 1931, ce même Kurt Gödel va publier ses deux théorèmes d'incomplétude montrant que pour toute théorie mathématique comportant l'arithmétique de base :
une théorie mathématique complète utilisant l'arithmétique de base (une théorie qui permet de démontrer que toute proposition P est VRAIE ou FAUSSE) est nécessairement une théorie incohérente : dans cette théorie, on peut prouver qu'une proposition est VRAIE en utilisant une démonstration et FAUSSE en utilisant une autre démonstration !
Pour être utilisable, une théorie doit donc être incomplète : il y existe certaines propositions P indécidables. Des formules qu'on ne peut ni démontrer (prouver que P est VRAIE), ni réfuter (prouver que P est FAUSSE) dans le cadre de cette théorie.
Pourquoi ? Simplement car une théorie est juste un ensemble d'axiomes. Or, ces axiomes s'appliquent à plusieurs modèles, plusieurs interprétations. Lorsqu'une formule est prouvable, elle l'est via les axiomes de la théorie et doit donc vraie dans tous les modèles possibles à partir de cette théorie.
Et c'est le problème avec la théorie de l'arithmétique : ses axiomes caractérisent l'ensemble des entiers naturels mais également des ensembles d'entiers "exotiques" légèrement différents. Et certains formules semblant vraies sur les entiers naturels (lorsqu'on utilise cette formule, les tests disent toujours que c'est vrai) ne sont pas vérifiées avec ces autres entiers "exotiques".
Lorsqu'une formule sur les entiers semble bonne mais qu'on a pas réussi encore à la démontrer définitivement, 3 possibilités :
On peut finir par trouver la démonstration et on montrera qu'elle est valide.
On peut finir par trouver un contre-exemple dans les entiers : la formule n'est pas valide, c'est juste que les exemples la mettant en défaut ne sont pas si courants que cela.
Elle est indécidable pour cette théorie. Par exemple, elle est "vraie" sur les entiers naturels mais pas sur tous les modèles exotiques d'entiers : on ne parviendra donc jamais à la démontrer ET on ne trouvera jamais de contre-exemples la mettant en défaut... Une proposition est donc indécidable s'il existe des modèles de la théorie où les tests donnent une conclusion et d'autres modèles où les tests donnent l'inverse. On ne pourra alors pas utiliser cette théorie pour aboutir à une conclusion sur cette propriété en particulier.
Moralité, si une formule semble bonne mais qu'on ne parvient pas à trouver de démonstration, on ne peut pas savoir si on parviendra un jour à prouver le cas 1 ou 2 ou si on est dans la cas 3.
Idem avec une formule qui semble toujours fausse mais dont on ne parvient pas à trouver de réfutation définitive.
Malheureusement, Gödel démontre également que déterminer si une théorie est incohérente est justement une formule indécidable. Il n'existe donc pas de prédicat permettant de savoir si une théorie est incohérente ou pas dans le cadre de cette théorie. C'est le fait de tomber, un jour, par hasard, sur une incohérence qui va lui donner un statut de théorie incohérente...
Tout ceci va permettre de redonner des bases stables et solides aux mathématiques : les mathématiciens ont pu se mettre d'accord sur un nombre limité d'axiomes pour chaque théorie.
Assez pour obtenir une théorie solide mais... incomplète. Ainsi, l'arithmétique caractère les entiers naturels, mais pas que cet ensemble.
Pas trop pour espérer ne pas travailler sur une théorie qu'on découvrira un jour incohérente.
Seuls les non mathématiciens pensent que c'est la fin des mathématiques. Depuis cette époque, on n'a jamais trouvé d'exemples montrant l'incohérence de l'arithmétique. Et si il s'avérait que ce soit le cas, il suffirait sans doute de modifier quelques axiomes. Et suffirait alors d'identifier les théorèmes qui ne seraient plus démontrables, ceux qui avaient besoin de cet axiome spécifique par exemple.
Après ce petit détour par les théories mathématiques, revenons à l'informatique.
D'abord, notez bien qu'on retrouve une notion que vous connaissez très bien : tester un algorithme ne revient pas à prouver un algorithme. Un jeu de tests d'un milliard de cas ne remplace pas une preuve de correction (sauf si vous parvenez alors à tester tous les cas possibles bien entendu : c'est alors une démonstration par cas).
C - La définition de l'algorithme et de la calculabilité
Le travail de formalisation de l'algorithme fut effectué en plusieurs étapes de 1931 à 1936 notamment par :
Image par : Konrad Jacobs, Erlangen, Copyright is MFO, CC BY-SA 2.0 DE <https://creativecommons.org/licenses/by-sa/2.0/de/deed.en>, via Wikimedia Commons"
Alan Turing
Image du domaine public
Kurt Godel.
Image du domaine public
De façon à caractériser l'arithmétique et le calcul, ils vont chercher à trouver ce qu'est le calcul justement. Plusieurs moyens de formaliser (définir mathématiquement) ce qu'est une fonction calculable vont être trouvés :
Les fonctions récursives sont utilisées dans le cadre théorique de modèle de calcul par Kurt Godel, notamment dans ses théorèmes d'incomplétude. Mais, sont-elles vraiment l'outil le plus adapté pour le calcul ? Calculent-t-elles tout ce qui est calculable ?
Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church. Il est basé fondamentalement sur le concept de fonction et formalise assez simplement la notion de calcul.
Sans rentrer dans les détails, voici la façon dont on écrit la fonction successeur en λ-calcul :
λx.x+1 : cette codification veut dire que notre fonction attend de recevoir un argument x et qu'elle renvoie alors x+1. C'est bien la fonction successeur.
La machine de Turing est un modèle abstrait du fonctionnement des appareils mécaniques de calcul créé par Alan Turing dans le but de définir précisément ce qu'est un algorithme et ce que représente la complexité d'un algorithme. Il ne s'agit pas d'une machine réelle mais plutôt d'une définition la plus épurée possible de ce que doit faire une machine qui calcule. Sa simplicité permet en réalité de réalité de réaliser des démonstrations sur ce qui est calculable, ou pas.
Stephen Kleene va tenter de montrer l'équivalence entre les fonctions récursives, le λ-calcul, et la machine de Turing. Cela va aboutir à la thèse de Church-Turing qui énonce (sans le démontrer) que toutes ces 3 méthodes de calcul "mécanique" (machine de Turing, λ-calcul et récursivité) sont équivalentes et peuvent toutes calculer les mêmes fonctions. Ces trois techniques ont donc la même "puissance prédictive". Si l'une d'entre elles parvient à réaliser un calcul, on pense que les autres le peuvent aussi.
Tous les tests jusqu'à présent ont montré cette équivalence. Mais tester, n'est pas prouver.
1.1 Calculabilité
Calculabilité "mécanique"
La calculabilité est définie comme tout traitement
issu d'un système physique de calculs (qu'on assimilera à une machine de Turing pour préciser la notion)
répondant après un nombre d'étapes fini (et donc un temps fini)
en utilisant un jeu fini d'instructions
Le point 1 contenant le terme "système physique de calculs" posait problème dans le cadre d'une définition mathématique. C'est en partie pour cela que Turing a développé sa fameuse machine : de cette façon, il est parvenu à formaliser mathématiquement ce qu'est un système physique de calculs. On a déterminé le caractère universel de cette machine : elle peut émuler le comportement de n'importe quel autre système de calculs connus et est facilement représentable théoriquement.
Vue d'artiste de la machine de Turing (domaine public, publié sur Wikipedia)
Thèse de Church
La thèse de Church élargit la définition au λ-calcul, à la récursivité et à tout langage de programmation Turing-complet (comme Python) : si Python peut effectuer un calcul, une machine de Turing également. Et inversement.
Calculable et Non Calculable
Cette définition de fonction calculable engendre donc naturellement la notion de fonction non calculable.
Sans entrer dans les détails de la démonstration, disons qu'il n'existe qu'un nombre limité d'algorithmes qui sont les combinaisons obtenues en prenant X mots dans l'alphabet du langage considéré contenant Y symboles. Avec un langage comportant 1000 symboles et un programme contenant 400 de ces symboles, on a 1000400 programmes différents (dont la plupart ne fonctionneront pas !). Un nombre fini, très grand, mais pas infini.
Or, les fonctions (même en ne considérant que les fonctions ayant un argument entier naturel et renvoyant un entier naturel) sont plus nombreuses ! Par conséquent, on ne pourra jamais calculer l'infinité des problèmes possibles à l'aide d'un programme de taille finie. Or, un programme de taille infinie ne peut pas répondre puisqu'il faudrait un temps infini pour exécuter son infinité d'instructions.
Une fonction calculable est une fonction pour laquelle on aura une réponse au bout d'un temps fini, quels que soient les arguments valides envoyés(c'est à dire respectant types et préconditions).
ENTREES VALIDES ➔ FONCTION CALCULABLE ➔ Fournit toujours une réponse
Une fonction non calculable est une fonction pour laquelle on aura parfois une réponse au bout d'un temps fini pour certains paramètres, et parfois aucune réponse car le calcul va provoquer une boucle infinie même avec des paramètres respectant les préconditions.
ENTREES VALIDES ➔ FONCTION NON CALCULABLE ➔ Peut founir une réponse OU boucler à l'infini
Bien entendu, impossible de prévoir à l'avance quelq sont les entrées qui génèrent une boucle infini.
Lorsque le programme ne fournit pas sa réponse et que vous trouvez le temps long, vous devez prendre une décision :
On le stoppe ? Mais il va peut-être répondre un jour !
On le laisse travailler ? Mais il est peut-être déjà en train de boucler à l'infini !
Bref, elles sont non calculables car elles ne rendent pas systématiquement la main. On ne peut pas les utiliser sans danger dans un système car elles peuvent, parfois, créer une boucle infinie.
To compute, computability, computer
On notera qu'en anglais la calculabilité se nomme computability ; on comprend bien le lien avec "computer", là où le mot "ordinateur" ne montre pas aussi bien le lien évident entre les deux notions.
1.2 Définition d'Algorithme
Définition plus formelle d'Algorithme
Un algorithme peut maintenant être défini comme un ensemble d'instructions réalisables par un système physique de calcul et répondant donc aux critères de la calculabilité.
Algorithme et calculabilité sont donc intimement liés.
Python est Turing-compatible
Comme vous ne connaissez pas la machine de Turing mais que Python est Turing-compatible, nous pouvons en déduire que tout ce qui est calculable avec Python est calculable par un algorithme. Et inversement.
Vous saviez déjà qu'un algorithme est assimilable à une fonction : on lui donne des ENTREES sur lesquelles il travaille et pour lesquelles il fournit une SORTIE. Vous devriez maintenant comprendre qu'il ne s'agit pas juste d'une similitude mais d'une réelle équivalence.
ENTREES ➔ ALGORITHME ➔ SORTIE
ENTREES ➔ FONCTION ➔ SORTIE
Cette remarque vise à rappeler ce que vous avez déjà vu de nombreuses fois : un algorithme doit résoudre une classe de problèmes et pas uniquement une instance particulière d'un problème. Si votre "algorithme" ne sait gérer qu'un énoncé unique aux valeurs fixées et pas tout un ensemble d'énoncés, il ne s'agit pas vraiment d'un algorithme.
1.3 Théorie de la calculabilité
Lors de vos études supérieures, vous verrez peut-être que cette théorie ne vise pas juste à distinguer les fonctions calculables et les fonctions non calculables.
Elle vise aussi à les classifier, à savoir par exemple s'il existe des fonctions non calculables encore plus non calculables que d'autres !
Le lien avec la calculabilité est immédiat : un problème est décidable s'il existe une fonction calculable qui décide par Oui / Non de la réponse à la question posée par le problème.
Définition générale : un problème de décision est décidable s'il existe une machine de Turing qui termine et répond Vrai ou Faux sur n'importe quelle instance du problème.
Définition NSI : un problème de décision est décidable s'il existe une fonction-prédicat Python qui termine et répond True ou False sur n'importe quelle instance du problème.
Exemple
Le problème suivant est un problème décidable algorithmiquement "Un entier naturel x est-il un nombre premier ?". De façon naïve, il suffit de tester sa division euclidienne par tous les entiers compris entre 2 et lui-même. Si le reste vaut 0 à un moment, c'est qu'il ne s'agit pas d'un nombre entier.
On peut donc créer une telle fonction :
1
defest_premier(n:int)->bool:
Voici la résolution naïve (voir l'activité sur les corrections de bugs parlant un peu de RSA pour des versions plus efficaces) :
Décidable ne veut pas dire FACILE. Un problème décidable peut être FACILE ou DIFFICILE. Dans ce dernier cas, on pourra alors le résoudre en théorie mais pas concrètement si les données seront importantes.
Même un problème décidable peut donc s'avérer impossible à résoudre en pratique.
2.2 Indécidabilié algorithmique
Tous les problèmes ne sont pas décidables.
Définition
Les problèmes indécidables sont ceux pour lesquelles on ne peut pas créer de programmes capables de répondre systématiquement OUI ou NON pour chacune des instances possibles du problème.
Certains problèmes indécidables sont un peu plus "faciles" que les autres mais ils n'en restent pas moins indécidables :
Ceux qui terminent toujours lorsque la réponse est OUI et qui, sinon, peuvent soit répondre NON, soit BOUCLER. On dit parfois qu'ils sont semi-décidables.
Ceux qui terminent toujours lorsque la réponse est NON et qui, sinon, peuvent soit répondre NON, soit BOUCLER.
Ils restent indécidables car si la réponse n'arrivent pas, vous ne savez pas s'ils bouclent ou s'ils sont dans la catégorie qu'ils savent gérer et vont finir par répondre.
Les plus "complexes" ne savent gérer systématiquement ni le OUI, ni le NON.
Gérer un problème indécidable ?
Dire qu'un problème est indécidable algorithmiquement ne veut pas dire qu'on ne peut pas trouver de solution à des instances particulières du problème. Cela veut dire que parfois on va boucler à l'infini, sans savoir qu'on est parti à l'infini !
Lorsque le programme ne fournit pas sa réponse et que vous trouvez le temps long, vous devez prendre une décision :
On le stoppe ? Mais il va peut-être répondre un jour !
On le laisse travailler ? Mais il est peut-être déjà en train de boucler à l'infini !
Globalement, si on sait que notre problème est indécidable, inutile de tenter de le gérer tel quel, il faut le rendre plus simple. Deux approches de simplification :
modifier la réponse attendue, en lui demandant d'être moins précise. On aura alors un problème légèrement différent mais c'est parfois mieux que rien.
réduire le domaine d'application. On se restreint à un certain type d'instances en entrée. On aura alors (peut-être) un algorithme applicable mais sur un domaine moins large.
Le principe est donc de répondre à un problème moins général mais décidable.
2.3 Hors programme : indécidabilité logique
L'indécidabilité algorithmique et l'indécidabilité logique sont deux notions différentes (mais elles ont un lien interne bien entendu).
En algorithmique, les algorithmes résolvent des instances d'un problème. Les entrées du problème sont donc variables et dépendent de l'instance. Pas d'histoire de théorie mathématique ici (du moins de façon apparente).
Un problème indécidable algorithmiquement est un problème pour lequel l'algorithme boucle parfois à l'infini et ne répond jamais.
Il s'agit donc de savoir :
si on peut trouver la réponse à
un problème aux entrées variables
en utilisant des actions basiques.
En logique, un énoncé est une propriété mathématique dont la description est totalement définie, aucune variable libre.
Un énoncé logique indécidable est un énoncé d'un théorie mathématique bien définie qu'on ne pourra jamais démontrer ou réfuter dans le cadre de cette théorie, car ses axiomes ne permettent pas de trancher.
Il s'agit de savoir :
si on peut trouver une démonstration (dire OUI) ou une réfutation (dire NON) à
un problème figé (un énoncé)
en utilisant les axiomes et théorèmes de la théorie considérée.
Nous allons voir et démontrer l'indécidabilité de l'un des problèmes indécidables les plus connus : le problême de l'arrêt d'un programme.
3.1 Démonstration par l'absurde
Vous avez vu plusieurs façons de réaliser des démonstrations :
La démonstration directe en utilisant l'implication
La démonstration par cas qui liste tous les cas possibles et prouve sur chaque cas qu'on obtient bien la réponse attendue
La démonstration par récurrence (initialisation, hérédité, conclusion à l'infini)
La preuve de correction d'un algorithme (initialisation, conservation, conclusion sur le cas final)
La démonstration par l'absurde
Le principe de la démonstration par l'absurde est le suivant :
On veut établir une preuve sur une propriété P.
On sait qu'une démonstration mathématique ne peut montrer l'absurde en partant de choses valides car, par construction, la logique mathématique est conçue pour préserver la vérité.
On fait l'hypothèse que NON P est valide.
On utilise cette hypothèse dans un raisonnement soigneusement conçu où tout le reste est parfaitement valide et démontré.
On espère aboutir à une contradiction logique.
Puisque la démonstration mathématique préserve la vérité et que le seul point douteux est l'hypothèse de départ, on peut en déduire que l'hypothèse de départ sur la propriété est fausse et qu'elle vaut l'inverse.
Si (NON P implique l'absurde) alors P.
3.2 Problème de l'Arrêt
Présentation informelle
Nous avons vu que algorithme, programme, fonction, machine de Turing ont le même pouvoir de déduction. On utilisera donc ici de façon totalement interchangeable programme et fonction par exemple. C'est pareil.
De façon informelle, on peut décrire le problème de cette façon : "Existe-il un programme capable de prédire l'arrêt de n'importe quel autre programme lancé sur des données quelconques mais connues ?"
Nous allons voir que ce problème de l'arrêt est indécidable : on ne peut pas créer un programme capable de prédire automatiquement si un autre programme dont on connaît le code-souce et les entrées va s'arrêter ou boucler à l'infini.
Les mathématiciens Church et Turing ont prouvé que ce problème est indécidable avant même l'apparition réelle des ordinateurs.
Formalisation sous forme d'une fonction Python
De façon plus formelle : peut-on créer une fonction arret() qui soit capable de prédire qu'une autre fonction quelconque f va s'arrêter un jour. La fonction arret() possède deux paramètres lui permettre de faire son analyse :
le paramètre f reçoit le code-source de la fonction qu'on veut étudier et
le paramètre e reçoit les entrées sur lesquelles f devra travailler.
La thèse de Church-Turing nous dit que cela revient à se demander si cette fonction Python peut exister :
1
2
3
4
defarret(f:code_source,e:données)->bool:"""Prédicat qui renvoie True si f(e) s'arrêtera et répondra un jour"""if l'analyse prédit que f(e) s'arrêtera : returnTrueelse:returnFalse
On profite ici du fait que Python accepte de ne pas passer à la ligne après if ou else si il n'y a qu'une seule instruction à réaliser. Evitez de le faire mais cela va permettre ici d'avoir une vision plus condensée des actions réalisées.
Arret analyse sans exécuter
Il faut bien comprendre que le code-source de f n'est pas réellement exécuté par arret() : il s'agit de créer une fonction qui analyse le code-source et l'entrée fournie de l'autre fonction.
Si vous créez une fonction qui lance réellement f(e) et qui répondra Vrai si f(e) lui répond un jour, il est évident qu'elle ne parviendra pas à répondre si f(e) ne lui rend jamais la main.
3.3 Création d'une fonction inv()
Fonction inv qui inverse la prédiction
Voici le code-souce parfaitement valide d'une fonction inv() qui utilise à l'interne la fonction arret() :
1
2
3
4
5
6
defboucler():whileTrue:passdefinv(f:code_source)->True:ifarret(f,f):boucler()# Si f(f) va répondre, inv() boucleelse:returnTrue# Si f(f) va boucler, inv() renvoie True
Aucune erreur de programmation, c'est bien une fonction totalement correcte. Elle se nomme inv() car :
L05 : si arret prédit que f(f) s'arrêtera alors inv(f) tourne en boucle .
L06 : sinon, si arret prédit que f(f) s'arrêtera alors inv(f) s'arrête en répondant True.
C'est pas bizarre f(f) ?
On lance arret() en lui donnant f et f comme arguments. Cela veut dire qu'on lui demande si la fonction f va s'arrêter lorsqu'elle travaillera avec l'appel sur son propre code-source : f(f).
Ca n'a rien de bizarre :
On peut demander à un programme anti-virus de vérifier son propre code-source.
On peut demander à un compilateur C de compiler son propre code-source.
On peut demander à un programme de compression de comprimer son propre code-source.
...
3.4 Démonstration par l'absurbe de l'indécidablité de l'Arrêt
Nous allons montrer que Arrêt est un problème indécidable et qu'on ne peut donc pas créer en Python le prédicat arret() décrit en 3.2 : elle ne peut pas systématiquement répondre oui ou non.
Pour cela, nous allons utiliser une démonstration par l'absurde.
a. Hypothèse de départ
On fait l'hypothèse que Arrêt est décidable. Sous cette hypothèse, on peut avoir à disposition un prédicat arret() tel que décrit ci-dessous :
1
2
3
4
defarret(f:code_source,e:données)->bool:"""Prédicat qui renvoie True si f(e) s'arrêtera et répondra un jour"""if l'analyse prédit que f(e) s'arrêtera : returnTrueelse:returnFalse
b. Recherche d'une utilisation d'arret() menant à une absurdité
Nous allons construire un programme totalement valide, si ce n'est qu'on doit considérer que arret() existe et fonctionne.
Regardons ce qui va se passer si on fait l'appel suivant en ligne 17 :
arret(inv, inv)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# Déclaration des fonctionsdefboucler():whileTrue:passdefinv(f:code_source)->True:ifarret(f,f):boucler()# Si f(f) va répondre, inv() boucleelse:returnTrue# Si f(f) va boucler, inv() renvoie Truedefarret(f:code_source,e:données)->bool:"""Prédicat qui renvoie True si f(e) s'arrêtera et répondra un jour"""if l'analyse prédit que f(e) s'arrêtera : returnTrueelse:returnFalse# Programme principalprint ( arret(inv, inv))
On se demande donc si la fonction inv() s'arrête lorsqu'elle travaille sur son propre code-source. Cela revient mentalement à avoir quelque chose comme ceci :
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# Déclaration des fonctionsdefboucler():whileTrue:passdefinv(f:code_source)->True:ifarret(f,f):boucler()# Si f(f) va répondre, inv() boucleelse:returnTrue# Si f(f) va boucler, inv() renvoie Truedefarret(f=inv:code_source,e=inv:données)->bool:"""Prédicat qui renvoie True si f(e) s'arrêtera et répondra un jour"""if l'analyse prédit que inv(inv) s'arrêtera : returnTrueelse:returnFalse# Programme principalprint ( arret(inv, inv))
Encore une fois, rien d'étrange pour le moment.
Regardons maintenant ce que va donner la fonction inv() lorsqu'elle travaillera sur son propre code-source, comme sur la ligne 12.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# Déclaration des fonctionsdefboucler():whileTrue:passdefinv(f=inv:code_source)->True:ifarret(inv,inv):boucler()# Si inv(inv) va répondre, inv() boucle !else:returnTrue# Si inv(inv) va boucler, inv() répond !defarret(f=inv:code_source,e=inv:données)->bool:"""Prédicat qui renvoie True si f(e) s'arrêtera et répondra un jour"""if l'analyse prédit que inv(inv) s'arrêtera : returnTrueelse:returnFalse# Programme principalprint ( arret(inv, inv))
Cela revient à écrire ceci en explicitant le code en français :
6
7
8
Sur un appel d'inv sur son propre code-source:
Si arrêt prédit que inv(inv) va s'arrêter, inv(inv) boucle sur son appel réel
Sinon, si arrêt prédit que in(inv) va boucler, inv(inv) répond et s'arrête lors de l'appel réel
Nous aboutissons donc à une contradiction : on fait l'hypothèse que le prédicat arret() existe et fonctionne et il prédit l'inverse de ce qu'il doit répondre.
Conclusion de la démonstration
Nous avons fait l'hypothèse de l'existence du prédicat arret() et cela nous a permis de créer un programme totalement rigoureux, à part cette hypothèse.
Cela mène à une contradiction.
L'hypothèse de départ ne peut donc pas être bonne, elle est donc fausse (tiers exclu : c'est soit vrai, soit faux).
Il n'est pas possible de créer un prédicat qui prédit Arret.
Arret est donc un problème indécidable.
4 - Conclusion
Nous avons fait l'hypothèse de l'existence d'une fonction arret capable d'analyser le code de n'importe quel autre programme ou fonction pour savoir si il va s'arrêter et répondre sur l'entrée qu'on lui propose
l'utilisation de cette hypothèse associée à d'autres raisonnements corrects eux mène à une incohérence, un résultat absurde.
Cela veut donc dire que notre hypothèse de départ n'est pas bonne et qu'il n'existe pas de programme ou fonction arret capable d'analyser le code de n'importe quel autre programme ou fonction pour savoir si il va s'arrêter et répondre sur l'entrée qu'on lui propose.
Prenons quelques minutes pour voir ce qu'est cette fameuse machine de Turing même si aucune connaissance n'est attendue à ce sujet dans le programme. Cela vous permettra de comprendre ce qu'on entend par "machine physique".
4.1 Machine de Turing
Il s'agit donc d'une machine composée fondamentalement des éléments suivants :
Un ruban (supposé infini s'il le faut) comportant des cases dans lesquelles on peut écrire des valeurs issues d'un ensemble fini A de valeurs permises à définir. Je prendrais ici A = {∅, 0, 1} par exemple (A comme alphabet).
Une tête de lecture se plaçant au dessus du ruban et capable :
de lire et modifier le contenu de la case actuelle au dessous de laquelle elle se trouve,
de se déplacer à droite ou à gauche de la case actuelle
de lire et modifier une mémoire définissant son état. Elle peut prendre une valeur dans un ensemble fini T d'états. Par exemple T = {'init', 'travail', 'fini'}.
Une table de transition (accessible depuis la tête) permettant de déterminer l'action à réaliser en fonction de ce que contient la case actuelle et la mémoire des états. Par exemple :
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Avec la combinaison (ETAT=INIT, LECTURE=0), on trouve l'instruction désignée dans le tableau (la case du milieu en haut), et on déduit qu'on doit placer ETAT sur TRAVAIL, écrire 0 dans la case (donc on ne fait rien) et se déplacer à droite.
Arrêt : une machine de Turing s'arrête si elle tombe sur une combinaison (état, lecture) qui n'est pas possible dans sa table de transition.
Ici, on voit qu'elle ne possède pas d'instructions à réaliser si l'état est FINI. Elle stoppera donc lorsqu'elle aura atteint cet état.
4.2 Exemple de Machine de Turing
Imaginons un ruban portant notamment des cases vides et une tête de lecture située sur l'une d'entre elles :
Notre ruban contient ∅∅010 au début, la droite de ruban est constituée de cases vides uniquement.
init∅∅010∅∅
Pour savoir ce qu'on doit faire, on cherche le couple (ETAT=init, LECTURE=∅) : on laisse INIT et ∅ et on se déplace à droite.
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
La "nouvelle" configuration après la première séquence :
∅init∅010∅∅
On retrouve le couple (ETAT=init, LECTURE=∅) : même action qui la précédente, on laisse INIT et ∅ et on se déplace à droite.
Nouvelle configuration après la deuxième action :
∅∅init010∅∅
Cette fois, on obtient le couple (ETAT=init, LECTURE=0) : on passe à TRAVAIL, on laisse 0 et on se déplace à droite.
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Nouvelle configuration :
∅∅0travail10∅∅
Cette fois, on obtient le couple (ETAT=travail, LECTURE=1) : on laisse TRAVAIL, on laisse 1, et on se déplace à droite.
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Nouvelle configuration :
∅∅01travail0∅∅
Cette fois, on obtient le couple (ETAT=travail, LECTURE=0) : on laisse TRAVAIL, on laisse 0, et on se déplace à droite.
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Nouvelle configuration :
∅∅010travail∅∅
On obtient le couple (ETAT=travail, LECTURE=∅) : on place FINI, on place 0, et on se déplace à droite.
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Nouvelle configuration :
∅∅0100fini∅
∅
0
1
init
Etat ← init Case ← ∅ Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
travail
Etat ← fini Case ← 0 Vers Droite
Etat ← travail Case ← 0 Vers Droite
Etat ← travail Case ← 1 Vers Droite
Et là, nous tombons sur un problème : le couple ('fini', ∅) n'est pas présent dans la table de transition : cette donnée n'est pas interprétable comme une instruction !
Dans ce cas, la machine s'arrête.
On est parti de ce ruban :
∅∅010∅∅
Et on obtient ce ruban :
∅∅0100∅
Le ruban de la machine est passée de 010 (soit 2 en décimal) à 0100 (soit 4 en décimal). Voilà ce que fait la table de transition de cette machine de Turing : elle multiplie par deux l'entier naturel encodé sur le ruban !
Fin sur une "vraie" machine de Turing
Pour parvenir à exécuter des actions à la suite les unes des autres, la Machine doit normalement s'arrêter au début de sa bande, tout à gauche.
Ici, il ne s'agit que d'un exemple rapide mais il faudrait rajouter des états supplémentaires pour parvenir à arrêter la tête de lecture correctement, sur la première case.
En conclusion, cette machine permet donc de formaliser ce que peut ou pas calculer un "système physique".
Puisqu'une machine donnée possède un nombre d'états dénombrables (nombre de cases et états), on est capable de les lister une par une en étant certain de ne pas en oublier une.
Exemple : 2 cases acceptant 0,1 sur le ruban et 2 états 0,1 donne 8 machines :
Etat 0 et Ruban 00
Etat 0 et Ruban 01
Etat 0 et Ruban 10
Etat 0 et Ruban 11
Etat 1 et Ruban 00
Etat 1 et Ruban 01
Etat 1 et Ruban 10
Etat 1 et Ruban 11
Or, nous ne pouvons pas faire la même chose avec les problèmes à résoudre : nous n'obtenons pas un ensemble dénombrable. Cela veut donc dire qu'il existe nécessairement des choses que la machine de Turing (ou, d'après la thèse de Church-Turing, n'importe quel système informatique) ne pourra pas résoudre.
Cette partie doit être vue comme un exposé de culture générale. Il ne s'agit que de vous montrer que la notion de décidabilité a été traitée sérieusement par des gens compétents, pas de le démontrer.
Les notions de décidabilité et d'indécidabilité sont loin d'être évidentes. Vous allez voir d'ailleurs qu'elles ne se limitent pas qu'aux algorithmes et à leurs limitations "physiques".
1 - Axiomes et théories mathématiques axiomatiques
Une théorie mathématique axiomatique est composée d'un ensemble d'axiomes, des propositions à la base de la théorie voulue. On les considère intrinsèquement vraies dans le cadre de la théorie. Ce sont ces axiomes qui définissent l'objet abstrait sur laquelle la théorie travaille.
Important : les axiomes ne doivent pas être contradictoires entre eux bien entendu.
La géométrie Euclidienne dispose de son jeu d'axiomes
L'arithmétique dispose de son jeu d'axiomes
La théorie des ensembles dispose de son jeu d'axiomes
...
L'arithmétique peut ainsi se résumer à un certain nombre d'axiomes. Voici les trois premiers :
L'élément appelé zéro et noté 0 est un entier naturel.
Tout entier naturel n a un unique successeur, noté s(n) ou Sn qui est un entier naturel.
Aucun entier naturel n'a 0 pour successeur.
...
2 - Construire des démonstrations à partir des axiomes
En associant ces axiomes à l'aide de la logique, on peut démontrer de nouvelles propriétés. D'où l'image des legos.
Une propriété valide dans une théorie n'est donc jamais une invention : elle est présente depuis le début. Encore fallait-il savoir comment "l'assembler" pour la démontrer.
Un théorème est une propriété démontrée dont la portée d'utilisation est grande, ce qui justifie le fait qu'il soit reconnu dans le cadre d'une théorie donnée. Beaucoup de propriétés démontrées n'ont pas le statut de "théorèmes".
La démonstration d'une proposition P pourrait donc être représentée comme un Arbre dont
les feuilles sont les axiomes et théorèmes (propriétés déjà démontrées et reconnues), et
la racine est liée à la proposition P qu'on veut démontrer démontrer (aboutir à P est VRAI) ou réfuter (aboutir à NON P est VRAI).
Cet Arbre est un peu particulière puisque pour le réaliser on part des feuilles et on remonte vers la racine qui sera P si on démontre la propriété ou NON P si on la réfute. Les liens de parenté sont établis en utilisant les règles de la logique que nous avons vu (ET, OU, NON, IMPLIQUE...)
Cela devrait vous faire penser à nos algorithmes : des associations d'instructions aboutissant à une réponse.
3 -Le choix des axiomes
Le choix des axiomes à prendre en compte pour rendre chacune des théories "efficaces" est un enjeu majeur.
Une fois les bases de la logique mathématique posées par les travaux de Bool et De Morgan, Frege va clarifier et formaliser le raisonnement logique en 1879 et va dégager trois caractéristiques qu'une théorie mathématique devrait avoir (notez que j'utilise le conditionnel) :
cohérence : impossibilité de démontrer une proposition et son contraire
complétude : à l'intérieur de la théorie, tout énoncé A est
soit démontrable (A est VRAI),
soit réfutable (not A est VRAI)
décidabilité : il existe une procédure de décision permettant de tester tout énoncé de la théorie.
Tout ceci va aboutir à une profonde refondation des mathématiques par les théoriciens de l'époque : la formalisation de la logique mathématique et l'apparition des théories axiomatiques. Grande réussite des mathématiques : son auto-réflexivité lui permet d'étudier des objets qui sont eux-mêmes... les théories mathématiques.
De nombreux théoriciens (dont Hilbert) vont justement tenter de trouver quels axiomes choisir pour chaque théorie de façon à éviter deux problèmes :
Si on sélectionne trop peu d'axiomes comme fondation d'une théorie, on peut aboutir à des situations où certaines propositions (qui pourtant sont bien VRAIES ou FAUSSES) ne sont ni démontrables, ni réfutables : la théorie construite est incompléte : on manque de "briques" pour construire certains raisonnements.
On peut ainsi trouver des énoncés pour lesquels :
alors que la proposition P est vraie pour l'ensemble d'objets qui vous intéresse, on ne parviendra jamais à le démontrer... Pourquoi ? Simplement car il existe au moins un autre ensemble d'objets compatibles avec la théorie étudiée dans laquelle P n'est pas vraie. Dans ce cas, pour votre ensemble, vous ne trouverez jamais de contre-exemples disant que c'est faux, mais en même temps, vous ne pourrez jamais démontrer que c'est vrai ! Il restera donc toujours un petit doute quand on fait qu'on soit bien dans cette situation.
même chose avec une proposition P qui semble fausse dès que vous l'appliquez à votre ensemble d'objets, mais que vous ne parvennez pas à réfuter.
Si on revient à l'image de l'Arbre, cela veut dire qu'on ne parviendra jamais à atteindre P ou NON P en partant des axiomes et théorèmes (propositions démontrées) de la théorie. La théorie ne peut donc pas trancher (ce qui ne veut pas dire que la propriété P n'est pas soit VRAI soit FAUX) appliquée aux objets qui vous intéresse vous.
Si on sélectionne trop d'axiomes comme fondation d'une théorie, il existe des propositions P pour lesquelles on parvient à montrer P avec une démonstration et à réfuter P avec une autre démonstration : la théorie construite est incohérente. Là, c'est l'inverse du cas précédent : on a pris trop de briques sans se rendre compte qu'elles étaient en partie contradictoire.
Situation embarrassante...
C'est une théorie qui prouve tout et son contraire...
A partir du moment où ceci a été clairement établi, plusieurs mathématiciens ont tenté pendant des années d'aboutir au parfait choix d'axiomes, un choix qui permettrait d'aboutir à ceci :
On aurait alors une théorie dans laquelle on pourrait tout démontrer ou réfuter. On pourrait répondre à toutes les énoncés.
Trouver cette théorie parfaite permettrait de pouvoir répondre à n'importe quel énoncé portant sur l'objet d'études de la théorie. Pourvu qu'on parvienne comment la démontrer ou la réfuter. Mais savoir qu'une démonstration ou une réfutation existe serait déjà confortable : on sait au moins qu'on travaille à trouver quelque chose qui existe.
4 - La réponse de Kurt Gödel
Un jeune mathématicien autrichien (naturalisé américain après sa fuite du régime nazi) va alors parvenir à démontrer en 1931 deux théorèmes importants de la logique mathématique.
Le premier théorème d'incomplétude établit qu'une théorie suffisante pour y démontrer les théorèmes de base de l'arithmétique est nécessairement incomplète : certains énoncés seront nécessairement indécidables dans cette théorie. Rappelons que cela signifie simplement qu'on ne pourra jamais les démontrer ou les réfuter dans le cadre de cette théorie.
Le second théorème d'incomplétude va lui établir qu'une théorie cohérente ne peut pas démontrer sa propre cohérence.
Notez bien que cela n'empêche pas les mathématiciens de dormir : ne faites pas dire à ces théorèmes plus qu'ils ne le font. Cela veut juste dire
qu'il existera toujours des énoncés indécidables dans une théorie cohérente
qu'on ne peut pas démontrer qu'une théorie est cohérente même si elle l'est : cela fait partie des énoncés... indécidables de la théorie.
Si les axiomes utilisés pour bâtir les théories reconnues actuelles menaient à des théories incohérentes, quelqu'un aurait bien réussi à trouver un cas problématique. Et même dans ce cas, il "suffirait" sans doute de redéfinir un système d'axiomes un peu plus restreint. Certains choses seraient à revoir, mais pas tout. C'est ce qui s'est passé avec la première version de la théorie des ensembles. Après ajustement, elle n'en est que plus solide.
Attention, il faut bien comprendre que nous parlons ici de l'indécidabilité logique d'un énoncé dans une théorie précise. Il est possible que l'énoncé soit décidable dans le cadre d'une autre théorie.
L'informatique théorique étant l'étude des fondements logiques et mathématiques de l'informatique, on va bien entendu retrouver les mêmes conséquences.
Néanmoins, souvenez-vous de ce qu'on vous a raconté sur les algorithmes : ils ne sont pas conçu pour résoudre un énoncé unique mais toute une classe d'énoncés similaires.
On le résumera en disant qu'un algorithme est concu pour résoudre une classe de problèmes et pas une seule instance du problème.
Et certains problèmes ne seront pas résolvables par un algorithme. On dira que ces problèmes sont indécidables de façon absolue.
5 - L'algorithme de démonstration ultime ?
Nous avons vu qu'une démonstration est en quelque sorte un Arbre utilisant les axiomes d'une théorie et de la logique.
Vous connaissez certainement l'histoire du singe qu'on place devant un clavier. En le laissant tapant ce qu'il veut pendant un temps infini, on pourrait obtenir une copie de n'importe quelle oeuvre.
Nous pourrions faire de même avec les démonstrations : faire tourner un programme qui teste un par un tous les Arbres de démonstration possibles à partir d'un certain ensemble d'axiomes jusqu'à démontrer ou réfuter n'importe quelle proposition P qu'on lui fournit en ENTREE. Si, pendant le parcours des raisonnements possibles, nous obtenons
un Arbre dont la racine est P, nous aurons démontré la proposition P. L'algorithme pourrait renvoyer True.
un Arbre dont la racine est NON P, nous aurons réfuté la proposition P. L'algorithme pourrait renvoyer False.
Malheureusement, dans le cadre d'une théorie suffisamment élaborée, nous ne pourrons jamais prouver la correction de cet algorithme à cause du premier théorème d'incomplétude : certaines propriétés font partie des propriétés indécidables : il est donc certain que l'algorithme va parfois établir des Arbres de démonstration sans jamais tomber ni sur P, ni sur NON P pour la bonne raison de cette proposition précise n'est ni démontrable, ni réfutable !
Notre programme pourrait donc tomber par hasard sur certaines démonstrations, mais ne peut pas démontrer ou réfuter n'importe quelle proposition fournie en ENTREE : il n'est donc pas CORRECT
Il s'agit donc d'un problème indécidable car même en changeant de théorie cohérente, il y aura toujours des propositions indécidables.
La preuve de terminaison d'un algorithme permet d'affirmer qu'il s'arrête de façon certaine sur toutes les entrées valides qu'on lui fournit (c'est à dire les entrées respectant les préconditions).
Preuve de terminaison : si les deux propositions suivantes sont vraies alors la boucle s'arrête :
Proposition A : les boucles s'expriment sous la forme TANT QUEVARIANT>0
Proposition B : le VARIANT est une suite d'ENTIERS strictement décroissante.
(A et B) implique alors que l'algorithme se termine.
Attention à la négation
(A et B) implique que l'algorithme s'arrête TOUJOURS.
NON (A et B) ou encore (NON A) ou (NON B) d'après De Morgan n'implique rien de particulier.
Il est possible que l'algorithme ne boucle jamais, boucle parfois ou boucle toujours.
Rappel : Preuve de correction et invariant
Définitions
La preuve de correction d'un algorithme permet d'affirmer
qu'il fournit toujours une réponse correcte
sur toutes les entrées valides qu'on lui fournit.
Pour faire la preuve de correction d'un algorithme, il faut trouver un INVARIANT : une propriété P vérifiable qui reste vraie lors des différentes étapes de l'algorithme.
Un INVARIANT DE BOUCLE est une propriété VRAIE à chaque début de tour, juste avant l'exécution de la première instruction de la boucle.
Cet invariant permettra de prouver que le résultat final après exécution est bien le résultat attendu.
Malheureusement, il n'y a pas de méthodologie automatique miraculeuse pour trouver cet invariant. Il faut réfléchir et tenter des choses, comme avec toute démonstration.
Démonstration en 3 phases : Initialisation-Conservation-Terminaison
Une fois qu'on dispose d'un INVARIANT P, la démonstration se fait en trois temps.
Phase d'initialisation : P0 est VRAI
On doit prouver que l'INVARIANT est VRAI lorsqu'on commence le premier tour de boucle mais sans l'avoir réalisé en entier. On a donc fait 0 tour en entier.
Le plus souvent, cette partie est triviale. Mais pas toujours...
Phase de conservation : Pk➡ Pk+1
SI P est vrai après k tours de boucles, ALORS P sera encore vrai en ayant fait un tour de boucles supplémentaire.
Hypothèse de départ :
On fait l'hypothèse qu'on a fait k tours de boucles et qu'on est au début du tour k+1. L'INVARIANT Pk est donc considéré juste.
Déroulement du tour de boucle (k+1) jusqu'au début du prochain
On doit montrer qu'en réalisant ce tour complétement jusqu'au début du prochain, l'invariant P reste vrai à la fin de cette boucle. On aura donc fait k+1 tours de boucle complet, Pk+1 serait encore vérifiée.
On se place dans le cadre d'un tour qui est suivi d'un autre tour. On ne se place pas dans le cadre de la toute dernière boucle ici. On boucle, point.
On peut donc écrire Pk➡ Pk+1
Phase de terminaison
On doit y prouver qu'à la fin du dernier tour, on obtient la situation voulue. Ni trop tôt, ni trop tard. C'est pour cela qu'on nomme cette partie la phase de terminaison, à ne pas confondre avec la preuve de terminaison.
P0➡ P1➡ P2➡ P3... ➡ Pfinal
Attention, la méthode est proche des démonstrations pour la récurrence mais pas vraiment identique. C'est pour cela d'ailleurs que les noms ne sont pas les mêmes. Avec la récurrence, les noms des phases sont
initialisation,
hérédité et
conclusion.
Activité publiée le 24 05 2021
Dernière modification : 24 05 2021
Auteur : ows. h.
