Infinite graphs, and how far first-order logic reaches

Infinite graphs, and how far first-order logic reaches#

The structures in the other notebooks are infinite but tame: arithmetic, orders, lattices. This one is about infinite graphs — the Cayley graph of \(\mathbb{Z}^n\), the infinite \(k\)-regular tree, the configuration graph of a Turing machine, and the configuration graph of a level 2 collapsible pushdown system.

The last two are the interesting pair. Both present computation as a graph: vertices are machine configurations, edges are single steps. Both have a decidable first-order theory. But reachability — is there a run of any length from here to there — is undecidable for the Turing machine and decidable for the collapsible pushdown system, and that difference is visible in what the library can hand you.

Variable naming. The formula parser treats a name as a variable only if it matches [a-df-z][0-9]* — a single lowercase letter (never e, which is the parser’s event marker), optionally followed by digits.

The integer grid#

\(\mathbb{Z}^n\) with its Cayley graph: vertices are integer points, and two are adjacent when they differ by one in a single coordinate. It is built as an asynchronous product of \(n\) copies of \((\mathbb{Z}, +)\) — the product that advances exactly one coordinate and holds the rest, which is precisely a grid step.

from autstr.infinite_graphs import IntegerGrid

grid = IntegerGrid(2)
S = grid.symbolic()
x, y = S.vars('x y')

print('(0,0) — (0,1):', ((0, 0), (0, 1)) in x.adj(y))
print('(0,0) — (1,1):', ((0, 0), (1, 1)) in x.adj(y), '  (diagonals are not edges)')
print('symmetric:    ', grid.is_symmetric())

neighbours = [b for (a, b), _ in zip(iter(x.eq((0, 0)) & x.adj(y)), range(4))]
print('neighbours of the origin:', neighbours)

(0,0) — (0,1): True
(0,0) — (1,1): False   (diagonals are not edges)
symmetric:     True
neighbours of the origin: [(0, 1), (0, -1), (1, 0), (-1, 0)]

Vertices are Python tuples because the structure ships a codec: the points go in and come out as (a, b), while underneath each is a word over a product alphabet.

The regular tree#

The infinite \(k\)-regular tree \(T_k\): vertices are finite words over \(k\) letters, each with \(k\) children. It carries the child relation, the successors S0…S{k-1} individually, and the prefix order — an ancestor relation, which is what makes it more than a graph.

from autstr.infinite_graphs import RegularTree

tree = RegularTree(2)
print('relations:', tree.get_relation_symbols())

T = tree.symbolic()
u, v = T.vars('u v')
print('root — its 0-child:  ', ((), (0,)) in u.adj(v))
print('root is an ancestor: ', tree.check('exists u.(all v.(Prefix(u,v)))'))
print('nobody is their own child:',
      tree.check('all u.(all v.(Child(u,v) -> (not Eq(u,v))))'))

relations: ['U', 'Eq', 'Prefix', 'S0', 'S1', 'Child', 'E']
root — its 0-child:   True
root is an ancestor:  True
nobody is their own child: True

Turing machines: where first-order logic stops#

A configuration is a state, a tape and a head position; one step is an edge. The step relation is automatic — it rewrites a bounded window of the tape — so the whole configuration graph is an automatic structure and its first-order theory is decidable.

What you may not ask is whether one configuration reaches another. That is the halting problem, and no amount of cleverness puts it inside first-order logic over this graph. So autstr.turing gives you E and Halt, and stops there.

from autstr.turing import TuringMachine, Configuration

# two states, flipping a bit and stepping right, then back
flipper = TuringMachine({('a', '0'): ('b', '1', 'R'),
                         ('a', '1'): ('b', '0', 'R'),
                         ('b', '0'): ('a', '0', 'L'),
                         ('b', '1'): ('a', '1', 'L')}, blank='0')

machine = flipper.configuration_graph()
print('relations:    ', machine.get_relation_symbols())
print('deterministic:', machine.is_deterministic())

start = Configuration('a', ('1', '0'), 0)
after = flipper.step(start)
print('one step:', start.state, start.tape, start.head, '->',
      after.state, after.tape, after.head)

M = machine.symbolic()
p, q = M.vars('p q')
print('and that step is an edge:', (start, after) in p.adj(q))

relations:     ['U', 'Eq', 'E', 'Halt']
deterministic: True
one step: a ('1', '0') 0 -> b ('0', '0') 1
and that step is an edge: True

