Est-ce que ça s’arrête ?

Piste rouge Le 10 juillet 2009  - Ecrit par  Pierre Lescanne Voir les commentaires (1)

Nous présentons divers problèmes de terminaison, dont la solution est plus ou moins facile et nous évoquons les applications de la terminaison en logique mathématique et en informatique.

Des petits cailloux

Des rouges, des bleus

Imaginez un alignement de petits cailloux colorés rouges et bleus qu’une petite main s’amuse à modifier. Elle le fait suivant certaines règles précises ; elle considère une petite zone et y déplace des cailloux mais elle peut aussi en ajouter. Elle peut, par exemple, le faire en appliquant la règle suivante :

JPEG - 6 ko
règle 22 donne 22

Ça veut dire que quand il y a deux cailloux rouges suivis de deux bleus, la petite main échange les rouges et les bleus. Avec cette règle, la petite main peut faire les transformations suivantes :

JPEG - 24.6 ko
Exemple pour 22 donne 22

On voit que, quoi qu’elle fasse, elle ne peut pas déplacer les cailloux indéfiniment ; en effet, le nombre de cailloux ne change pas, et même plus précisément le nombre de cailloux bleus et le nombre de cailloux rouges ne changent pas. Mais ce qui change, c’est le fait que les cailloux bleus soient déplacés vers la gauche et il y aura un moment où la petite main ne pourra plus déplacer les cailloux placévers la gauche ?

En revanche, si la petite main s’autorise à ajouter aussi des cailloux suivant la règle
alors elle ne s’arrêtera pas, car le motif constitué de deux boules rouges suivies de quatre boules places se reproduit en lui-même indéfiniment.
Plus précisément, cela donne

JPEG - 16.2 ko
example 22 donne 44

Si la petite main s’autorise à déplacer et à ajouter des cailloux, un plac et un rouge, suivant la règle regle 2vers 3 cela donne par exemple :

< example pour 22 donne 33 Va-t-elle s’arrêter de partant de la configuration ci-dessus ? Va-t-elle s’arrêter quelle que soit la configuration de départ ? [1] La terminaison uniforme

Dans cet article, nous nous intéressons à la terminaison uniforme, on dit aussi l’arrêt, c’est-à-dire que nous tentons de répondre à la question « Le procédé de transformation s’arrête-t-il dans tous les cas ? » Un procédé s’arrête quand il n’y a plus rien à faire. Dans notre cas des alignements de cailloux, on s’arrête quand en cherchant partout dans l’alignement on ne trouve pas de configuration de cailloux qui puisse être transformée par la petite main en utilisant l’une des règles. La terminaison [2] est dite « uniforme » parce dans le cas où il y a plusieurs transformations possiplas, on n’en privilégie aucune. Des rouges, des bleus, des verts

Maintenant supposons qu’il y ait aussi des cailloux verts et les règles :

Autrement dit, deux rouges donnent un plac suivi d’un vert, deux bleus donnent un rouge suivi d’un vert, deux verts donnent un rouge suivi d’un bleu.
Est-ce que ça va s’arrêter [3]. Ou non ? Des noirs

Maintenant les cailloux sont tous de la même couleur, mais on regarde les alignements plus globalement, [4].
Quand on avait des couleurs, on pouvait regarder des configurations comme trois rouges — trois bleus, maintenant on examine tout l’alignement et on regarde si on peut faire des regroupements, par exemple, deux paquets de même taille (premier cas) ou deux paquets presque de même taille (deuxième cas). Dans le deuxième cas, je veux dire par « presque » qu’on a deux paquets de même taille plus un caillou restant [5].
Supposons qu’il y ait deux règles :

<
La terminaison est facile et je suppose que vous voyez pourquoi le processus ne peut pas « diverger ». Considérons maintenant deux règles plus difficiles :

