prog calculabilité

Identification

Infoforall

38 - Calculabilité


Vous allez voir aujourd'hui que l'informatique théorique a des liens de parenté é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 ?

Logiciel nécessaire pour l'activité : Python 3 : Thonny, IDLE ...

Résumé :

1 - Calculabilité

1 - La notion vague d'algorithme 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.

2 - L'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 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 aux mathématiques
  • en 1929, Kurt Gödel montre dans sa thèse de doctorat que tout raisonnement mathématique peut être formalisé à l'aide de la logique des relations
  • en 1931, ce même Kurt Gödel va publier ses deux théorèmes d'incomplétude montrant que dans toute théorie mathématique "bien pensée" :
    1. est incomplète : il existe nécessairement des propriétés qu'on ne pourra jamais démontrer ou réfuter : on dit que ces propriétés sont indécidables dans le cadre de cette théorie
    2. est peut-être incohérente : savoir si la théorie est incohérente (et donc mal conçue car elle permet parfois de dire VRAI et FAUX en passant par deux raisonnements) est ... indécidable. On ne peut donc pas montrer son incohérence et c'est le fait de tomber sur une incohérence un jour qui va lui donner ce statut...

Tout ceci va redonner des bases stables aux mathématiques : en sachant d'où peuvent venir les incohérences, les différentes théories vont devenir plus solides et cohérentes.

3 - 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 Alonzo Church, Stephen Kleene, Alan Turing et Kurt Godel.

  • Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church invente le système formel du lambda-calcul (ou λ-calcul) qui fonde les concepts de fonction et d'application : cela formalise la notion de calcul. La notion de récurivité est réellement intégrée au λ-calcul.
  • 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écisement ce qu'est un algorithme et ce que représente la complexité d'un algorithme
  • Les fonctions récursives sont également utilisées dans le cadre théorique de modèle de calcul par Kurt Godel, notamment dans ses théorèmes d'incomplétude.
  • Stephen Kleene va démontrer l'équivalence entre les fonctions récursives et le λ-calcul, ainsi qu'entre les fonctions récursives et la machine de Turing. Cela va aboutir à la thèse de Church-Turing qui énonce que toutes ces méthodes de calcul "mécanique" sont équivalentes et peuvent toutes calculer les mêmes fonctions. Elles sont donc de même "puissance prédictive".
Calculabilité

La calculabilité est définie comme tout traitement

  1. issu d'un système physique de calculs (qu'on assimilera à une machine de Turing pour préciser la notion)
  2. répondant après un nombre d'étapes fini (ou un temps fini)
  3. 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.

https://fr.wikipedia.org/wiki/Machine_de_Turing#/media/Fichier:Maquina.png
Vue d'artiste de la machine de Turing (domaine public, publié sur Wikipedia)

La thèse de Church élargit encore la définition puisqu'elle affirme que les méthodes de calculs de la machine de Turing, du λ-calcul, de la récursivité ou de tout langage de programmation Turing-complet (comme Python) ont le même pouvoir de calcul : toutes ces méthodes sont équivalentes et permettent de faire les mêmes calculs.

On notera qu'en anglais la calculabilité se nomme computability : on comprend bien le lien avec "computer". La calculabilité est donc la capacité d'un système informatique de réaliser des calculs.

Et nous avons là une véritable différence entre fonctions informatiques et fonctions mathématiques : les fonctions informatiques ne regroupent que les fonctions calculables par une machine de Turing, le λ-calcul ou tout langage Turing-complet.

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.

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.

La notion de calculabilité n'est néanmoins pas liée qu'aux fonctions. Elle englobe également les nombres calculables.

Un algorithme est, lui, bien assimilable à une fonction : on lui donne des ENTREES sur lequel il travaille et pour lequels il fournit une SORTIE.

ENTREES ➔ ALGORITHME ➔ 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é, il ne s'agit pas vraiment d'un algorithme.

2 - OPTIONNEL : Machine de Turing

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".

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 lequelles 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, pouvant lire le contenu d'une case et se déplacer à droite ou à gauche
  • La tête de lecture possède une case-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) indiquant ce qu'on doit faire ensuite à partir de la lecture de la case du ruban et de l'état. 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

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, le reste étant constitué de cases vides.