Determinism is first-order — “every configuration has at most one successor” quantifies over one step, not over runs — so it costs nothing beyond E. Reachability would quantify over runs of unbounded length, and that is exactly the line first-order logic does not cross.

Collapsible pushdown graphs: where reachability comes back#

A level 2 collapsible pushdown system has a stack of stacks. It can clone the topmost word, push a letter carrying a collapse link back to the stack it was created over, pop, and collapse — jump straight back to that stack, however far away it now is. These systems generate the level 2 graphs of the pushdown hierarchy.

Their configuration graphs are tree-automatic rather than string-automatic (Kartzow), and that is not a technicality: their MSO theory is undecidable, so the tree encoding is the only automatic route to them. A stack of stacks is a tree of blocks, and each stack operation is a bounded rewrite at the end of the tree’s last path.

The payoff is the contrast with the Turing machine above. Here reachability is first-order definable — a relation of the graph like any other — so you may ask about runs of unbounded length.

from autstr.collapsible import Level2CPS

# clone the topmost word, then pop it back off
system = Level2CPS([('0', None, 'c', '1', 'clone'),
                    ('1', None, 'o', '0', 'pop 2')], symbols=('a',))
graph = system.configuration_graph()

print('relations:', graph.get_relation_symbols())

relations: ['U', 'Eq', 'E', 'Edgec', 'Edgeo', 'State0', 'State1', 'Topa', 'TopBottom', 'Level1', 'Level2', 'Clone', 'Pop1', 'Pop2', 'Collapse', 'Reach']

Reach is in that list but not yet built: it is exponential in the number of control states, so it is declared up front and compiled the first time a query mentions it. That deferral is the opt-out — nothing pays for it until it is asked for.

Kartzow’s construction is a decomposition rather than a fixpoint. Every run splits into four stretches — whole words come off the stack, then letters come off, then letters go back on, then words go back on — and each stretch is its own automaton. All four relations are reflexive, so composing them excludes nothing, and reachability is the first-order formula

\[\mathrm{Reach}(x,y) \;=\; \exists d\, \exists f\, \exists g.\; A(x,d) \wedge B(d,f) \wedge C(f,g) \wedge D(g,y)\]

over the four — no fifth automaton, and no fixpoint over trees.

import time

t = time.perf_counter()
reach = graph.presentation.relation('Reach')          # built on first use
print(f'Reach: {reach.num_states} states, built in {time.perf_counter() - t:.1f}s')

# properties of runs of ANY length -- the questions the Turing graph cannot answer
print('reflexive:        ', graph.check('all x.(Reach(x,x))'))
print('contains one step:', graph.check('all x.(all y.(E(x,y) -> Reach(x,y)))'))
print('transitive:       ', graph.check(
    'all x.(all y.(all z.((Reach(x,y) & Reach(y,z)) -> Reach(x,z))))'))

Reach: 29 states, built in 0.6s
reflexive:         True
contains one step: True
transitive:        True

Transitivity is worth pausing on. It is a statement about all configurations and all runs between them, decided by automata operations in well under a second — and it is not a test that was passed, it is a theorem that was proved.

Constraining the labels a run may read is reach_along, which builds Kartzow’s \(\mathrm{Reach}_L\) by putting the label automaton into a product system whose ordinary reachability is the answer. An \(\varepsilon\)-contraction — any number of silent steps followed by one visible one — is the special case of that with a two-state label automaton.

Keeping what was expensive#

Reach cost real work to build, and nothing about it depends on the session. Tree presentations serialize exactly as string ones do, so it can be written out and read back — the reloaded relation is still reachability.

import tempfile, os
from autstr.tree_presentations import TreeAutomaticPresentation

path = os.path.join(tempfile.mkdtemp(), 'collapsible.autstr')
graph.presentation.automatic_presentation_to_file(path)
print(f'{os.path.getsize(path)} bytes on disk')

reloaded = TreeAutomaticPresentation.automatic_presentation_from_file(path)
print('Reach is there:', 'Reach' in reloaded.get_relation_symbols())
print('and still transitive:', reloaded.check(
    'all x.(all y.(all z.((Reach(x,y) & Reach(y,z)) -> Reach(x,z))))'))

22709 bytes on disk
Reach is there: True
and still transitive: True