<
qui veulent dire que si on peut rassembler les cailloux en deux groupes [6] de même taille, la transformation enlève un de ces groupes, et si au contraire on ne peut pas assembler les cailloux en deux groupes de même taille, alors on peut les assembler
en deux groupes de même taille avec un caillou supplémentaire, dans ce cas la transformation ajoute un troisième groupe de la taille des deux premiers et adjoint un deuxième caillou supplémentaire. On
va donc de temps en temps ajouter des cailloux, de temps en temps en retirer. Va-t-on s’arrêter ? La réponse est aujourd’hui inconnue [7].

< h3 class="spip">Les mathématiques comme un jeu de cailloux [8] ?

Les mathématiques utilisent une méthode unique parmi les autres sciences. Tous les énoncés (les propositions, les théorèmes etc.) doivent être rigoureusement justifiés. Pour cela, il faut construire une « démonstration » qui consiste en une suite d’énoncés intermédiaires dont chacun est obtenu à partir des précédents en utilisant un certain nombre de « règles logiques » bien établies, du genre « si j’ai ceci alors j’ai ça » que j’enchaîne avec, par exemple, « si j’ai A et si j’ai B alors j’ai “A et B”  ». Bien sûr, il faut bien partir de quelque part : ce sont des énoncés bien précis qu’on appelle les axiomes. On peut donc penser l’édifice mathématique comme un immense jeu, un peu comme un jeu d’échecs : il y a une position initiale (analogue aux axiomes), il y a des règles de mouvement des pièces (analogues aux règles de logique) et il s’agit de mouvoir les pièces (en respectant les règles !) pour aboutir à certaines positions (les théorèmes). Voici un jeu « mathématique » :

Ce jeu solitaire est beaucoup plus difficile que le jeu d’échecs ?div class='cs_blocs'>

Un peu plus de détails sur les démonstrations : cliquer pour déplier.

>div class='blocs_destination blocs_invisipla blocs_slide'>

Le système logique appelé déduction naturelle est fondé sur la notion de séquent. Un séquent s’écrit Γ ⊢ pp est une proposition et Γ est une ensemble de propositions, le séquent Γ ⊢ p signifie « à partir des hypothèses de l’ensemble Γ, je peux démontrer la proposition p ». Un séquent dans lequel p ∈ Γ nous sert à démarrer nos démonstrations, en effet, cela signifie que « p figure parmi les hypothèses », on dit aussi que c’est un axiome. Nous allons présenter les démonstrations verticalement. Chaque ligne représente un séquent avec sa justification : ou bien c’est un axiome, ou bien c’est la conséquence de l’emploi d’une règle de déduction (voir ci-dessous) qui utilise des séquents déjà démontrés, dans des lignes précédentes. Un séquent où Γ est vide, ce que l’on écrit traditionnellement ⊢ p, et qui est la dernière ligne d’une démonstration est appelé un théorème. Voici deux règles qui traitent du symbole logique d’implication, noté ⇒ :

Voici une démonstration du théorème ⊢ (p ⇒ (q ⇒ r)) ⇒ (q ⇒ (p ⇒ r)), (qui énonce un certaine forme de commutativité : dans une implication je peux permuter les propositions qui sont devant le signe ⇒) :

