Système de Thue

En informatique théorique et en logique mathématique, un système de semi-Thue ou sa version symétrique, un système de Thue, est un système de réécriture de chaînes de caractères ou mots, appelé ainsi d'après son inventeur, le mathématicien norvégien Axel Thue. Contrairement aux grammaires formelles, un tel système ne distingue pas entre symboles terminaux et non terminaux, et ne possède pas d'axiome.

Un système de semi-Thue est donné par une relation binaire finie fixe entre mots sur un alphabet donné, dont les éléments sont appelés les règles de réécriture, et notées . La relation est étendue en une relation de réécriture entre tous les mots dans lesquels les parties gauche et droite d'une règle apparaissent en facteur, en d'autres termes on a la relation , pour une règle de et des mots , et quelconques.

Les systèmes de semi-Thue sont Turing-complets. Ils sont voisins des systèmes de Post. Axel Thue a étudié les systèmes de réécriture dans deux articles, l'un sur la réécriture de termes, l'autre sur la réécriture des mots ; c'est du deuxième que dérivent les systèmes de semi-Thue[1].

Le problème de décider de l'existence d'une relation entre deux mots est indécidable.

Définition

Un système de semi-Thue est un couple , où est un alphabet supposé en général fini, et où est une relation binaire finie entre mots sur , donc une partie finie Un élément est une règle de réécriture et est habituellement écrite sous la forme . Si la relation est symétrique, c'est-à-dire si implique , le système est appelé un système de Thue.

Les règles de réécriture sont étendues aux mots de en permettant le remplacement de facteurs selon les règles de . Formellement la relation est étendue par :

si et seulement il existe tels que , , et .

On rencontre aussi la notation , ce qui permet d'omettre l'indice . La relation de réécriture, notée , est la clôture réflexive et transitive de la relation ; elle est définie par une suite d'étapes

Congruence de Thue

Dans un système de semi-Thue, la relation est compatible avec l'opération de multiplication (concaténation) du monoïde libre , en d'autres termes implique pour tous les mots . Comme est un préordre, le couple forme un préordre monoïdal.

De même, la clôture réflexive transitive et symétrique de , parfois dénotée par , est une congruence, c'est-à-dire une relation d'équivalence compatible avec la concaténation. Cette congruence est appelée congruence de Thue engendrée par . Si le système de semi-Thue est symétrique, donc un système de Thue, la congruence coïncide avec la relation de réécriture.

Comme est une congruence, on peut définir le monoïde quotient du monoïde libre par la congruence de Thue, comme dans tout monoïde. Si un monoïde est isomorphe à , le système de semi-Thue est une présentation du monoïde . Par exemple, le système est une présentation du groupe libre à un générateur ; le système réduit à la seule règle est une présentation du demi-groupe bicyclique. De fait, on a[2] : Tout monoïde admet une présentation de la forme pour un système de semi-Thue, éventuellement sur un alphabet infini.

Le problème du mot

Le problème du mot pour un système de semi-Thue se formule comme suit : Étant donné un système de semi-Thue et deux mots , peut-on transformer en en appliquant des règles de  ? Ce problème est indécidable. La première preuve est de Emil Post[3]. Une autre, pratiquement en même temps, par A. Markov[4]. Les preuves sont discutées dans le livre de Davis[5].

Connexions avec d'autres concepts

Un système de semi-Thue peut être vu comme un système de réécriture de termes dont les mots sont des termes d'arité 1[6]. Un système de semi-Thue est aussi un cas particulier d'un système de Post, et réciproquement tout système de Post peut être transformé en un système de semi-Thue. Les deux formalismes sont Turing-complets, et sont donc équivalents aux grammaires de type 0 de la hiérarchie de Chomsky qui parfois sont appelées grammaires de semi-Thue[7]. Une grammaire formelle diffère d'un système de semi-Thue par la séparation de l’alphabet en symboles terminaux et non terminaux et la présence d'un axiome. On rencontre aussi la définition d'un système de semi-Thue comme triple , où est appelé l'« ensemble des axiomes »[8].

