Overview

AutStr represents infinite mathematical structures as finite automata and decides first-order and monadic second-order questions about them. This chapter is the guided tour: it works through the two things the library represents — single structures and whole classes — the operations that combine them, the rank-width families, implicit evaluation, and finally how the machine works underneath. Every part has a matching executable notebook, linked as we go.

The README <https://github.com/fariedabuzaid/AutStr>_ is the short version of this page; the API reference is generated from the docstrings and linked in the sidebar.

Decision procedure and theorem prover

An AutomaticPresentation bundles automata for a domain and its relations, and decides first-order statements about the presented structure:

from autstr.buildin.presentations import BuechiArithmeticZ

Z = BuechiArithmeticZ()          # (ℤ, +, <, |) as automata

Z.check('all x.(exists y.(A(x,y,x)))')          # ∀x ∃y: x+y=x   — True
Z.check('exists x.(all y.(Lt(x,y)))')           # a least integer? — False

Because the first-order theory of an automatic structure is decidable, check always terminates with a definite answer — a theorem prover for the fragment of mathematics these structures capture. evaluate goes further and returns the automaton of all satisfying assignments, which you can enumerate or reuse. The arithmetic & algebra notebook walks through Presburger and Büchi arithmetic in full.

Computer algebra over infinite domains

Structures need not be finitely generated. The localizations ℤ[1/p] — the rationals whose denominator is a power of p — are infinite, non-finitely-generated groups, yet each has an exact automatic presentation:

from autstr.algebra import z1p_localization

z2 = z1p_localization(2)                       # (ℤ[1/2], +)

x = z2.from_fraction(1, 2)
y = z2.from_fraction(3, 4)
z2.check('A(x,y,z)', x=x, y=y, z=z2.add(x, y))                    # 1/2 + 3/4 = 5/4 — True
z2.check('all x.(exists y.(A(y,y,x)))')                           # 2-divisible?    — True
z2.check('all x.(exists y.(exists w.(A(y,y,w) and A(w,y,x))))')   # 3-divisible?    — False

The first-order divisibility theory even distinguishes the localizations: every element of ℤ[1/2] is 2-divisible but not 3-divisible, and vice versa for ℤ[1/3].

Uniformly automatic classes: one automaton for a whole family

A uniformly automatic class presents not one structure but an entire family, by giving every automaton one extra tape that reads an advice string synchronously with the elements. Fixing the advice instantiates one member; a query is compiled once for the class and then decides any member by running its advice word through the resulting automaton.

autstr.graphs, autstr.algebra, and autstr.groups ship ready-made classes:

# Finite abelian groups — advice is the cyclic decomposition
from autstr.groups import FiniteAbelianGroups
ab = FiniteAbelianGroups()
ab.check('A(x,y,z)', [2, 3], x=(1, 1), y=(1, 2), z=(0, 0))   # (1,1)+(1,2)=(0,0) in Z2⊕Z3

# Non-abelian groups — dihedral, quaternion, semidihedral, modular, ...
from autstr.groups import IndexTwoCyclicGroups
G = IndexTwoCyclicGroups()
G.check('M(x,y,z)', G.dicyclic(4), x=(0, 1), y=(1, 0), z=(1, 1))   # i·j = k in Q₈

# Extraspecial p-groups — nilpotency class 2, order p^(1+2n)
from autstr.groups import ExtraspecialGroups
H = ExtraspecialGroups(3)
H.check('M(x,y,z)', 2, x=(1, (0, 0), (0, 0)), y=(0, (1, 0), (0, 0)),
        z=(1, (1, 0), (0, 0)))

The generic machinery in autstr.uniform turns any advice-indexed family of automata into a class with relativized query evaluation, sentence checking, member instantiation (get_structure), and a first-order define for bootstrapping complex relations from primitives.

The same machinery runs over trees rather than words. Where an automatic presentation encodes elements as strings and a word automaton reads them, a tree-automatic presentation encodes them as finite trees read by a bottom-up tree automaton — exactly the step from Büchi’s theorem to Rabin’s. autstr.tree_uniform hosts the classes whose advice is naturally a tree: a tree decomposition (bounded tree-width) or a k-expression (bounded clique-width), and Skolem arithmetic (ℕ, ·) in autstr.buildin.tree_presentations, where a number is the tree of its prime exponents.

The graphs and groups notebooks build these classes and query them; the arithmetic & algebra notebook covers the Boolean algebras, ℤ[1/p], and the MSO0 finite-powerset structure.

Composing presentations

Automatic structures over a shared signature are closed under disjoint union and direct products; uniformly automatic classes of finite structures are closed under union and under taking all finite direct products of their members. autstr.composition builds the new presentation for you.