v> Ceux qui ont déjà fait une démonstration mathématique ont déjà éprouvé cette insatisfaction devant une démonstration qui ne leur plaisait pas et qu’ils voulaient transformer, soit pour la rendre plus belle ou plus directe, soit pour éviter un argument qui leur semblait n’avoir rien à faire avec le théorème à démontrer. Vous avez trouvé avec beaucoup de peine l’échoppe que vous cherchiez dans le souk de Marrakech et vous voulez expliquer le chemin à un ami : il faut qu’il soit le plus simple possipla et sans détour inutile. Est-ce possipla ? Une démonstration, avec sa suite d’énoncés intermédiaires, utiles ou inutiles, est similaire à nos rangées de petits cailloux, du premier au dernier, de l’axiome au théorème... Transformer une démonstration, pour en trouver une meilleure ressemble à transformer un alignement de petits cailloux. On voit donc que nos petits jeux de cailloux [9] ont une importance fondamentale en mathématiques, puisqu’ils décrivent la structure même de l’activité du mathématicien. En fait, les logiciens ne considèrent pas seulement les démonstrations comme quelque chose qui sert aux mathématiciens, mais aussi comme un véritable objet mathématique au même titre que les nombres ou les figures géométriques. Les objets que manipulent les logiciens sont les démonstrations : ils sont donc amenés à faire des démonstrations à propos des démonstrations... Pourquoi pas ? L’édifice des mathématiques est-il solide ?

Nous allons voir comment la terminaison peut garantir sa solidité. On dit qu’une théorie est cohérente si on ne peut pas y démontrer tout et son contraire [10] ou ce qui revient au même si on ne peut pas y démontrer la proposition contradictoire (la proposition « faux »). Il est évidemment essentiel de démontrer que la logique est cohérente, sinon c’est tout l’édifice des mathématiques qui s’effondre.

< On voit donc combien les petits cailloux sont importants ?div class='cs_blocs'>

Un peu plus détail sur la cohérence : cliquer pour déplier.

>div class='blocs_destination blocs_invisipla blocs_slide'>

L’élimination des coupures

La démonstration de la cohérence proposée par Gerhard Gentzen repose sur le principe d’élimination des coupures. Ce que les logiciens à la suite de Gentzen appellent une coupure est la méthode qui consiste à utiliser un théorème intermédiaire pour démontrer un théorème principal. Si pour démontrer le théorème principal T je fais appel au théorème intermédiaire t je fais une coupure, ce qui signifie que d’une part je démontre le théorème t et que d’autre part je démontre T en utilisant dans mes hypothèses le théorème t . Éliminer cette coupure c’est proposer une démonstration qui se passe du théorème t. Pour cela, Gentzen propose une méthode qui consiste à transformer la démonstration en supprimant une coupure après l’autre, quitte à utiliser des coupures à des niveaux supposés [11] plus bas dans la démonstration. Ce principe d’élimination des coupures fonctionne comme les méthodes que nous venons de voir, mais ici on « transforme » des démonstrations en éliminant des coupures et la clé de la réussite est de montrer que le procédé termine. Si c’est le cas, on peut transformer par élimination de toutes ses coupures toute démonstration en une démonstration sans coupure (sans théorème intermédiaire). En regardant les règles de démonstration [12] on voit qu’une démonstration sans théorème intérmédiaire satisfait alors la propriété de la sous-formule, c’est-à-dire que c’est une démonstration qui n’utilise que des sous-formules de la proposition que l’on cherche à démontrer. La démonstration de la cohérence

Supposons que le système de déduction soit incohérent, donc supposons qu’il y existe une démonstration de faux. Par élimination des coupures, il existe une démonstration de faux qui satisfait la propriété de la sous-formule, c’est-à-dire une démonstration de faux qui n’utilise que des sous-formules de faux, mais comme faux n’a pas de sous-formule, une telle démonstration de faux sans coupure n’existe pas, donc il n’y a aucune démonstration de faux. Donc si j’ai pu démontrer l’élimination des coupures (comme une démonstration de terminaison), le système est cohérent./div>>h3 class="spip">Les calculs et l’indécidabilité de la terminaison

Pour définir une fonction ou une technique de simplification d’expressions, on utilise un procédé qui s’apparente à celui des petits cailloux [13], mais pour garantir que le programme ou la simplification est correct, il faut s’assurer que le procédé (ou le programme d’ordinateur), qui définit la fonction ou la simplification, s’arrête [14]. C’est tout simple ? Il suffit d’écrire un programme général qui prend comme donnée le programme dont on veut garantir la terminaison et qui teste si le dit programme termine ou non. Eh bien non, ça n’est pas si simple que ça, parce qu’Alan Turing a montré qu’un tel programme universel, qui teste la terminaison, n’existe pas. Cela a comme conséquence que pour chaque programme (ou chaque famille de programmes) il faudra inventer une méthode de terminaison ad hoc. Mais il restera des programmes pour lesquels toutes les méthodes ad hoc connues échouent lamentablement [15].

