Post Canonical Systems

A Python implementation of Emil Post's formal string rewriting systems for computation and formal language exploration.

What is this?

Post Canonical Systems are a foundational model of computation developed by mathematician Emil Post in the 1920s. They define formal languages through string rewriting: starting from initial words (axioms) and repeatedly applying production rules to generate new strings. Despite their simplicity, Post systems are Turing-complete and serve as an elegant framework for exploring computability, formal grammars, and proof derivations.

Features

Installation

pip install post-canonical

Or with uv:

uv add post-canonical

Quick Start

from post_canonical.builder import SystemBuilder

# Build the MU puzzle from Godel, Escher, Bach
system = (SystemBuilder("MIU")
    .var("x")
    .var("y")
    .axiom("MI")
    .rule("$xI -> $xIU", name="add_U")
    .rule("M$x -> M$x$x", name="double")
    .rule("$x III $y -> $x U $y", name="III_to_U")
    .rule("$x UU $y -> $x$y", name="delete_UU")
    .build())

# Generate all derivable words up to 3 steps. The default `max_steps=10`
# prevents accidental runaway on systems whose word set explodes; raise
# it (or use `iterate()`) for deeper exploration. Results come back
# already ordered by length, then lexicographically.
words = system.generate_words(max_steps=3)
print(words)
# ('MI', 'MII', 'MIU', 'MUI', 'MIIU', 'MIIII', 'MIUIU', 'MIIIIU',
#  'MIIUIIU', 'MIIIIIIII', 'MIUIUIUIU')

# Check if a word is reachable
from post_canonical.query import ReachabilityQuery

query = ReachabilityQuery(system)
print(query.is_derivable("MU", max_words=10000))
# 'MU' NOT_FOUND after exploring 10000 words

Variables use $ prefix in patterns ($x, ${x}). Whitespace is ignored, so $x III $y reads cleanly. Three variable kinds are available:

builder = (SystemBuilder("abc")
    .var("x")                      # ANY: matches "" or "a" or "abc"...
    .var("y", kind="non_empty")    # NON_EMPTY: matches "a" or "abc"...
    .var("z", kind="single")       # SINGLE: matches exactly one symbol
)

Pattern syntax

The pattern grammar is intentionally tiny:

pattern    ::= element+
element    ::= constant | variable
constant   ::= [^$]+
variable   ::= "${" name "}"          (canonical)
             | "$" name                (shorthand)
name       ::= [A-Za-z_][A-Za-z0-9_]*

Pattern.parse accepts only the canonical ${name} form to avoid ambiguity when a variable name could be confused with the trailing constant. The SystemBuilder DSL accepts both $x and ${x} and normalizes them.

CLI

The package includes an interactive REPL for exploring systems without writing code:

$ pcs
Post Canonical Systems REPL vX.Y.Z          # the live REPL prints the current __version__
Type 'help' for commands.

pcs> alphabet MIU
Alphabet set: {I, M, U}

pcs> axiom MI
Axiom added: MI

pcs> var x
Variable added: x (ANY)

pcs> rule "$xI -> $xIU"
Rule added: $xI -> $xIU

pcs> rule "M$x -> M$x$x"
Rule added: M$x -> M$x$x

pcs> generate 3
Generated 8 words:
  MI, MII, MIU, MIII, MIIU, MIIII, MIIIU, MIUIU

pcs> query "MU"
'MU' NOT_FOUND after exploring 10000 words

pcs> exit
Goodbye.

Visualization

Export derivations as DOT/GraphViz, LaTeX, Mermaid, or ASCII trees:

from post_canonical import create_mu_puzzle
from post_canonical.visualization import to_ascii_tree

system = create_mu_puzzle()
for dw in system.generate(max_steps=3):
    if dw.word == "MIIII":
        print(to_ascii_tree(dw.derivation))
        break

MIIII
+-- MII (double)
    +-- MI (axiom)

Preset Systems

Requirements

• Python 3.12+
• No external dependencies

License

MIT