Un sistema de etiquetas es un modelo computacional determinista publicado por Emil Leon Post en 1943 como una forma simple de un sistema canónico Post . Un sistema de etiquetas también puede verse como una máquina abstracta, llamada máquina de etiquetas Post (que no debe confundirse con las máquinas Post-Turing ); en pocas palabras, una máquina de estados finitos cuya única cinta es una cola FIFO de longitud ilimitada, de modo que en en cada transición, la máquina lee el símbolo al principio de la cola, elimina un número constante de símbolos del principio y añade al final una cadena de símbolos que depende únicamente del primer símbolo leído en esta transición.
Debido a que todas las operaciones indicadas se realizan en una sola transición, una máquina etiquetadora tiene estrictamente un solo estado.
Se define una transformación t (llamada operación de etiqueta ) en el conjunto de palabras que no se detienen, de modo que si x denota el símbolo más a la izquierda de una palabra S , entonces t ( S ) es el resultado de eliminar los m símbolos más a la izquierda de S y agregando la palabra P(x) a la derecha. Por lo tanto, el sistema procesa la cabeza del símbolo m en una cola de longitud variable, pero la cola generada depende únicamente del primer símbolo de la cabeza.
Un cálculo por un sistema de etiquetas es una secuencia finita de palabras producidas al iterar la transformación t , comenzando con una palabra dada inicialmente y deteniéndose cuando se produce una palabra de detención. (Según esta definición, no se considera que exista un cómputo a menos que se produzca una palabra de detención en un número finito de iteraciones. Las definiciones alternativas permiten cálculos sin detención, por ejemplo, mediante el uso de un subconjunto especial del alfabeto para identificar palabras que codifican la salida).
El término sistema de etiquetas m se usa a menudo para enfatizar el número de eliminación. Las definiciones varían un poco en la literatura (cf. Referencias), siendo la que se presenta aquí la de Rogozhin.
El uso de un símbolo de parada en la definición anterior permite que la salida de un cálculo se codifique solo en la palabra final, mientras que, de lo contrario, la salida se codificaría en la secuencia completa de palabras producida al iterar la operación de etiqueta.