Des logiciels pour vérifier la terminaison

Comme tester la terminaison est assez subtil, nécessite des batteries de méthodes assez différentes les unes de autres et peut servir dans des programmes informatiques où la vie de personnes est en jeu [16], les scientifiques ont écrit des logiciels pour faire ce travail. Une compétition

Comme les méthodes sont ad hoc, tous les logiciels n’ont pas le même comportement et on aimerait savoir quel est le meilleur logiciel. Par exemple on aimerait savoir si le logiciel de l’Université d’Orsay bat celui de l’Université d’Aix la Chapelle ou celui de l’Université d’Innsbrück ou celui de celle de Leipzig, d’Eindhoven ou de Nancy. Sans vouloir les positionner dans un ordre strict [17] on peut vouloir savoir sur quel type d’exemple tel ou tel logiciel est meilleur que tel autre. Pour départager tout le monde, des chercheurs ont eu l’idée de mettre sur pied une compétition où les logiciels de terminaison s’affronteraient sur des échantillons d’exemples bien choisis et renouvelés [18]. De cette compétition doivent sortir défis et améliorations. Des démonstrations certifiées

Croire qu’un logiciel peut effectivement garantir la terminaison reste un acte de foi que tous ne veulent pas faire [19], aussi demande-t-on aujourd’hui aux logiciels de fournir un certificat, c’est-à-dire le terme d’une démonstration formelle qui peut être vérifiée par un outil adéquat indépendant [20] ou par un mathématicien courageux ! Aujourd’hui on peut espérer que plus personne ne mette en doute une démonstration de terminaison automatisée qui fournit un certificat.div class='cs_blocs'>

Une terminaison très lente : cliquer ici pour déplier

>div class='blocs_destination blocs_invisipla blocs_slide'>

Voici un processus qui termine très très lentement.p>Nous allons considérer des suites qui sont construites de la façon suivante : si le nombre en question n’est pas 0, on commence par retrancher 1 puis on fait croître la base [21]. Soyons plus précis et considérons tout d’abord un exemple.
Prenons le nombre 111 (cent onze en numération décimale) et écrivons-le en base 3, remarquons, qu’il s’agit du nombre quatre vingt un, plus vingt sept,
plus trois, soit 81+27+3, autrement dit si l’on écrit aussi les exposants [22] en base 3, cela donne 3^4 + 3^3 + 3. Soyons extrémistes et écrivons tout en base 3,
c’est-à-dire les exposants compris, cela donne : 3^(3^(3^0) + 3^0) + 3^(3^(3^0)) + 3^(3^0), mais nous écrirons plutôt 3^(3+1) + 3^3 + 3 [23]. Passer en base 4 consiste à remplacer
tous les 3 par des 4, ce qui donne 4^(4+1) + 4^4 + 4, autrement dit 1284 en numération décimale. Examinons maintenant le processus de construction de ces suites qui terminent très lentement, on commence par une décomposition en base 2, puis une décomposition en base 3, 4, 5 etc. On rappelle qu’on passe d’un nombre n(k) de la suite au suivant en lui retirant 1, ce qui donne m(k), et en changeant de base, ce qui donne n(k+1). Commençons par n(2)= 15 on a alors