init 0 1 0

Pour savoir ce qu'on doit faire, on doit aller lire la case (), l'état (init) et le tableau permettant d'en faire l'interprétation :

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

On applique en trois étapes les deux modifications et le déplacement :

init 0 1 0

init 0 1 0

init 0 1 0

La "nouvelle" configuration après la première séquence :

init 0 1 0

Situation semblable à la précédente : une lecture de case associée à init. Mêmes conséquences : on gére l'état, la valeur de la case puis on se déplace.

init 0 1 0

init 0 1 0

init0 1 0

Nouvelle configuration après la deuxième séquence d'actions :

init0 1 0

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

On obtient alors ces 3 actions élémentaires :

travail0 1 0

travail0 1 0

0 travail1 0

Nouvelle configuration après la troisième séquence d'actions :

0 travail1 0

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

0 travail1 0

0 travail1 0

0 1 travail0

Nouvelle configuration après la quatrième séquence d'actions :

0 1 travail0

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

0 1 travail0

0 1 travail0

0 1 0 travail

Nouvelle configuration après la cinquième séquence d'actions :

0 1 0 travail

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

0 1 0 fini

0 1 0 fini0

0 1 0 0 fini

Nouvelle configuration après la sixième séquence d'actions :

0 1 0 0 fini

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é n'est pas interprétable comme une instruction !

Dans ce cas, la machine s'arrête.

On est parti de ce ruban :

0 1 0

Et on obtient ce ruban :

0 1 0 0

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 !

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 :

  1. Etat 0 et Ruban 00
  2. Etat 0 et Ruban 01
  3. Etat 0 et Ruban 10
  4. Etat 0 et Ruban 110
  5. Etat 1 et Ruban 00
  6. Etat 1 et Ruban 01
  7. Etat 1 et Ruban 10
  8. Etat 1 et Ruban 110

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.

3 - Décidabilité

Décidabilité algorithmique

Un problème de décision est décidable s'il existe une machine de Turing qui accepte les instances du problème où la réponse est OUI.

