Voir la source de Système de Post

En [[informatique théorique]] et en [[logique mathématique]], un '''système de Post''', ou '''système canonique de Post''', appelé ainsi d’après son créateur [[Emil Post]], est un système de manipulation de [[Chaîne de caractères|chaînes de caractères]] qui commence avec un nombre fini de [[Mot (mathématiques)|mots]] et les transforme par application d’un [[ensemble fini]] de règles d’une forme particulière, et par là engendre un [[langage formel]]. Ces système ont surtout un intérêt historique car tout système de Post peut être réduit à un système de [[Réécriture (informatique)|réécriture]] de mots (un système de semi-Thue) qui est une formulation plus simple. Les deux formalismes -- système de Post et réécriture -- sont [[Turing-complet]]s.

== Un exemple : les expressions bien parenthésées ==
Un système de Post est la donnée d'un alphabet, un ensemble de mots initiaux et de règles de production. Par exemple :
* Un alphabet constitué des deux caractères  <code><math>[</math></code> et <code><math>]</math></code>;
* L'ensemble qui contient le mot <code>[]</code>comme seul mot initial ;
* Les trois règles de production suivantes : 
#  <math> X \to [X]</math>
#  <math> X \to XX</math>
#  <math> X_1X_2 \to X_1[\ ]X_2</math>
Voici quelques mots dérivés :
{| class="wikitable"
|<code>[]</code>
|mot initial
|-
|<code>[][]</code>
|obtenu par la règle 2.
|-
|<code>[[][]]</code>
|obtenu par la règle 1.
|-
|<code>[[][]][[][]]</code>
|obtenu par la règle 2.
|-
|<code>[[][]][][[][]]</code>
|obtenu par la règle 3.
|}
== Définition formelle ==

Un '''système canonique de Post''' est un triplet <math>(A,I,R)</math>, où

* <math>A</math> est un alphabet fini ; 
* <math>I</math> est un ensemble fini de ''mots initiaux'' sur l'alphabet ''<math>A</math>'' ;
* <math>R</math> est un ensemble fini de règles de transformation de mots, appelées ''règles de production''.
Chaque règle est de la forme :
:<math>g_1,\ldots, g_k \to h</math>
où <math>g_1,\ldots,g_k</math> et <math>h</math> sont des mots fixes contenant des ''variables'', notées <math>X_{i,j}</math> et <math>Y_k</math> respectivement, de la forme
:<math>g_i=g_{i0}X_{i1}g_{i1}X_{i2}g_{i2}\cdots X_{im_i}g_{im_i}</math>
et
:<math>h=h_0Y_1h_1Y_2h_2\cdots Y_nh_n</math>.
Les mots <math>g_i</math> sont appelés les ''antécédents'',  le mot <math>h</math> le ''conséquent'' de la règle. La condition requise est que chaque <math>Y_k</math>  dans le conséquent figure parmi les variables <math>X_{i,j}</math> des antécédents, et que chaque conséquent et antécédent contient au moins une variable.

En général, une règle de production ne contient qu'un seul antécédent<ref>C’est la définition de Dexter Kozen {{harv|Kozen|1997|p=256-257}}.</ref>, auquel cas elle s'écrit plus simplement
:<math>g_0X_{1}g_{1}X_{2}g_{2}\cdots X_{m}g_{m} \to h_0Y_1h_1Y_2h_2\cdots Y_n h_n  </math>.

On peut appliquer une règle à un mot <math>w</math> s'il se factorise selon l'antécédent de la règle, en associant à chaque variable un facteur du mot. Le mot obtenue est alors celui où les variables du conséquent sont remplacées par les valeurs associées aux variables dans l'antécédent. Dans le cas de plusieurs antécédents, le mot <math>w</math> doit se factoriser selon chacun des antécédents pour dériver le conséquent. Post lui-même a prouvé, preuve reprise dans le livre de Minsky<ref>{{harvsp|Minsky|1967|p=}}.</ref> a prouvé que l’on peut se contenter de règles avec un seul antécédent.

Le [[Langage formel|langage]] ''engendré'' par le système de Post est l’ensemble des mots composés des mots initiaux et des mots que l’on obtient par une application répétée de règles de production. Ces ensembles sont des langages [[récursivement énumérable]]s et, réciproquement, tout langage récursivement énumérable est la restriction d’un tel ensemble à un sous-alphabet de <math>A</math>.

== Théorème de forme normale ==
Un système de Post est en '''forme normale''' (''normal form'') si toutes ses règles sont de la forme

: <math> gX \ \rightarrow \ Xh </math>

Les règles en forme normale consistent  donc à enlever le préfixe <math>g</math> au début d' un mot et d'ajouter le mot <math>h</math> à la fin. Post a démontré en 1943<ref>{{Harvsp|Post|1943|p=}}.</ref> le théorème de forme normale suivant :  
{{Théorème|nom=Théorème de forme normale de Post|énoncé=Pour tout système de Post, il existe un système de Post en forme normale équivalent ; ce système peut être construit effectivement.}}

Les [[Système de tague|systèmes de tague]] qui eux aussi sont un modèle de calcul universel, sont des exemples particuliers de systèmes de Post en forme normale ; ils sont de plus « monogènes » : Un système est dit ''monogène'' si, pour toute chaîne, il existe au plus un nouveau mot peut être produit, en d’autres termes, si le système est déterministe.

== Systèmes de réécriture et grammaires de type 0 ==
Un [[Réécriture (informatique)#Systèmes de réécriture |système de réécriture ]] est un cas particulier d’un système de Post où les productions sont de la forme : 
: <math> X_1 g X_2  \ \rightarrow \ X_1  h X_2 </math>
Les productions sont des règles de substitution, aussi écrites sous la forme <math>g\to h</math>. On peut démontrer que tout système de Post peut être ramené à un tel système, qui est une [[grammaire formelle]] de type 0 dans la [[hiérarchie de Chomsky]].

== Notes et références ==
{{Traduction/Référence|en|Post canonical system|725029631|type=note}}
{{Références}}

== Bibliographie ==
* {{Article
|langue=
|auteur1= [[Emil Post]]
|titre= Formal Reductions of the General Combinatorial Decision Problem
|périodique= [[American Journal of Mathematics]]
|volume= 65
|numéro= 2
|date= 1943
|pages= 197-215
}}.
* {{Ouvrage
|auteur1=[[Marvin Minsky]]
|titre=Computation
|sous-titre=Finite and Infinite Machines
|éditeur=Prentice-Hall
|année=1967
|pages totales=317
|isbn=978-0-13-165563-8
}}.
*{{Ouvrage
|auteur1=[[Dexter C. Kozen]]
|titre=Automata and Computability
|éditeur=Springer
|collection=Undergraduate Texts in Computer Science
|année=1997
|pages totales=400
|isbn=978-0-387-94907-9
|lire en ligne=https://books.google.com/books?id=8lKyxS8_CNoC&printsec=frontcover
}}.

== Articles connexes ==

* [[Réécriture (informatique)]]
* [[Machine de Turing]]
* [[Système de tague]]
* [[Automate à file]]

{{Palette|Langages formels grammaires et automates}}
{{Portail|Informatique théorique|Logique}}

[[Catégorie:Langage formel]]
[[Catégorie:Modèle de calcul]]