Notes

  1. Wolfgang Thomas, « "When nobody else dreamed of these things" – Axel Thue und die Termersetzung », Informatik-Spektrum, vol. 33, no 5, , p. 504–508 (ISSN 0170-6012, DOI 10.1007/s00287-010-0468-9)
  2. Book et Otto, Theorem 7.1.7, p. 149.
  3. Post 1947.
  4. Markov 1947.
  5. Davis 1965.
  6. Nachum Dershowitz (en) et Jean-Pierre Jouannaud. Rewrite Systems (1990) p. 6
  7. Daniel I. A. Cohen (en), Introduction to Computer Theory, 2nd ed., Wiley-India, 2007, (ISBN 81-265-1334-9), p.572
  8. Dan A. Simovici et Richard L. Tenney, Theory of formal languages with applications, World Scientific, 1999, (ISBN 981-02-3729-4), chapitre 4

Bibliographie

Monographies
  • Ronald V. Book (en) et Friedrich Otto, String-rewriting Systems, Springer, , 189 p. (ISBN 0-387-97965-4).
  • Matthias Jantzen, Confluent string rewriting, Birkhäuser, , 126 p. (ISBN 0-387-13715-7).
  • (en) Franz Baader et Tobias Nipkow, Term rewriting and all that, Cambridge (GB), Cambridge University Press, , 316 p. (ISBN 0-521-77920-0, lire en ligne).
Manuels
  • Martin Davis, Ron Sigal et Elaine J. Weyuker, Computability, Complexity, and Languages : Fundamentals of Theoretical Computer Science, Academic Press, , 2e éd., 609 p. (ISBN 0-12-206382-1, lire en ligne), chapitre 7
  • Elaine Rich, Automata, computability and complexity : theory and applications, Prentice Hall, , 1099 p. (ISBN 978-0-13-228806-4 et 0-13-228806-0), chapitre 23.5.
Chapitres de manuels
  • Samson Abramsky, Dov M. Gabbay, Thomas S. E. Maibaum (ed.), Handbook of Logic in Computer Science: Semantic modelling, Oxford University Press, 1995, (ISBN 0-19-853780-8).
  • Nachum Dershowitz et Jean-Pierre Jouannaud, « Rewrite Systems », dans Jan van Leeuwen (éditeur), Handbook of Theoretical Computer Science, vol. B : Formal Models and Semantics, Elsevier et MIT Press, (ISBN 0-444-88074-7, lire en ligne), p. 243-320
  • Matthias Jantzen, « Basics of Term Rewriting », dans Grzegorz Rozenberg et Arto Salomaa (éditeurs), Handbook of Formal Languages, vol. 3 : Beyond Words, Springer, (ISBN 3-540-60420-0), p. 269-337
  • Martin Davis (éditeur), The Undecidable : Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, New York, Raven Press, , 414 p. (ISBN 978-0-486-43228-1, lire en ligne) — Réimpression avec corrections par Dover en 2004.
Articles historiques
  • Axel Thue, « Die Lösung eines Spezialfalles eines generellen logischen Problems », Norske Vid. Skrifter I Mat.-Nat. Kl., Christiania, no 8, — réimpression dans les Œuvres mathématiques, p. 273–310
  • Axel Thue, « Probleme über Veränderungen von Zeichenreihen nach gegebenen Regeln », Norske Vid. Skrifter I Mat.-Nat. Kl., Christiania, no 10, — réimpression dans les Œuvres mathématiques, p. 493–524
  • Trygve Nagell, Atle Selberg, Sigmund Selberg et Knut Thalberg (éditeurs) (préf. Carl Ludwig Siegel), Selected Mathematical Papers of Axel Thue, Oslo, Universiteitsforlaget, , lviv+ 591 (ISBN 82-00-01649-8, présentation en ligne)
    Introduction par Carl Ludwig Siegel ; résumés en anglais des articles écrits en norvégien en fin de volume.
  • Emil Post, « Recursive unsolvability of a problem of Thue », Journal Symbolic Logic, vol. 12, no 1, , p. 1–11.
  • A. Markoff, « On the impossibility of certain algorithms in the theory of associative systems, », C. R. (Doklady) Acad. Sci. URSS (N.S.), vol. 55, , p. 583–586 (Math Reviews 0020528)

Voir aussi


  • Portail de la logique
  • Portail de l'informatique théorique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.