Post canonical system

Post calculus

A way of defining enumerable sets (cf. Enumerable set) of words. The notion of a Post canonical system was introduced in 1943 by E. Post and was the first general notion of a calculus suitable to define arbitrary enumerable sets and not attached to the logical structure of the generated objects, to their semantics or to the logic of the derivation rules (cf. Derivation rule). A Post canonical system is given by a quadruple , where is the alphabet of the calculus, (which has no letters in common with ) is the alphabet of variables, is a list of words in (the axioms of the calculus), and is a list of derivation rules of the form

(*)

( are the designations of words in ; are the designations of letters from ). A word is obtained from by applying the rule (*) if for any letter from in (*) one can find a word in (the value of this variable) after substitution of which at all places where the considered variable appears in (*) one obtains the words above the line and the word under the line. On the basis of such understanding of rules a derivation is defined in the Post canonical system. In the theory of calculi one uses the following definition of an enumerable set of words in , which is equivalent to the usual one: is called enumerable if it coincides with a set of words in deduced in some Post canonical system whose alphabet contains (the necessity of the extension of by at least one letter is non-removable but one can require that besides only words of the form , where is in , should be derivable).

One can consider different specializations of the notion of a Post canonical system: 1) Post normal systems (all rules have the form

2) local calculi (rules of the form

3) restricted calculi (a one-letter alphabet, rules with one premise); etc.

The above-mentioned specializations are assumed to have one axiom, and an arbitrary Post canonical system can be reduced to any of them (the equivalence between a Post canonical system and a Post normal calculus (cf. Post normal system) established by Post has fundamental significance in studies in this direction in order to find unsolvable systems).

For references see Calculus.

Comments

Regular canonical systems have turned out to be of particular importance. In a regular canonical system every derivation rule is of the form "Gp yields G'p" where and are words over the alphabet of the calculus and is a variable. Further details are contained in [a1].

References

[a1]	A. Salomaa, "Computation and automata" , Cambridge Univ. Press (1985)