that has monadic words (functions) ending in the same variable as the left- and right-hand side terms, e.g. a term rule is equivalent to the string rule . A semi-Thue system is also a special type of Post canonical system, but every Post canonical system can also be reduced to an SRS. Both formalisms are Turing complete, and thus equivalent to Noam Chomsky's unrestricted grammars, which are sometimes called semi-Thue grammars. A formal grammar only differs from a semi-Thue system by the separation of the alphabet into terminals and non-terminals, and the fixation of a starting symbol amongst non-terminals. A minority of authors actually define a semi-Thue system as a triple , where is called the set of axioms. Under this "generative" definition of semi-Thue system, an unrestricted grammar is just a semi-Thue system with a single axiom in which one partitions the alphabet into terminals and non-terminals, and makes the axiom a nonterminal. The simple artifice of partitioning the alphabet into terminals and non-terminals is a powerful one; it allows the definition of the Chomsky hierarchy based on what combination of terminals and non-terminals the rules contain. This was a crucial development in the theory of formal languages. In quantum computing, the notion of a quantum Thue system can be developed. Since quantum computation is intrinsically reversible, the rewriting rules over the alphabet are required to be bidirectional (i.e. the underlying system is a Thue system, not a semi-Thue system). On a subset of alphabet characters one can attach a Hilbert space , and a rewriting rule taking a substring to another one can carry out a unitary operation on the tensor product of the Hilbert space attached to the strings; this implies that they preserve the number of characters from the set . Similar to the classical case one can show that a quantum Thue system is a universal computational model for quantum computation, in the sense that the executed quantum operations correspond to uniform circuit classes (such as those in BQP when e.g. guaranteeing termination of the string rewriting rules within polynomially many steps in the input size), or equivalently a Quantum Turing machine. History and importance Semi-Thue systems were developed as part of a program to add additional constructs to logic, so as to create systems such as propositional logic, that would allow general mathematical theorems to be expressed in a formal language, and then proven