View source for Post canonical system

<!--
p0740001.png
$#A+1 = 33 n = 0
$#C+1 = 33 : ~/encyclopedia/old_files/data/P074/P.0704000 Post canonical system,
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

''Post calculus''

A way of defining enumerable sets (cf. [[Enumerable set|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|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|Derivation rule]]). A Post canonical system is given by a quadruple  $  A , P , {\mathcal A} , \pi $, 
where  $  A $
is the alphabet of the calculus,  $  P $(
which has no letters in common with  $  A $) 
is the alphabet of variables,  $  {\mathcal A} $
is a list of words in  $  A $(
the axioms of the calculus), and  $  \pi $
is a list of derivation rules of the form

$$ \tag{* }

\begin{array}{c}
G _ {1,1} p _ {1,1} \dots G _ {1 , n _ {1}  } p _ {1, n _ {1}} G _ {1 , n _ {1}  + 1 }  \\
\dots \dots \dots \dots  \\
G _ {m,1} p _ {m,1} \dots G _ {m , n _ {m}  } p _ {m, n _ {m}} G _ {m , n _ {m}  + 1 } \\
\\
\hline \\
G _ {1} p _ {1} \dots G _ {n} p _ {n} G _ {n+1}
\end{array}

$$

( $  G _ {i,j} $
are the designations of words in  $  A $; 
$  p _ {i,j} $
are the designations of letters from  $  P $). 
A word  $  Q $
is obtained from  $  Q _ {1} \dots Q _ {m} $
by applying the rule (*) if for any letter from  $  P $
in (*) one can find a word in  $  A $(
the value of this variable) after substitution of which at all places where the considered variable appears in (*) one obtains the words  $  Q _ {1} \dots Q _ {m} $
above the line and the word  $  Q $
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  $  A $, 
which is equivalent to the usual one:  $  M $
is called enumerable if it coincides with a set of words in  $  A $
deduced in some Post canonical system whose alphabet contains  $  A $(
the necessity of the extension of  $  A $
by at least one letter  $  \xi $
is non-removable but one can require that besides  $  M $
only words of the form  $  \xi Q $, 
where  $  Q $
is in  $  A $, 
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

$$ 
\left . 
\frac{G p }{p G  ^  \prime  }
 \right ) ;
$$

2) local calculi (rules of the form

$$ 
\left . 
\frac{p _ {1} G p _ {2} }{p _ {1} G  ^  \prime  p _ {2} }
 \right ) ;
$$

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|Post normal system]]) established by Post has fundamental significance in studies in this direction in order to find unsolvable systems).

For references see [[Calculus|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  $  G $
and  $  G  ^  \prime  $
are words over the alphabet of the calculus and  $  p $
is a variable. Further details are contained in [[#References|[a1]]].

====References====
<table>
<TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Salomaa,   "Computation and automata" , Cambridge Univ. Press  (1985) {{ZBL|0565.68046}}</TD></TR>
</table>