Si on se ramène à un programme Python plutôt qu'à la machine de Turing, cela veut dire qu'un problème décidable est un problème pour lequel on peut créer une fonction booléenne qui pourra répondre True ou False pour répondre à toute 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
def estPremier(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 :

1 2 3 4 5 6 7 8 9 10
def estPremier(n:int) -> bool: if n < 2: return False elif n == 2: return True else: for x in range(2, n): if n % x == 0: return False return True

Attention : la notion de décidabilité algorithmique n'est pas liée à la notion de difficulté algorithmique. Un problème peut être décidable sans pour autant disposer d'un algorithme qui ne soit pas difficile : on pourra alors le résoudre en théorie mais pas concrétement dès que les données seront importantes.

Problème indécidable

Tous les problèmes ne sont pas décidables.

Certains problèmes sont indécidables : on ne peut pas créer de fonctions, de programmes ou de machines de Turing capables de répondre OUI ou NON pour chacune des instances possibles du problème.

Attention : dire qu'un problème est indécidable algorithmiquement ne veut pas dire qu'on ne peut pas trouver de solution à une instance particulière, ou trouver de solution sans passer par un algorithme. Cela veut dire qu'on ne peut pas trouver la solution d'une instance quelconque automatiquement.

Globalement, si on sait que notre problème est indécidable, il faut le rendre plus simple.

Première approche : simplifier la réponse attendue, la rendre "plus vague". On aura alors un problème légérement différent mais une réponse approximative par rapport à la réponse attendue, mais c'est parfois mieux que rien.

Deuxième approche : réduire le domaine d'application. On se restreint à un certain type d'instances. On aura alors peu-être un algorithme applicable mais pas à toutes les entrées du vrai problème.

Et une fois qu'on a trouvé un algorithme valide ? Il faut voir comment se rapprocher du vrai problème initial si c'est possible. En sachant qu'on ne l'atteindra jamais si le problème initial est indécidable.

4 - Problème de l'arrêt

Vous allez découvrir aujourd'hui l'un des problèmes indécidables : le problême de l'arrêt d'un programme.

Vous savez qu'un programme peut être vu comme une donnée qu'on fournit à un autre programme.

Le problème qu'on se pose est le suivant : peut-on créer un programme arrêt arret qui soit capable d'affirmer qu'un autre programme quelconque p va s'arrêter à coup un jour sur connaissant :

  • le code du programme quelconque p et
  • les entrées e sur lesquelles p devra travailler.

Ce serait assez pratique surtout d'un point de vue sécurité : on pourrait vérifier qu'un programme va bien s'arrêter et répondre quelque chose plutôt que de tourner en boucle avant de le lancer. La question n'est pas de savoir ce qu'il va répondre, juste de savoir s'il va répondre un truc ou ne jamais s'arrêter.

La thèse de Church-Turing nous dit que cela revient à savoir si cette fonction Python peut exister :

1
def arret(p:code_en_tant_que_donnees, e:données) -> bool:

Nous allons voir que ce problème de l'Arrêt est indécidable : on ne peut pas créer un programme capable de détecter automatiquement si un autre programme dont on connait les entrées va s'arrêter ou non.

Les mathématiciens Church et Turing ont prouvé que ce problème est indécidable avant même l'apparition réelle des ordinateurs.

Que faire avec notre énoncé "Existe-il un programme capable de détecter l'arrêt de n'importe quel autre programme ?" ?

Nous allons montrer que cela n'est pas possible en utilisant un raisonnement par l'absurde :

  • Nous allons considérer qu'un telle fonction arret existe
  • Nous allons créer une nouvelle situation en utilisant cette fonction arret
  • Nous allons montrer que l'existence de arret mène à une incohérence ce qui permet donc de montrer que l'hypothèse initiale de l'existence de arret est fausse.
  • Comme la fonction existe ou n'existe pas, nous pourrons en déduire qu'elle n'existe pas.

1 - Description de la fonction arret

Nous allons travailler dans une l'optique d'une programmation Python.

On considère donc VRAI l'existence de cette fonction arret :

1 2 3
def arret(p:code, e:entrees_pour_p) -> bool: if p(e) s'arrête : return True else : return False

Notez bien que je ne donne pas le 'vrai code'. Il n'existe pas, je suppose juste que ce code peut fonctionner dans l'idée. Imaginez une fonction capable de prévoir le fonctionnement d'une autre fonction en lisant son code-source. Ca n'a pas l'air inimaginable si ?

  • Le paramètre p constitue donc le code de la fonction p, code fourni en tant que données pour que arret puisse l'analyser, pas le lancer directement.
  • Le paramètre e contient les données qu'on va confier à la fonction p si on l'exécute.

On imagine que la fonction arret est capable d'analyser le code-source p et de dire si un vrai appel de type p(e) va répondre ou tourner à l'infini.

La seule chose à comprendre est donc que le code-source p n'est pas réellement exécuté : il s'agit juste d'analyse.

2 - Création d'une fonction inverser

Voici le code parfaitement valide de la fonction inverser :

1 2 3 4 5 6
def boucler(): while True: pass def inverser(f:code): if arret(f, f): boucler() else : return 1

Comme on peut le voir, le code de la fonction inverser est parfaitement valide. Aucune erreur.

Notre fonction se nomme inverser car :

  • inverser(f) tourne en boucle si arret détermine que f(f) s'arrête.
  • inverser(f) s'arrête si arret détermine que f(f) ne s'arrêtera pas (sans le lancer, juste en lisant son code-source et ses données d'entrée).

Il n'y a donc aucun problème pour l'instant.

3 - Utilisation créant un paradoxe

Regardons maintenant ce qui va se passer si on fait l'appel suivant :

arret(inverser, inverser)

Autrement dit, on se demande si la fonction inverser va s'arrêter dans le cas d'un appel inverser(inverser) valide puisque cette fonction a juste besoin d'un code-source (un fichier-texte en gros) à analyser. Imaginez un anti-virus qui analyse son propre code-source si cela vous choque. Vous verrez qu'il n'y a rien de génant en soi.

Souvenez-vous que nous avons fait l'hypothèse au départ que arret pouvait déterminer l'arrêt de n'importe quelle fonction.

Voici le code de arret :

1 2 3
def arret(p:code, e:entrees_pour_p) -> bool: if p(e) s'arrête : return True else : return False

Puisqu'on lance arret(inverser, inverser), lors de cet appel, cela revient mentalement à avoir quelque chose comme ceci :

1 2 3
def arret(p=inverser, e=inverser) -> bool: if inverser(inverser) s'arrête : return True else : return False

Et c'est maintenant que nous allons observer la contradiction qui va mener à une absurdité.

Regardons ce qui se passe si arret(inverser, inverser) renvoie True, pour dire que inverser(inverser) va s'arrêter :

1 2 3 4 5 6 7
def arret(p=inverser, e=inverser) -> bool: if inverser(inverser) s'arrête : return True else : return False def inverser(f=inverser): if arret(inverser, inverser): boucler() else : return 1

Cela revient à écrire :

1 2 3 4 5 6 7
def arret(p=inverser, e=inverser) -> bool: if inverser(inverser) s'arrête : return True else : return False def inverser(f=inverser): if inverser(inverser) s'arrête: boucler() else : return 1

Et c'est en ligne 6 ici qu'il y a un problème : la fonction arret affirme que cet appel inverser(inverser) s'arrête mais on voit bien qu'il va... boucler et ne pourra donc pas s'arrêter.

4 - Conclusion

  1. 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
  2. l'utilisation de cette hypothèse associée à d'autres raisonnements corrects eux mène à une incohérence, un résultat absurde.
  3. 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.

5 - Fortement optionnel : indécidable ?

Nous allons voir aujourd'hui pourquoi l'informatique et les mathématiques sont fortement en interaction.

Nous avons déjà vu

  • qu'on pouvait démontrer qu'un algorithme s'arrête à tous les cas ou pas : on fait la preuve de terminaison en utilisant un VARIANT (et on utilise les suites mathématiques pour cela, voir le rappel de 1er dans la FAQ)
  • qu'on pouvait alors montrer qu'un algorithme donne la bonne réponse à chaque fois : on fait la preuve de correction en utilisant un INVARIANT (et on utilise un raisonnement proche des démonstrations de récurrence en mathématiques, voir le rappel de 1er dans la FAQ)
  • qu'on pouvait ramener les choix logiques booléens à des calculs avec l'algèbre de Bool (a ET b peut se ramener à a.b, justification de la priorité des opérateurs NON puis ET puis OU ect...)
  • et que bien des notions d'informatique sont issues des mathématiques (les arbres, les graphes, les fonctions et j'en passe...)
  • qu'on pouvait démontrer mathématiquement que certains problèmes ne sont pas capables d'être résolus par un algorithme

Logique mathématique et informatique théorique sont en réalité beaucoup plus proches que vous ne l'imaginez certainement pour l'instant.

Cette partie purement optionnelle vise simplement à vous éclairer sur l'époque qui a précédé l'apparition de l'informatique et à vous montrer que les instructions et fonctions de l'informatique sont des choses issues de la théorie mathématique.

Vous allez voir que le jeu de construction qu'on peut utiliser pour batir des fonctions à partir d'instructions élémentaires est très proche des démonstrations qu'on peut batir en utilisant les axiomes des théories mathématiques...

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. Voic les trois premiers :

  1. L'élément appelé zéro et noté 0 est un entier naturel.
  2. Tout entier naturel n a un unique successeur, noté s(n) ou Sn qui est un entier naturel.
  3. Aucun entier naturel n'a 0 pour successeur.
  4. ...

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é vraie n'est donc jamais une invention : elle est présente depuis le début dans la théorie. 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éee. Comprendre par là que beaucoup de propriétés pourtant démontrées n'ont pas pour autant 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) :

  1. cohérence : impossibilité de démontrer une proposition et son contraire
  2. 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)
  3. 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 lequels :

    • alors que la proposition P est vraie, on ne parviendra jamais à le démontrer... Pour vous donner une image de ce cas, imaginez le théorème de Pythagore en version conjoncture et sans que jamais on ne parvienne à la démontrer. Dans ce cas, il est vrai mais on ne pourra pas lui faire ABSOLUMENT confiance. Tous les exemples montrent qu'on obtient le bon résultat, mais on ne parvient pas à le démontrer. C'est donc un peu l'équivalent d'une fonction qu'on a créé, qui a l'air de fonctionner mais dont on ne parvient pas à prouver la correction.
    • alors que la proposition P est fausse, on ne parviendra pas à la 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)

  • 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 coup précédent : on a trop de briques et on finit par pouvoir bâtir des raisonnements contradictoires.
  • On pourrait ainsi trouver deux arbres de démonstration, l'un menant à P et l'autre menant à NON P.

