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 ${\displaystyle R}$ finie fixe entre mots sur un alphabet donné, dont les éléments sont appelés les règles de réécriture, et notées ${\displaystyle s\rightarrow t}$. 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 ${\displaystyle usv\rightarrow utv}$, pour une règle ${\displaystyle s\to t}$ de ${\displaystyle R}$ et des mots ${\displaystyle u}$, et ${\displaystyle v}$ 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.

Un système de semi-Thue est un couple ${\displaystyle (\Sigma ,R)}$, où ${\displaystyle \Sigma }$ est un alphabet supposé en général fini, et où ${\displaystyle R}$ est une relation binaire finie entre mots sur ${\displaystyle \Sigma }$, donc une partie finie ${\displaystyle R\subseteq \Sigma ^{*}\times \Sigma ^{*}.}$ Un élément ${\displaystyle (u,v)\in R}$ est une règle de réécriture et est habituellement écrite sous la forme ${\displaystyle u\rightarrow v}$. Si la relation ${\displaystyle R}$ est symétrique, c'est-à-dire si ${\displaystyle (u,v)\in R}$ implique ${\displaystyle (v,u)\in R}$, le système est appelé un système de Thue.

Les règles de réécriture sont étendues aux mots de ${\displaystyle \Sigma ^{*}}$ en permettant le remplacement de facteurs selon les règles de ${\displaystyle R}$. Formellement la relation est étendue par :

${\displaystyle s\rightarrow _{R}t}$ si et seulement il existe ${\displaystyle x,y,u,v\in \Sigma ^{*}}$ tels que ${\displaystyle s=xuy}$, ${\displaystyle t=xvy}$, et ${\displaystyle u\rightarrow v\in R}$.

On rencontre aussi la notation ${\displaystyle s\Rightarrow t}$, ce qui permet d'omettre l'indice ${\displaystyle R}$. La relation de réécriture, notée ${\displaystyle \rightarrow _{R}^{*}}$, est la clôture réflexive et transitive de la relation ${\displaystyle \rightarrow _{R}}$; elle est définie par une suite d'étapes

${\displaystyle s_{0}\to _{R}s_{1}\to _{R}s_{2}\to _{R}\cdots }$

Dans un système de semi-Thue, la relation ${\displaystyle \rightarrow _{R}^{*}}$ est compatible avec l'opération de multiplication (concaténation) du monoïde libre ${\displaystyle \Sigma ^{*}}$, en d'autres termes ${\displaystyle x\rightarrow _{R}^{*}y}$ implique ${\displaystyle uxv\rightarrow _{R}^{*}uyv}$ pour tous les mots ${\displaystyle u,v\in \Sigma ^{*}}$. Comme ${\displaystyle \rightarrow _{R}^{*}}$ est un préordre, le couple ${\displaystyle \left(\Sigma ^{*},\cdot ,\rightarrow _{R}^{*}\right)}$ forme un préordre monoïdal.

De même, la clôture réflexive transitive et symétrique de ${\displaystyle \rightarrow _{R}}$, parfois dénotée par ${\displaystyle {\overset {*}{\underset {R}{\longleftrightarrow }}}}$, 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 ${\displaystyle R}$. 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 ${\displaystyle {\overset {*}{\underset {R}{\longleftrightarrow }}}}$ est une congruence, on peut définir le monoïde quotient ${\displaystyle M_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\longleftrightarrow }}}}$ du monoïde libre ${\displaystyle \Sigma ^{*}}$ par la congruence de Thue, comme dans tout monoïde. Si un monoïde ${\displaystyle {\mathcal {M}}}$ est isomorphe à ${\displaystyle M_{R}}$, le système de semi-Thue ${\displaystyle (\Sigma ,R)}$ est une présentation du monoïde ${\displaystyle {\mathcal {M}}}$. Par exemple, le système ${\displaystyle R=\{ab\to \varepsilon ,ba\to \varepsilon \}}$ est une présentation du groupe libre à un générateur ; le système réduit à la seule règle ${\displaystyle ab\to \varepsilon }$ est une présentation du demi-groupe bicyclique. De fait, on a^[2] : Tout monoïde admet une présentation de la forme ${\displaystyle (\Sigma ,R)}$ pour un système de semi-Thue, éventuellement sur un alphabet infini.

Le problème du mot pour un système de semi-Thue se formule comme suit : Étant donné un système de semi-Thue ${\displaystyle (\Sigma ,R)}$ et deux mots ${\displaystyle u,v\in \Sigma ^{*}}$, peut-on transformer ${\displaystyle u}$ en ${\displaystyle v}$ en appliquant des règles de ${\displaystyle R}$ ? 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].

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 ${\displaystyle (\Sigma ,A,R)}$, où ${\displaystyle A\subseteq \Sigma ^{*}}$ est appelé l'« ensemble des axiomes »^[8].

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Semi-Thue systems » (voir la liste des auteurs).

Monographies

• Ronald V. Book et Friedrich Otto, String-rewriting Systems, Springer, 1993, 189 p. (ISBN 0-387-97965-4).
• Matthias Jantzen, Confluent string rewriting, Birkhäuser, 1988, 126 p. (ISBN 0-387-13715-7).
• (en) Franz Baader et Tobias Nipkow, Term rewriting and all that, Cambridge (GB), Cambridge University Press, 1999, 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, 1994, 2^e éd., 609 p. (ISBN 0-12-206382-1, lire en ligne), chapitre 7
• Elaine Rich, Automata, computability and complexity : theory and applications, Prentice Hall, 2007, 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, 1990 (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, 1997 (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, 1965, 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, n^o 8,‎ 1910 — 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, n^o 10,‎ 1914 — 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, 1977, 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, n^o 1,‎ 1947, 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,‎ 1947, p. 583–586 (MR 0020528)

• L-Système
• Système de Post

• Portail de la logique
• Portail de l'informatique théorique