Post Canonical Systems

Origin. Emil Post, "Formal reductions of the general combinatorial decision problem" (American Journal of Mathematics 65, 1943, pp. 197–215), defining canonical and normal systems and proving the normal-form theorem. The formalism is two decades older than its publication: Post reached it, together with the unsolvability it implies, in his Princeton work of the early 1920s, published only as "Absolutely unsolvable problems and relatively undecidable propositions — account of an anticipation" in Martin Davis's The Undecidable (Raven Press, 1965). "Recursive unsolvability of a problem of Thue" (Journal of Symbolic Logic 12, 1947, pp. 1–11) carried the formalism into algebra, settling the word problem for semigroups; Markov proved the same result independently. The second life began when Allen Newell and Herbert Simon made production rules the medium of their cognitive theory in Human Problem Solving (1972); Charles Forgy's Carnegie Mellon thesis "On the efficient implementation of production systems" (1979) and the Carnegie Mellon OPS languages culminating in his OPS5 made production systems a programming practice, and "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem" (Artificial Intelligence 19, 1982, pp. 17–37) supplied its match algorithm.

Models. A canonical system is an alphabet, a finite set of primitive assertions (words taken as axioms), and a finite set of productions, each carrying the strings that match its antecedent templates to the corresponding instance of its consequent template. Derivability is the consequence relation, and the set of derivable words is the system's language: the generative content of a formal system and nothing else, with Post's thesis the claim that every formal system can be put in this shape. The entry's point is the double legacy. One line runs to formal grammars — an unrestricted grammar is a canonical system over terminals and nonterminals, and Pullum ("On the Mathematical Foundations of Syntactic Structures", Journal of Logic, Language and Information 20, 2011, pp. 277–296) documents that the rewriting formalism of Chomsky's Syntactic Structures comes directly from Post's production systems, which the book does not cite. The other runs through Newell and Simon to the production systems of AI: working memory in place of axioms, condition-action rules in place of productions, the recognize-act cycle in place of derivation. Among the neighbours, Petri nets fire ground rules over multisets (a transition consumes its matched tokens and produces its outputs as a rule retracts and asserts facts), and rewriting logic is the generalization from strings to terms modulo equations.

Formalism.

Canonical system: alphabet Σ; primitive assertions (axiom words over Σ); finitely many productions. Generated set = closure of the axioms under the productions.

Production: g₀ P₁ g₁ P₂ g₂ … Pₘ gₘ → h₀ Pᵢ₁ h₁ Pᵢ₂ h₂ … Pᵢₙ hₙ The g and h are fixed words, possibly empty; the P are variables ranging over words of Σ. Several antecedent templates allowed; every variable of the consequent occurs in an antecedent.

Normal system: a single axiom; every production of the shape g P → P h Post (1943): every canonical system reduces to a normal system over an enlarged alphabet, and restricted to words of the original alphabet the two generated sets coincide.

Tag system: the further specialization. Deletion number m; each letter assigned a word. Step: read the first letter, delete the first m letters, append that letter's word. Introduced in the 1943 paper as a simple form of canonical system; the name, suggested by B. P. Gill, is the children's game.

Production-rule system (the AI descendant): Working memory: ground facts. Rules: conditions with variables and negated conditions → actions asserting and retracting facts. Recognize–act cycle: match all conditions against working memory; conflict resolution picks one instantiation (recency, specificity); act; repeat. Conflict resolution is control, not logic.

Symbols.

Metatheory. Canonical systems generate exactly the recursively enumerable sets, so the formalism is Turing-complete and derivability is undecidable in general; Post proved the reductions among his own systems in the 1943 paper; the correspondence problem ("A variant of a recursively unsolvable problem", Bulletin of the American Mathematical Society 52, 1946) and Thue's word problem (1947) carried the unsolvability into formal language theory and algebra, the latter the same undecidability Equational Logic records for finitely presented semigroups. Minsky ("Recursive unsolvability of Post's problem of 'tag' and other topics in theory of Turing machines", Annals of Mathematics 74, 1961, pp. 437–455) proved the halting problem for tag systems unsolvable, and Cocke and Minsky (1964) showed tag systems with deletion number 2 already universal. On the production-system side the central result concerns the match. Rete (Forgy 1979, 1982) compiles the rule conditions into a dataflow network (alpha nodes testing single facts, beta nodes joining partial matches, memories at the nodes), so that each change to working memory propagates as a delta through the network instead of a rescan of every rule against every fact; read logically, it computes the set of rule instantiations incrementally, the production-system counterpart of Datalog's semi-naive evaluation. TREAT (Miranker, "TREAT: A Better Match Algorithm for AI Production Systems", AAAI-87, pp. 42–47) keeps the conflict set and the alpha memories but no beta memories, recomputing joins as rules fire, and outperformed Rete by more than fifty percent on the OPS5 programs tested. The monotone fragment — no retraction, no negated conditions — computes the least fixed point of the immediate-consequence operator, the same T_P iteration that gives Horn Logic its least model and Datalog its bottom-up semantics. Retraction and negated conditions make a run nonmonotonic: a fired rule's conclusion can lose its support, the bookkeeping that withdraws it is the justification network of a Truth Maintenance System, and the consequence relations that tolerate such withdrawal are the subject of the Structural/Nonmonotonic division.

Applies to. The reduction toolkit of computability theory — the word problem for semigroups, the problem of tag, and the Post correspondence problem are stock sources of undecidability, the last the standard one in formal language theory. The ancestry of formal grammars and the Chomsky hierarchy. Rule engines and business-rule systems: the recognize-act cycle over working memory is what CLIPS-style engines implement. Cognitive modeling in the Newell–Simon line, where human problem-solving behavior is simulated as production firing.

Limitations. Conflict resolution is extra-logical: which enabled rule fires is settled by recency, specificity, or insertion order, so a production system's run is not determined by its logical content, and two engines agreeing on the rules can disagree on the result. Retraction forfeits monotonicity and with it the least-model guarantee; what replaces the guarantee is justification bookkeeping, and Truth Maintenance records its failure case — a network with an odd loop through a negated condition admits no labelling at all. The formalism is syntax over strings or ground tuples, with no terms and no quantifiers: first-order Horn clauses add both, Datalog adds the relational reading over a finite database, and each has a model-theoretic semantics where a canonical system has only its generated set. Post's normal-form austerity — one axiom, productions g P → P h — is what makes the systems the right source for undecidability reductions and what makes them unusable directly, since encoding any actual problem into a normal system is itself a reduction.

© 2026 Lingenic LLC