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