from autstr.composition import (
    class_union, direct_product_closure, blocks, tagged_advice,
)
from autstr.groups import ExtraspecialGroups, IndexTwoCyclicGroups
from autstr.uniform import UniformlyAutomaticClass

cyclic, extra = IndexTwoCyclicGroups(), ExtraspecialGroups(3)

def reduct(uniform):                     # the signature the two classes share
    return UniformlyAutomaticClass(
        {'U': uniform.class_automata['U'], 'M': uniform.class_automata['M']})

# Members of either family ...
both = class_union(reduct(cyclic.cls), reduct(extra.cls))
# ... and every finite direct product of them.
groups = direct_product_closure(both)

z4 = tagged_advice(cyclic.cyclic(4), '<l>')          # Z4, abelian
heis = tagged_advice(extra.advice(1), '<r>')         # extraspecial 3^(1+2)

abelian = 'all x.(all y.(all z.(M(x,y,z) -> M(y,x,z))))'
groups.check(abelian, blocks(z4, z4))       # True  — Z4 × Z4
groups.check(abelian, blocks(z4, heis))     # False — one nonabelian factor

operation	on	construction
disjoint_union(A, B)	structures	tag each element with the side it came from
direct_product(A, B, kind='sync')	structures	R_A(a,a') ∧ R_B(b,b')
direct_product(A, B, kind='async')	structures	(R_A(a,a') ∧ b=b') ∨ (R_B(b,b') ∧ a=a')
class_union(C, D)	classes	tag the advice, so the advice languages are disjoint
direct_product_closure(C)	classes	advice α₁|…|αₙ presents A_{α₁} × … × A_{αₙ}

Two of these are worth a word. The direct product encodes a pair over the pair alphabet, where a letter carries one letter of each factor; each factor is then embedded by a variable renaming into its half of the bits, and the two products are Boolean combinations of the embeddings. That is affordable only because the pair alphabet has |Σ_A|·|Σ_B| letters but bits_A + bits_B variables — letters multiply, bits add, which is precisely what the decision diagrams buy.

The product closure concatenates advices with a separator. Since an element of a finite member is never longer than its advice, the blocks line up across every tape, so a relation of the product is the original relation holding in every block — one automaton with one extra state, where an interleaved encoding would need one copy per component. FiniteAbelianGroups is this construction applied to the cyclic groups, and it predates the module. The composition notebook walks through all five operations.

Bounded rank-width: groups and graphs from one linear algebra

The width notions above bound how much combinatorial structure crosses a cut. Rank-width bounds the linear-algebraic rank of what crosses, and one body of machinery — interface bases, streamed basis changes, and a two-sided factorization of the sibling block (autstr.chain_ring) — presents both groups and graphs of bounded rank-width uniformly.

Class-2 groups (autstr.groups.CutRankGroups, autstr.tree_groups.CutRankTreeGroups): a member is a central extension of (ℤ/pᵈ)ⁿ by (ℤ/pᵈ)ᵏ given by commutator labels; the advice spells out, cut by cut, a rank-≤r factorization of the crossing block of the commutation form, and the multiplication automaton carries r linear functionals instead of the digits it has read. With d = 1 this is the field F_p; with d > 1 the center has exponent pᵈ and the width is measured over the chain ring ℤ/pᵈ. Bounded pathwidth, bounded vertex cover, the extraspecial matching and the complete graph are all special layouts; the tree class recovers the word class on spine layouts. autstr.cocycle_groups.CocycleRankWidthGroups generalizes further to distributed centers — central generators scattered through the layout — via a six-register protocol whose advice is microcode.

When a flat advice alphabet would be astronomical (it grows like q^(r²+r+kr)), the classes switch to factored letters: one letter per ring entry of the factorization, streamed through an accumulator — the advice alphabet drops to q+1 letters, and width r ≥ 2 over ℤ/4 goes from unrepresentable to explicitly buildable this way.

Graphs (autstr.tree_graphs.RankWidthClass): the advice is a rank decomposition annotated with the GF(2) factorization of its cuts; adjacency of two vertices is a bilinear form applied to their r-bit interface vectors at the node where their subtrees meet. Rank-width lower-bounds clique-width and stays bounded on dense graphs (cliques have rank-width 1), and the class answers MSO queries like every other graph class:

from autstr.tree_graphs import RankWidthClass, RankWidthGraph

rw = RankWidthClass(1)
two_col = ('exists a.(all x.(all y.((not E(x,y)) or '
           '((Subset(x,a) and (not Subset(y,a))) or '
           '(Subset(y,a) and (not Subset(x,a)))))))')
rw.check(two_col, RankWidthGraph.complete_bipartite(2, 3))   # True  (rank-width 1)
rw.check(two_col, RankWidthGraph.clique(3))                  # False (odd cycle)

The bounded-rank-width groups appear in the groups notebook and the graphs in the graphs notebook.

Implicit evaluation: members whose automata cannot be built

For the heavy ring members the base multiplication automaton is already infeasible to construct — an O(|Σ|⁴) product over a huge advice alphabet. The autstr.implicit layer decides first-order formulas on such members anyway, by never building anything: Boolean connectives keep composite states and step the base automata on the fly, exists is an on-the-fly powerset over the (tiny) element alphabet, not flips acceptance. Because the advice is fixed input, the cost is driven by quantifier alternation, not by alphabet size.

from autstr.groups import CutRankGroups

G = CutRankGroups(2, d=3)         # commutation forms over Z/8 — automata unbuildable
advice = G.advice(3, G.clique_form(3))
x = ((5,), (3, 1, 6))

# model checking, implicitly:
G.check_implicit('exists y.(M(x,y,u))', advice, x=x, u=G.identity(3))   # True

# the satisfying SET, implicitly: exact count without enumeration, lazy iteration
inv = G.evaluate_implicit('M(x,y,u)', advice, x=x, u=G.identity(3))
len(inv)                          # 1 — the unique inverse
next(iter(inv))['y']              # ... and here it is, as a (b, a) tuple

Every uniform class offers check_implicit (model checking) and evaluate_implicit (the satisfying assignments of a formula with open free variables, with the exact solution count computed by dynamic programming — no enumeration — and lazy iteration). ImplicitClass / ImplicitTreeClass package functional atoms and an element alphabet as a first-class fully implicit presentation. The implicit-evaluation notebook also times the implicit path against a compiled one.

How it works

An automatic presentation encodes a countable structure so that its domain is a regular language and each relation is recognized by a synchronous multi-tape automaton reading its arguments letter-by-letter in lockstep. The foundational fact is that this recognizability is closed under first-order definability: Boolean combinations correspond to product automata, and quantifiers to projection followed by determinization. Consequently the first-order theory of any automatic structure is decidable, and every definable relation is again automatic.

A concrete encoding

In the arithmetic package an integer is written sign-magnitude, least-significant bit first: the first symbol is a sign bit (0 for non-negative, 1 for negative), followed by the binary digits of the magnitude from the lowest bit upward, with * padding the shorter arguments of a multi-tape relation so all tapes advance in lockstep. Under this encoding a definable set is a genuinely small automaton — here, for instance, is the recognizer for the integers greater than 1 that are divisible by neither 2 nor 3:

The start state consumes the sign bit; the remaining states scan the magnitude bits from least to most significant. Because “greater than 1” and “not divisible by 2 or 3” are both regular properties of that bit stream, a handful of states suffice — doubled circles are accepting, and * marks the padding that ends the word.

Advice and trees

Allowing the automata to read an additional fixed advice word widens the reach to structures like (ℚ, +) and, using a set of advices, to whole parameterized classes of finite structures. Deciding the first-order theory of a uniformly automatic class reduces to the monadic second-order theory of its advice language (Abu Zaid–Grädel–Reinhardt 2017; Abu Zaid 2018). The same programme runs over finite trees read by bottom-up tree automata, which reaches structures no string encoding captures naturally — (ℕ, ·) with a number written as the tree of its prime exponents, and classes whose advice is inherently a tree.

Why it is fast — and where it is hard

Evaluating a fixed formula on a structure is one linear pass of its advice through the query automaton, so on any class of bounded width every fixed MSO property is decided in linear time — a constructive, streaming form of Courcelle’s theorem. The cost lives entirely in compiling the automaton.

A transition is not a symbol -> target table but a decision diagram over the symbol’s digits, hash-consed and shared across states and automata (autstr.mtbdd) — the representation MONA uses, for the same reason. A transition that ignores a tape never tests that tape’s variables, so cylindrification is a variable renaming rather than a duplication of every row once per letter of every new tape, complementation touches no diagram at all, and the alphabet’s width stops driving the cost. What remains is the subset explosion of determinizing an existential quantifier: element quantifiers are cheap, and set quantifiers (MSO proper) determinize over subsets of the intermediate automaton’s states. Connectedness and bipartiteness compile in seconds; 3-colourability — the minimal NP-hard MSO query — is a genuinely large one-time compile. Once compiled, an automaton can be serialized (diagrams and all) and reused forever.

Around the diagrams the engine is batched NumPy: frontier-batched constructions, hashed partition refinement, and a subset construction that runs in a collectable scratch store. JAX is an optional accelerator used only for bulk word processing.