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înes de caractères qui commence avec un nombre fini de 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 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-complets.
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 et ;
L'ensemble qui contient le mot []comme seul mot initial ;
Les trois règles de production suivantes :
Voici quelques mots dérivés :
Un système canonique de Post est un triplet , où
est un alphabet fini ;
est un ensemble fini de mots initiaux sur l'alphabet ;
est un ensemble fini de règles de transformation de mots, appelées règles de production.
Chaque règle est de la forme :
où et sont des mots fixes contenant des variables, notées et respectivement, de la forme
et
Les mots sont appelés les antécédents, le mot le conséquent de la règle. La condition requise est que chaque dans le conséquent figure parmi les variables 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, auquel cas elle s'écrit plus simplement
On peut appliquer une règle à un mot 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 doit se factoriser selon chacun des antécédents pour dériver le conséquent.