Situation embarrassante...

Il y a toujours des énoncés qui sont uniquement VRAI ou uniquement FAUX. Mais, il existe dans ces théories des énoncés dont on peut démontrer qu'ils sont VRAI en suivant un raisonnement et FAUX en suivant un autre raisonnement. Bref, c'est une théorie dans laquelle il est dangereux de faire confiance à ce qu'on démontre.

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 parle de tiers exclus : soit c'est VRAI et démontrable, soit c'est FAUX et réfutable.

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 suite 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 batir 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 redefinir 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.

evaluer_une_proposition(proposition, axiomes:list) -> bool

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.

Dans les années 1930, les énoncés indécidables semblaient un peu artificiels, mais rapidement des cas plus simples et utiles ont été trouvés.

Aujourd'hui, connaître la liste des problèmes indécidables est important de façon globale pour un informaticien et certains chercheurs se spécialisent dans la conquête de la zone comprise entre les algorithmes connus pour résoudre certains problèmes proches de problèmes indécidables. On ne pourra jamais rentrer algorithmiquement dans la zone indécidable mais s'en approcher au plus près permet déjà de résoudre beaucoup de choses.

6 - FAQ

Rappel : Preuve de terminaison

La preuve de terminaison d'un algorithme permet d'affirmer qu'il s'arrête de façon certaine (c'est à dire qu'il ne boucle pas infiniment) sur toutes les entrées valides qu'on lui fournit (c'est à dire les entrées respectant les préconditions).

