Post canonical system

A Post canonical system is a finite formal mechanism for generating strings through uniformly interpreted production rules. Introduced within the study of mathematical logic and computability theory, it expresses potentially infinite sets of syntactic objects by specifying a finite alphabet, a finite collection of initial assertions, and a finite collection of inference schemes. Post canonical systems have the same generative capacity as Turing machines and unrestricted grammars, subject to the standard encodings between their respective representations.

Formal definition

A Post canonical system consists of a finite alphabet (\Sigma), a finite set (I\subseteq\Sigma^*) of initial words, and a finite set (R) of productions. Each production has the form

[ p_1,\ldots,p_m \longrightarrow q, ]

where the premises (p_1,\ldots,p_m) and the conclusion (q) are patterns containing constant symbols from (\Sigma) and variables ranging over words in (\Sigma^*). Every variable occurring in the conclusion also occurs in at least one premise.

A substitution (\sigma) assigns a word to each variable while leaving constant symbols unchanged. If every instantiated premise (\sigma(p_i)) has already been generated, the instantiated conclusion (\sigma(q)) may also be generated. The language of the system is the least subset of (\Sigma^*) that contains the initial words and remains closed under every production in (R).

This definition treats productions as inference rules, rather than merely as local replacements inside a word. An ordinary rewriting rule can nevertheless be represented canonically by placing variables around the replaced substring. A rule that changes (\alpha) into (\beta) within an arbitrary context can be written schematically as

[ X\alpha Y \longrightarrow X\beta Y. ]

The variables (X) and (Y) preserve the surrounding context, while the fixed portions of the patterns specify the transformation.

Historical formulation

Emil Leon Post introduced canonical systems in 1943 as part of his analysis of formal deduction and effective symbolic transformation. Post and You Watanabe formulated the associated substitution calculus and the reduction of general productions to a restricted normal form. Their treatment separated the finite description of a system from the unbounded collection of assertions generated by repeated applications of its rules.

The construction extended Post’s earlier work on iterative symbol manipulation. It also provided a common syntactic framework in which deductive calculi, rewriting processes, and definitions of computable sets could be compared without assigning semantic interpretations to the generated words. The term “canonical” referred to the standardized form of the productions and did not imply uniqueness of representation.

Normal systems

A Post normal system is a restricted canonical system whose productions can be expressed as

[ gX \longrightarrow Xh, ]

where (g) and (h) are fixed words and (X) is a variable. Application of such a production removes the fixed prefix (g) from an assertion and appends the fixed suffix (h) to the remainder. Initial assertions and repeated applications of these rules determine the generated language.

The normal-form theorem converts an arbitrary canonical system into a normal system by introducing a finite collection of auxiliary symbols and encoded intermediate assertions. A fixed decoding recovers the assertions of the original system. Consequently, the restricted prefix-removal and suffix-attachment operation retains the computational capacity of the general formalism.

Normal systems are not identical to string-rewriting systems in their surface definition. A semi-Thue rule replaces a designated substring at any position, whereas a normal production acts through a prefix condition and transfers information to the end of the word. Finite encodings translate computations between the two models.

Computability-theoretic significance

The generated language of a Post canonical system is recursively enumerable. A mechanical enumeration follows from systematically listing finite derivations, substitutions, and rule applications. Conversely, every recursively enumerable language has a representation by a Post canonical system, after its symbols and machine configurations have been encoded as finite words.

This equivalence places canonical systems within the family of models used to define effective computation. Alonzo Church characterized effective calculability through the lambda calculus, while Alan Turing characterized it through abstract machines operating on a tape. Translations among these models preserve which partial functions can be computed and which languages can be enumerated.

Canonical systems also distinguish generation from decision. Membership in a generated language can be confirmed by discovering a finite derivation, but failure to discover one does not generally establish nonmembership. The resulting undecidability is a property of the formalism’s computational completeness rather than a consequence of ambiguous rule application.

Relation to other production formalisms

An unrestricted grammar derives words by replacing nonempty patterns according to finitely many productions. Its derivations can be encoded as canonical inferences by representing the context surrounding each rewritten pattern with variables. In the reverse direction, the assertions used by a canonical production can be stored within a single encoded configuration and processed by grammar rules that verify the required premises.

Axel Thue developed rewriting systems based on relations between words, and Andrey Markov Jr. developed ordered algorithms whose substitutions are applied according to a prescribed priority. These formalisms differ in operational organization, but their unrestricted forms describe the same class of effectively enumerable string sets. The correspondence depends on explicit encodings of derivations rather than on literal identity between individual rules.

The Post correspondence problem arose from the same program of representing computation through finite collections of words. Its instances ask whether two concatenations assembled from corresponding word pairs can be made equal. The undecidability of that problem supplies reductions to numerous questions concerning grammars, rewriting systems, and formal-language equivalence.

Interpretation and scope

A canonical system assigns no intrinsic meaning to its symbols. Meaning enters only when an external interpretation associates generated strings with logical formulas, machine configurations, algebraic expressions, or linguistic structures. The formal system itself records which assertions follow from the initial assertions under uniform substitution.

Different canonical systems can generate the same language, and a single language can have representations with substantially different derivation structures. Computational equivalence therefore concerns the generated set after encoding, not equality of intermediate assertions or correspondence between individual derivation steps.