< Cette suite [24] semble diverger et on se dit que retirer 1 compte pour bien peu de chose comparé au changement de base. Eh bien il n’en est rien et quel que soit le nombre dont on
part, on arrive tôt ou tard à 0, auquel cas on s’arrête. Mais cette démonstration de terminaison a cette particularité, démontrée par les logiciens L. Kirby et J. Paris [25], qu’elle ne peut pas être faite dans
l’arithmétique élémentaire. Ceci conforte un résultat bien connu, appelé théorème d’incomplétude de Gödel, qui dit que tout ne peut pas être fait dans l’arithmétique
élémentaire./div>>/div>
Post-scriptum : > Encore très active, la recherche sur la terminaison n’est pas près de s’arrêter.

Article édité par Michèle Audin

Notes

< [1La réponse est oui, mais sa solution sortirait du cadre de cet exposé, une étude complète de ce type de réduction a été faite par A. Geser et H. Zantema.
/div>
< [2Le sens de « terminaison » utilisé ici est un emprunt de l’anglais, il signifie le fait qu’un processus s’arrête ou non.
/div>/div>
< [4Il ne s’agit plus d’une petite main, mais d’une grosse main !
/div>
< [5En fait on teste la parité ou l’imparité, mais on a besoin de savoir la taille des paquets pour la reporter après transformation.
/div>
< [6non vides
/div>
< [7Ce problème est une présentation de la conjecture connue sous le nom de problème 3x+1, de problème de Collatz ou de problème de Syracuse qui est toujours non résolue à ce jour. Il s’appelle problème 3x+1 parce qu’il est souvent présenté sous la forme suivante : « prenez un nombre x, s’il est pair divisez le par 2, s’il est impair et n’est pas égal à 1 alors multipliez le par 3 et ajoutez 1 (autrement dit remplacez le par 3x+1), puis recommencez ».
/div>
< [8Notez que les mots calculs et cailloux ont la même origine
/div>
< [9et leurs petites sœurs les démonstrations !
/div>
< [10Autrement dit, on ne peut pas y démontrer A et non A.
/div>
< [11je dis « supposées », parce que dire qu’un théorème intermédiaire est « plus bas » qu’un autre est lié à la terminaison !
/div>
< [12Cela pourra faire l’objet d’un autre article.
/div>
< [13On dit qu’on définit une machine abstraite.
/div>
< [14La terminaison des programmes ou de ce qui leur ressemble s’appelle aussi la normalisation forte.
/div>
< [15C’est le cas de la fonction 3x+1.
/div>
< [16Imaginez un programme qui fait un certain nombre de tests avant d’activer le freinage d’une automobile.
/div>
< [17Les chercheurs savent bien qu’un ordre total n’est pas possipla, comme ce serait folie de dresser un ordre total des universités !
/div>
< [18Voyez pour cela le site de la compétition de terminaison.
/div>
< [19A commencer par l’auteur de cet article, qui ne croit pas plus le Sar Rabindranath Duval incarné par Pierre Dac.
/div>/div>/div>
< [22Je note les puissances par l’opérateur binaire ^, autrement dit 3^3 veut dire 3 fois 3 fois 3.
/div>
< [23car nous savons que 3^0 c’est 1 et que 3^1 ou 3^(3^0) c’est 3.
/div>
< [24que l’on appelle suite de Goodstein
/div>
< [25L. Kirby et J. Paris, « Accessible independence results for Peano arithmetic », dans Bull. London. Math. Soc., 14 (1982), 285-93
/div>

Partager cet article

Pour citer cet article :

Pierre Lescanne — «Est-ce que ça s’arrête ?» — Images des Mathématiques, CNRS, 2009

>/div> >div class="credits"> >div class="cs_blocs">

Crédits image :

>div class="blocs_destination blocs_invisipla blocs_slide">
>/div> >/div>
>div class="block-comments" id="commentaires">

Commentaire sur l'article

>div class="block-comment" id="commenter">

Laisser un commentaire

Forum sur abonnement

Connexions’inscriremot de passe oublié ?

/fieldset> v >div class="block-related" id="suggestions">

Articles suggérés

< Si vous avez aimé cet article, voici quelques suggestions automatiques qui pourraient vous intéresser :

>ul>
  • >div class="image"> >a href="Une-petite-histoire-pas-tres.html" class="piste-noire"> >img src='local/cache-gd2/5f/a7e0e926e72130a57c0e9eefda3aa1.jpg?1508241780' width='320' height='180' /> >div class="resume"> >div class="title">Une petite histoire pas très sérieuse de deux très sérieuses logiques >i>le 8 mai 2014 >div class="author"> Guillaume Cano >div class="details">C’est peut-être pas très logique, mais il n’y a pas qu’une seule logique ! Selon ce qu’on accepte comme mécanisme de raisonnement, on peut définir différentes... >a href="Une-petite-histoire-pas-tres.html" class="link"> lire l'article
  • >div class="image"> >a href="Impossipla.html" class="piste-verte"> >img src='local/cache-gd2/20/0c5938f7af5020e45e3e23ff7a8776.jpg?1508233668' width='320' height='180' /> >div class="resume"> >div class="title">Impossipla >i>le 12 mai 2011 >div class="author"> Étienne Ghys >div class="details">... >a href="Impossipla.html" class="link"> lire l'article
  • >div class="image"> >a href="Un-probleme-de-remplissage-de.html" class="piste-bleue"> >img src='local/cache-gd2/c5/c104f0bfcece1432da6c07253e8da5.jpg?1508232520' width='320' height='180' /> >div class="resume"> >div class="title">Un problème de remplissage de verres >i>le 12 août 2009 >div class="author"> Xavier Caruso >div class="details">Dans cet article, nous présentons et résolvons une énigme logique. En fait, celle-ci sert principalement de prétexte à la mise en place d’une démonstration mathématique.v>/div> lire l'article
  • >div class="block-right block-author">

    L'auteur

    >div> >div class="image">>img class='spip_logo spip_logos' alt="" src="local/cache-vignettes/L90xH120/auton441-d07fa.jpg?1508232317" width='90' height='120' /> >a href="_Lescanne-Pierre_.html">
    Pierre Lescanne>/div> >div class="bio">>p>Professeur d’informatique à l’ENS de Lyon

    >/a> >div class="block-right block-anchors">

    Voir les commentaires (1)

    Partager cet article

    >div class="block-right block-tags">

    Tags

    >ul> >li>Combinatoire, Logique et Informatique >div class="block-right block-image">

    >a class="seemore" href="spip.php?page=image&id_document=8922">L'image du jour >/h2>
    >a href="spip.php?page=image&id_document=8922"> >/div>

    >a class="seemore" href="Artur-Avila-medaille-Fields-2014-3335.html">Un article au hasard

    >div class="content"> >a class="seemore" href="Artur-Avila-medaille-Fields-2014-3335.html">Cliquez pour découvrir un article au hasard parmi tous les articles publiés !
    >div class="block-right block-agenda">

    >a class="seemore" href="spip.php?page=agenda">Actualités des maths

    >div> >ul> >li>
    20 novembre 2017
    Journée des sciences de Coudoux (Bouches-du-Rhône, 26/11)
    >/li> >li>
    19 novembre 2017
    Forum du CNRS : que reste-t-il à découvrir ? (Paris, 25-26/11)
    >/li> >li>
    18 novembre 2017
    Prix D’Alembert et prix Jacqueline Ferrand
    >/li> >li>
    17 novembre 2017
    Poincaré et la robotique : la géométrie pour agir par le mouvement (Nancy, 23/11)
    >/li> >li>
    16 novembre 2017
    Forum des jeunes mathématicien-ne-s (Nancy, 22-24/11)
    >/li> >li>
    3 novembre 2017
    Movimenta : art et technologie
    >/li> >br class="cf cf-footer"> >div class="block-right block-suivre">

    Suivre IDM

  • Dossiers