Pour faire la preuve de terminaison, il faut montrer que :

  • ses boucles s'expriment sous la forme TANT QUE VARIANT > 0
  • avec un VARIANT de boucle pouvant s'écrire comme une suite un strictement décroissante d'entiers.

Rappel : Preuve de correction et invariant

La preuve de correction d'un algorithme permet d'affirmer

  • qu'il fournit toujours la bonne réponse (réalise sans erreur le travail pour lequel il est conçu)
  • sur toutes les entrées valides qu'on lui fournit (les entrées respectant les préconditions).

Pour faire la preuve de correction, il faut trouver un INVARIANT, une propriété P vérifiable qui reste vraie tout le long du déroulement de l'algorithme. 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.

Une fois qu'on dispose d'un INVARIANT P, la démonstration se fait en trois temps.

  1. L'initialisation P0 est VRAI
  2. On montre que l'INVARIANT est VRAI avant le premier passage dans une boucle.

    Si on note la propriété invariante P, on montre donc que P0 est VRAI. 0 doit s'entendre comme "avant le moindre passage dans la boucle".

    Le plus souvent, cette partie est triviale. Mais pas toujours...

  3. La conservation Pk Pk+1
  4. On montre que l'INVARIANT reste VRAI après chaque passage dans une boucle.

    1. On suppose que Pk est vérifié : vous avez fait k tours de boucle et on suppose qu'on obtient une certaine configuration qui respecte l'INVARIANT.
    2. On montre alors qu'avec un tour de boucle en plus, Pk+1 est vérifié obligatoirement.
    3. On peut donc écrire Pk Pk+1
  5. La terminaison
  6. On montre que l’algorithme a bien traité toutes les donneés une fois sorti des boucles : il faut montrer qu'il s'arrête où il faut.

    On exploite les deux phases précédentes pour montrer qu'avec le nombre finale N de boucles effectuées, l'algorithme a bien répondu à son objectif en s'arrêtant juste où il faut.

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.