autstr package

Contents

autstr package#

Subpackages#

Submodules#

autstr.algebra module#

Finite boolean algebras and the localizations Z[1/p] as automatic structures.

Finite boolean algebras (FiniteBooleanAlgebras): the algebra with n atoms is (up to isomorphism) the powerset algebra of [n]. The advice is simply the unary word 1^n; elements are subsets of [n] as bitvectors of length n, and all operations are positionwise. Signature:

Leq(x,y) x <= y Meet(x,y,z) z = x AND y Join(x,y,z) z = x OR y Compl(x,y) y = NOT x Atom(x) x is an atom

The localizations Z[1/p] (Z1pLocalization): a single automatic structure, not a class. An element is written with a sign and a radix-aligned pair of integer and fractional digits, and addition is recognized by a Buechi-style carry automaton.

The finite abelian groups live in autstr.groups beside the other group classes.

class autstr.algebra.Z1pElement(num, exp)[source]#

Bases: object

Canonical element of Z[1/p] represented as num / p**exp.

In canonical form, either num == 0 and exp == 0, or p does not divide num.

Parameters:
num: int#
exp: int#
class autstr.algebra.Z1pLocalization(p)[source]#

Bases: object

Factory-backed arithmetic model for the fixed localization Z[1/p].

This class provides a canonical representation and exact arithmetic for a fixed prime p. It is designed as the API layer that a dedicated automatic presentation can be attached to.

Parameters:

p (int)

normalize(num, exp)[source]#

Return the canonical representative of num / p**exp.

Return type:

Z1pElement

Parameters:
element(num, exp=0)[source]#

Create a canonical element from num / p**exp.

Return type:

Z1pElement

Parameters:
from_fraction(num, den)[source]#

Create an element from a reduced or unreduced fraction num/den.

The denominator must be a positive power of p.

Return type:

Z1pElement

Parameters:
add(x, y)[source]#

Return x + y in canonical form.

Return type:

Z1pElement

Parameters:
neg(x)[source]#

Return -x in canonical form.

Return type:

Z1pElement

Parameters:

x (Z1pElement)

sub(x, y)[source]#

Return x - y in canonical form.

Return type:

Z1pElement

Parameters:
equals(x, y)[source]#

Semantic equality in Z[1/p] (canonical reps compare directly).

Return type:

bool

Parameters:
property sigma: set#
property presentation: AutomaticPresentation#

The automatic presentation of (Z[1/p], +), built on first use. Signature: A(x,y,z) [z = x + y], N0(x) [x >= 0], Z(x) [x = 0], Eq(x,y).

encode(value)[source]#

Encode an element as a word of the presentation.

Return type:

List[str]

evaluate(phi)[source]#

Evaluate a first-order query; see AutomaticPresentation.evaluate. The result’s tapes are the free variables in sorted order.

Return type:

SparseDFA

check(phi, **elements)[source]#

Model check a formula against (Z[1/p], +). Free variables can be assigned elements (Z1pElement, int, or (num, exp) pairs); unassigned free variables are existentially quantified.

Return type:

bool

autstr.algebra.z1p_localization(p)[source]#

Return a fixed-prime localization factory for Z[1/p].

Return type:

Z1pLocalization

Parameters:

p (int)

class autstr.algebra.FiniteBooleanAlgebras(eager_equality=False)[source]#

Bases: SymbolicClassWrapper

The uniformly automatic class of all finite boolean algebras. The member with n atoms has advice 1^n; its elements are the subsets of {0, …, n-1}, encoded as bitvectors of length exactly n.

Parameters:

eager_equality (bool)

GRAPH = None#

meet and join are both there, so the vocabulary stays methods and only equality is bound

Type:

no single binary operation

EQUALITY = 'Leq(x,y) and Leq(y,x)'#

antisymmetry of the order is equality

advice(n)[source]#

Advice string of the boolean algebra with n atoms.

Return type:

List[str]

Parameters:

n (int)

encode(subset, n)[source]#

Encode a subset of {0, …, n-1} as an element word.

Return type:

List[str]

Parameters:

n (int)

evaluate(phi)[source]#
Return type:

Tuple[SparseDFA, List[str]]

check(phi, n, **subsets)[source]#

Model check against the algebra with n atoms; free variables can be assigned subsets of {0, …, n-1}.

Return type:

bool

Parameters:

n (int)

get_structure(n)[source]#
Return type:

AutomaticPresentation

Parameters:

n (int)

autstr.arithmetic module#

Büchi arithmetic, over the naturals and over the integers.

\((\mathbb{N}, +, <, \mid_2)\) and \((\mathbb{Z}, +, <, \mid_2)\) presented in base 2, where x \mid_2 y says that y is a power of two dividing x. Adding that predicate to Presburger arithmetic is what makes the structure Büchi arithmetic: it can talk about the binary expansion of a number, and it remains decidable.

>>> Z = BuechiArithmeticZ().symbolic()
>>> x, y, z = Z.vars("x y z")
>>> ((x + y).eq(z) & z.lt(100)).check()
True

Both presentations are compiled from a handful of small automata the first time they are constructed; the derived relations (order, equality, negation) are first-order definitions over those.

class autstr.arithmetic.BuechiArithmetic[source]#

Bases: CompiledPresentation

Büchi arithmetic over the natural numbers: \((\mathbb{N}, +, <, \mid_2)\) in base 2.

>>> N = BuechiArithmetic()
>>> x, y = N.symbolic().vars("x y")
>>> ((x + y).eq(12) & x.lt(y)).check()
True

B(x, y) holds iff y is a power of two dividing x; it is spelled .divided_by_power rather than bound to |, which on formulas already means union.

Parameters:

automata – dictionary containing the automata that recognize the domain and the relations of the structure. ‘U’ is reserved key for the universe. All other keys are assumed to recognize relations over L(U)^k. They can be addressed by their keys in first-order queries.

PADDING = '*'#

the magnitude, least significant bit first

Type:

base-2 encoding

static encode(n)[source]#

The word encoding a natural number: binary, least significant bit first.

Return type:

List[str]

Parameters:

n (int)

static decode(word)[source]#

The natural number encoded by a word, ignoring padding.

Return type:

int

default_signature()[source]#

+ as addition, with the order, equality and divisibility as methods, and naturals written as Python integers.

class autstr.arithmetic.BuechiArithmeticZ[source]#

Bases: CompiledPresentation

Büchi arithmetic over the integers: \((\mathbb{Z}, +, <, \mid_2)\) in base 2.

>>> Z = BuechiArithmeticZ()
>>> x, y, z = Z.symbolic().vars("x y z")
>>> ((x + y).eq(z) & z.lt(100)).check()
True
>>> (3, 4, 7) in (x + y).eq(z)
True

Integers are written directly wherever a term is expected – x + 5, x.lt(100) – and solutions come back as Python integers. Anything the operators do not cover is reachable through SymbolicContext.rel.

Parameters:

automata – dictionary containing the automata that recognize the domain and the relations of the structure. ‘U’ is reserved key for the universe. All other keys are assumed to recognize relations over L(U)^k. They can be addressed by their keys in first-order queries.

SIGN_POSITIVE = '0'#

a sign symbol, then the magnitude, least significant bit first

Type:

base-2 encoding

SIGN_NEGATIVE = '1'#
PADDING = '*'#
static encode(n)[source]#

The word encoding an integer: sign symbol, then magnitude bits least significant first.

Return type:

List[str]

Parameters:

n (int)

static decode(word)[source]#

The integer encoded by a word, ignoring padding.

Return type:

int

default_signature()[source]#

+ as addition and unary - as negation, with the order, equality and divisibility as methods, and integers written as Python integers.

autstr.chain_ring module#

Linear algebra over the finite chain ring R = Z/p^d.

This is the algebraic foundation for the chain-ring extension of the bounded-rank-width group classes: letting the center of a class-2 group have exponent p^d turns the commutator cocycle into an R-bilinear form over R = Z/p^d. R is a finite chain ring – a local principal ideal ring whose ideals are the chain

R ) pR ) p^2 R ) … ) p^d R = 0,

every element being u * p^s with u a unit and s = v(.) its valuation.

Over a field every module has a basis and every submodule is a direct summand; over R neither holds, which is what separates the routines here from ordinary linear algebra. A minimal generating set of a row module may consist of non-unit rows – the row (2, 0) over Z/4 generates 2R, not a direct summand – so a two-sided factorisation cannot be read off such a set directly. The routines therefore work with a free basis of the saturation of a module (saturate), which keeps the outer interfaces of factor_two_sided free and confines the valuation to its middle factor Q.

At d = 1 the ring is the field F_p, a module is its own saturation, and every routine reduces to the familiar field case, so field and ring callers share one saturate / factor_two_sided interface.

This module is a leaf (nothing in autstr is imported here) so that the group constructions can build on it without an import cycle; the small mod-p echelon helper _rref_mod_p below mirrors groups._rref_mod for locating unit r x r minors.

autstr.chain_ring.modulus(p, d)[source]#

The ring size q = p^d.

Return type:

int

Parameters:
autstr.chain_ring.valuation(x, p, d)[source]#

The p-adic valuation v(x) in {0, .., d} of x in R; v(0) = d.

Return type:

int

Parameters:
autstr.chain_ring.is_unit(x, p, d)[source]#

A unit of R is a valuation-0 element (x not divisible by p).

Return type:

bool

Parameters:
autstr.chain_ring.unit_inverse(u, p, d)[source]#

The inverse of a unit u in R = Z/p^d.

Return type:

int

Parameters:
autstr.chain_ring.to_digits(x, p, d)[source]#

An R-element as its d base-p digits, least significant first.

Return type:

Tuple[int, ...]

Parameters:
autstr.chain_ring.from_digits(digits, p)[source]#

Reassemble an R-element from base-p digits, least significant first.

Return type:

int

Parameters:

p (int)

autstr.chain_ring.inv_mod_pp(B, p, d)[source]#

Inverse of a square matrix that is invertible over R = Z/p^d.

Gaussian elimination with unit pivots; a unit pivot always exists because an R-invertible matrix is invertible mod p. Raises if B is singular over R.

Return type:

ndarray

Parameters:
autstr.chain_ring.smith_normal_form(M, p, d)[source]#

Diagonalise M over R = Z/p^d.

Returns (exps, Winv) where exps are the valuations of the nonzero invariant factors (each < d) in order, and Winv is a unimodular n x n matrix whose first len(exps) rows are a free basis of the saturation of rowsp(M): concretely rowsp(M) == rowsp(diag(p^exps) @ Winv[:t]).

Return type:

Tuple[List[int], ndarray]

Parameters:
autstr.chain_ring.saturate(M, p, d)[source]#

A free basis of the saturation of rowsp(M) over R = Z/p^d.

Returns (basis, exps): basis (rho x n) are the rows of a free direct summand equal to the saturation (pure closure) of the row module, and exps the valuations with rowsp(M) == rowsp(diag(p^exps) @ basis). The free rank rho = len(basis) = dim_{F_p}(M / pM) is the module cut-rank – the number of invariant factors – and equals the ordinary F_p rank when d = 1.

Return type:

Tuple[ndarray, List[int]]

Parameters:
autstr.chain_ring.module_cut_rank(M, p, d)[source]#

The free rank rho of the saturation of rowsp(M) (module cut-rank).

Return type:

int

Parameters:
autstr.chain_ring.right_invertible(V, p, d)[source]#

True iff the rows of V are a free basis of a direct summand of R^n, equivalently V has full row rank mod p, equivalently some r x r minor is a unit. This is the “saturated interface” hypothesis required by factor_two_sided.

Return type:

bool

Parameters:
autstr.chain_ring.right_inverse(V, p, d)[source]#

A right inverse Y (n x r) with V @ Y == I_r over R, for a right-invertible V (r x n). Raises if V is not right-invertible.

Return type:

ndarray

Parameters:
autstr.chain_ring.solve_left(V, B, p, d)[source]#

The general ring solve X with X @ V == B over R = Z/p^d.

V is (r x m) and may be rank-deficient (e.g. a padded basis with zero rows); B is (s x m); the result X is (s x r). Every row of B must lie in rowsp(V) – otherwise there is no solution and a ValueError is raised. Free coordinates of the solution are set to 0.

Solves A @ Y = C with A = V^T (m x r) and C = B^T by Smith-style diagonalisation of A: row operations are mirrored on C and column operations are accumulated in Wc so the solution maps back as Y = Wc @ Z. This is the ring generalisation of the field solver autstr.groups._solve_xa_eq_b (X A = B) used by the linear layout compiler, and drives the saturated streaming update over the chain ring.

Return type:

ndarray

Parameters:
autstr.chain_ring.factor_two_sided(X, Vbar, Wbar, p, d)[source]#

The two-sided factorisation over R = Z/p^d.

Given X (m x m’), a saturated Vbar (r x m’) and a saturated Wbar (r’ x m) such that every row of X lies in rowsp(Vbar) and every column of X lies in colsp(Wbar^T), returns Q (r’ x r) with X == Wbar^T @ Q @ Vbar. The valuations are absorbed into Q, not the (free) interfaces. Raises if the containment hypotheses are violated.

Solved as two ring linear systems (Wbar^T Y = X then Q Vbar = Y), which – unlike a right-inverse – tolerates zero-padded bases whose true rank (the module cut-rank) is below r, and reduces to the field two-step at d = 1. Correctness of the result is confirmed by reconstruction.

Return type:

ndarray

Parameters:

autstr.cocycle_groups module#

Distributed-center class-2 groups: cocycle tensors on site trees.

The tensor cut-rank generalisation of the bounded rank-width group classes. A site tree is a binary tree whose nodes are generators: ‘x’ sites and central ‘z’ sites. The commutator data is a tensor T[j, i, v] over the chain ring R = Z/p^d (i < j x-positions in post-order, v a z-position), presenting the central extension with the bilinear cocycle

(b, a)(b’, a’) = (b + b’ + C(a, a’), a + a’), C(a, a’)_v = sum_{i<j} T[j, i, v] a_j a’_i .

Both coordinate blocks range over R = Z/p^d (an exponent-p^d center forces an exponent-p^d quotient); the default d = 1 is the field case R = F_p. The width is the module cut-rank: the minimal number of generators of each flattening’s module, which chain_ring computes via Smith normal form.

This module provides the reference group law, the six crossing flattenings whose module ranks measure, per subtree cut, the traffic a bottom-up automaton must carry – upward digit functionals (F_y, F_x), upward pair-sums (F_m), inward claims (F_g), and the mixed exports whose products flow back into inside checks (F_py, F_px); reshaping changes rank, so the width is their maximum – and CocycleRankWidthGroups, the uniformly tree-automatic presentation of these groups at any width r and depth d. The classes CutRankTreeGroups (all z-sites on a chain above the root) and TreeExtraspecialGroups (z-sites at the leaves, laminar targets, width 1) are corner cases.

class autstr.cocycle_groups.CocycleSites(p, shape, d=1)[source]#

Bases: object

A site tree over the chain ring R = Z/p^d with its cocycle tensors: reference law and cut-width measures.

Elements are (b, a) with b the center coordinates (one per z-site) and a the quotient coordinates (one per x-site), both over R = Z/p^d and in ascending post-order. With d = 1 (the default) R is the field F_p and this is exactly the original field construction; d > 1 is the exponent-p^d case (center of exponent p^d), where the commutator cocycle is R-bilinear and the tensor coefficients live in R. The quotient shares the exponent p^d: a class-2 group whose commutator subgroup has exponent p^d cannot have an exponent-p quotient.

The width measure cut_width is the module cut-rank: the free rank of the saturated interface (chain_ring.module_cut_rank), which coincides with the ordinary F_p flattening rank when d = 1 but, over the ring, correctly counts valuation-carrying (p-divisible) generators that vanish under a naive mod-p reduction.

Parameters:
check_tensor(T)[source]#
Parameters:

T (Dict[Tuple[int, int, int], int])

multiply(T, g, h)[source]#

The reference group law of G(T) over R = Z/p^d.

Both the center coordinates b and the quotient coordinates a range over R; the cocycle C is R-bilinear, which is what makes the law associative over the ring. (Keeping a over F_p while C is R-valued would break associativity for d > 1: a carry a_j + a’_j >= p drops a term p*T*a’’ that is nonzero mod p^d. In a class-2 group with commutator subgroup of exponent p^d the quotient necessarily has exponent p^d as well, since [x,y]^p = [x^p,y] = 1 would otherwise force G’ to have exponent p.)

Parameters:

T (Dict)

identity()[source]#
cut_profile(T)[source]#

For every proper subtree cut (keyed by its root position), the module cut-ranks of the six crossing flattenings over R = Z/p^d.

Return type:

Dict[int, Dict[str, int]]

Parameters:

T (Dict)

cut_width(T)[source]#

The width of this layout for the tensor: the maximum flattening rank over all subtree cuts.

Return type:

int

Parameters:

T (Dict)

autstr.cocycle_groups.fixed_k_sites(p, layout_shape, form, k, d=1)[source]#

Embed a CutRankTreeGroups instance: an all-x copy of the layout with a chain of k z-sites above the root. Positions of the x-layout are preserved; the z-chain occupies positions n+1 (innermost = center coordinate 0) through n+k. With d > 1 the sites and the form labels live over the chain ring R = Z/p^d.

Return type:

Tuple[CocycleSites, Dict]

Parameters:
autstr.cocycle_groups.laminar_sites(p, shape, d=1)[source]#

Embed a TreeExtraspecialGroups instance: every inner node w of the shape becomes a chain x-site (for x_w) over x-site (for y_w), every leaf becomes a z-site, and [x_w, y_w] hits every leaf below w. Returns the sites, the tensor, and the address map {shape address: site positions}. With d > 1 the sites live over the chain ring R = Z/p^d (the tensor keeps unit coefficients; the center gains exponent p^d).

Return type:

Tuple[CocycleSites, Dict, Dict]

Parameters:
autstr.cocycle_groups.point_target_sites(p, shape, d=1)[source]#

A width-1 family covered by neither corner class: as laminar_sites, but every commutator [x_w, y_w] hits only the leftmost leaf below w (point targets: the center grows with the tree, the law is not laminar). With d > 1 the sites live over the chain ring R = Z/p^d.

Return type:

Tuple[CocycleSites, Dict]

Parameters:
autstr.cocycle_groups.scattered_sites(p, m, d=1)[source]#

The lower-bound family: m private z-sites on a chain at the bottom, m commuting x-pairs above, pair t targeting exactly z_t. The cut at the z-chain has an identity claim flattening: width m (the module cut-rank over R = Z/p^d equally, for d > 1).

Return type:

Tuple[CocycleSites, Dict]

Parameters:
class autstr.cocycle_groups.CocycleRankWidthGroups(p, r=1, d=1)[source]#

Bases: SymbolicClassWrapper

The uniformly tree-automatic class of distributed-center class-2 groups of tensor cut-rank <= r over R = Z/p^d. The bottom-up automaton’s state is six R^r registers (plus three scratch slots):

wy, wx : upward digit functionals   (column modules of F_y, F_x)
qy, hx : mixed exports for inside targets       (F_py, F_px)
m      : representative of the exports element of E_S = rowsp(F_m)
g      : representative of the residuals element of the claim
         module Gamma_S = colsp(F_g); a residual leaving the
         module is a rejection

The advice is a table-driven instruction stream: each site expands into its marker letter followed by a chain of operations, each either linear – a streamed matrix or injection column, the folds and read-off coefficients of the restriction calculus – or a streamed table keyed on register values and the residual digit: the sibling pairing tables and the claim extensions and joins. Over the ring these functions are well-defined and bilinear on the interface images but need not be matrices. Merges are one-step: the binary marker consumes both children’s raw registers and the stretch above it folds directly to the parent cut; no joint-interval interfaces exist.

advice(sites, T) compiles a tensor of module cut-width <= r; every linear coefficient and every table entry is derived through chain_ring solves, each guarded by an assertion that the required membership or factorisation actually holds, so a compilation that succeeds has verified its own structural hypotheses. Interfaces are minimal generating sets of the flattening modules (Smith normal form with the p-power factors kept); at d = 1 they are ordinary bases and every table is semantically a matrix, though the letter format is uniform in d.

The explicit presentation automata are beyond the enumeration builder by construction (the instruction phase is part of the state); simulate runs the exact transition function over the convolved trees, and check_implicit / evaluate_implicit decide first-order properties through the functional atoms.

Parameters:
MARKERS = {'K': ('z', 0), 'L': ('x', 0), 'M': ('x', 2), 'U': ('x', 1), 'V': ('z', 1), 'W': ('z', 2)}#

(site kind, arity)

Type:

marker letters

advice(sites, T)[source]#

Compile a tensor of module cut-width <= r into the instruction stream; ValueError beyond the width, AssertionError if any structural check fails.

Return type:

Tree

Parameters:
encode(element, sites, advice)[source]#

Element tree of the advice’s shape: each site’s digit repeats along its instruction stretch.

Return type:

Tree

Parameters:
decode(tree, advice)[source]#

Inverse of encode: the digit at each marker; z-sites to b and x-sites to a, in ascending post-order.

Parameters:
multiply(sites, T, g, h)[source]#
Parameters:
simulate(advice, tx, ty, tz)[source]#

Run the transition function over the convolved trees, with an explicit stack (instruction stretches can be long).

Return type:

bool

Parameters:
property cls#
evaluate(phi)[source]#
check(phi, sites, advice, **elements)[source]#
Return type:

bool

Parameters:
get_structure(advice)[source]#
Parameters:

advice (Tree)

property implicit_cls#
check_implicit(phi, sites, advice, **elements)[source]#

First-order model checking over the functional atoms.

Return type:

bool

Parameters:
evaluate_implicit(phi, sites, advice, **elements)[source]#

The satisfying set of phi, computed implicitly; yields assignments {var: (b, a)}.

Parameters:

autstr.collapsible module#

Level 2 collapsible pushdown systems and their configuration graphs.

A collapsible pushdown stack of level 2 is a stack of stacks in which every letter additionally carries a collapse link to some part of the stack lying below it — a record of what the stack looked like when the letter was pushed. The collapse operation throws the stack back to that recorded point in one step, which is what makes these systems strictly more expressive than ordinary higher-order pushdown systems: they are the operational counterpart of higher-order recursion schemes.

Why the tree engine. Kartzow (2010) proved that level 2 collapsible pushdown graphs are tree-automatic, and that is the only automatic route to them: their MSO theory is undecidable, so the infinite-tree machinery that serves ordinary pushdown graphs (Muller-Schupp, Caucal) has nothing to offer here, while a finite-tree presentation gives the whole first-order theory. The tradeoff is exactly the opposite of the one for ordinary pushdown graphs, whose point is decidable MSO. It is also tight: Broadbent showed that at level 3 even first-order model checking becomes undecidable.

The encoding. A stack w_1 : w_2 : … : w_n is a list of words, and consecutive words share long prefixes, because that is the only way clone_2 can make new ones. So the words are laid into one tree: a block is a maximal run of consecutive words sharing their first two letters, blocks of a blockline hang off each other as right children (1-successors), and the blockline a block induces — the same words with their shared first letter removed — hangs below it as a left child (0-successor). Every initial left-closed path of the tree is then one word of the stack. Collapse links are not stored: a level 1 link always points to the preceding letter, and a level 2 link on a node d points to the substack of width |{d' a right child : d' ≤ d}|, which the position of d already determines. That is what makes the encoding a bijection between configurations and a regular set of trees, and so the whole structure tree-automatic without a quotient.

>>> system = Level2CPS(                       # Hague et al.'s example
...     transitions=[('0', None, 'Cl', '1', 'clone'),
...                  ('1', None, 'A', '0', 'push a 2'),
...                  ('1', None, "A'", '2', 'push a 2'),
...                  ('2', 'a', 'P', '2', 'pop 1'),
...                  ('2', 'a', 'Co', '0', 'collapse')])
>>> graph = system.configuration_graph()
>>> graph.is_deterministic()               # two rules fire in state 1
False
>>> graph.check('exists x.(not exists y.(E(x,y)))')    # some are stuck
True

Reachability, and the contrast with Turing machines. For a level 2 collapsible pushdown graph the reachability relation is itself tree-automatic (Kartzow, Prop. 5.1), and it is built here — Reach is a relation of the graph like any other, so a first-order formula may ask about runs of any length. That is the very question autstr.turing cannot answer, since for a configuration graph of a Turing machine reachability is the halting problem. It is also the reason these graphs belong on the tree engine at all:

>>> 'Reach' in graph.get_relation_symbols()
True

reach_along gives the sharper version: reachability along runs whose labels a finite automaton accepts, which is Kartzow’s Reach_L and covers the ε-contraction of the graph as the case of any number of silent labels followed by one other. The construction is in autstr.collapsible_reach; it is exponential in the number of control states, so Reach is declared but not built until a query asks for it.

Configurations are all of them, not only those reachable from an initial one — the same reading Kartzow’s result takes.

References:

  • A. Kartzow, Collapsible Pushdown Graphs of Level 2 are Tree-Automatic, Logical Methods in Computer Science 9(1), 2013 (STACS 2010).

  • M. Hague, A. S. Murawski, C.-H. L. Ong, O. Serre, Collapsible Pushdown Automata and Recursion Schemes, LICS 2008.

  • C. Broadbent, The Limits of Decidability for First Order Logic on CPDA Graphs, STACS 2012.

autstr.collapsible.PAD = '*'#

the padding symbol of the tree convolutions; it must sort before every other letter of the alphabet

autstr.collapsible.SEP = '.'#

the label of a separator node — a node that splits one block from the next, written ε in the literature because it repeats no letter

autstr.collapsible.BOTTOM = '⊥'#

the default bottom-of-stack symbol

class autstr.collapsible.Letter(symbol, level=1, link=None)[source]#

Bases: object

A stack letter: a symbol plus its collapse link.

Parameters:

  • symbol (str) – the stack symbol.

  • level (int) – the level of the collapse link, 1 or 2.

  • link (Optional[int]) – at level 2, the width of the substack the link points to; a level 1 link always points to the preceding letter, so it carries no value of its own.

symbol: str#
level: int = 1#
label()[source]#

The tree label of this letter — the symbol and the link level, the only parts the encoding stores.

Return type:

str

class autstr.collapsible.Stack(words)[source]#

Bases: object

A level 2 collapsible stack: a nonempty list of nonempty words.

The operations return None where they are undefined — popping the last letter of a word, popping the last word, or collapsing on a link that points nowhere — rather than raising, so that a configuration with no successor is an ordinary answer rather than an error.

Parameters:

words (Tuple[Tuple[Letter, ...], ...])

words: Tuple[Tuple[Letter, ...], ...]#
property width: int#

The number of words — the n of w_1 : … : w_n.

top()[source]#

The topmost letter: the last letter of the last word.

Return type:

Letter

clone()[source]#

clone_2: duplicate the topmost word, links and all.

Return type:

Stack

push(symbol, level=1)[source]#

push_{symbol,level}: write a letter onto the topmost word. A level 2 link points at the stack below the topmost word, whose width is recorded; a level 1 link needs no record.

Return type:

Stack

Parameters:
pop1()[source]#

pop_1: drop the topmost letter, if the topmost word has one to spare.

Return type:

Optional[Stack]

pop2()[source]#

pop_2: drop the topmost word, if it is not the only one.

Return type:

Optional[Stack]

collapse()[source]#

collapse: jump to the stack the topmost letter’s link points to.

At level 1 that is the preceding letter, so the operation coincides with pop1; at level 2 it is the substack of the recorded width, so it is a whole run of pop2 at once.

Return type:

Optional[Stack]

apply(operation)[source]#

The stack this operation produces, or None where it is undefined.

Return type:

Optional[Stack]

Parameters:

operation (Operation)

class autstr.collapsible.Configuration(state, stack)[source]#

Bases: object

A configuration: a control state and a stack.

Parameters:
state: str#
stack: Stack#
class autstr.collapsible.Operation(kind, symbol=None, level=None)[source]#

Bases: object

A stack operation, as it appears in a transition rule.

Parameters:

  • kind (str) – 'clone', 'push', 'pop' or 'collapse'.

  • symbol (Optional[str]) – the symbol a push writes.

  • level (Optional[int]) – the level of a push’s link, or of a pop.

kind: str#
symbol: str | None = None#
level: int | None = None#
static parse(spec)[source]#

An operation from its spelling: 'clone', 'push a', 'push a 2', 'pop 1', 'pop 2' or 'collapse'.

Return type:

Operation

autstr.collapsible.initial_stack(bottom='⊥')[source]#

The initial stack ⊥_2: one word holding the bottom symbol.

Return type:

Stack

Parameters:

bottom (str)

autstr.collapsible.encode_stack(stack)[source]#

The tree of a stack: blocks of a blockline hang off each other to the right, the blockline a block induces hangs below it to the left.

Return type:

Tree

Parameters:

stack (Stack)

autstr.collapsible.decode_stack(tree)[source]#

The stack a tree encodes.

Every word ends where the descent to the left ends, and every node that is a right child starts the next word. The collapse links are read off the positions: a level 2 link points to the substack whose width is the number of right children up to and including this node in the traversal.

Return type:

Stack

Parameters:

tree (Tree)

autstr.collapsible.encode_configuration(configuration)[source]#

The tree of a configuration: the state labels the root and the stack hangs below it to the left.

Return type:

Tree

Parameters:

configuration (Configuration)

autstr.collapsible.decode_configuration(tree)[source]#

The configuration a tree encodes.

Return type:

Configuration

Parameters:

tree (Tree)

class autstr.collapsible.Rule(state, symbol, label, target, operation)[source]#

Bases: object

One transition: in state state, with symbol on top of the stack, read label, go to target and apply operation. A symbol of None matches any topmost symbol.

Parameters:
state: str#
symbol: str | None#
label: str#
target: str#
operation: Operation#
applies_to(configuration)[source]#

Whether this rule’s state and stack guard match.

Return type:

bool

Parameters:

configuration (Configuration)

class autstr.collapsible.Level2CPS(transitions, bottom='⊥', initial_state=None, states=(), symbols=())[source]#

Bases: object

A collapsible pushdown system of level 2.

Parameters:

  • transitions (Iterable[Sequence]) – the rules, as (state, symbol, label, target, operation) tuples. The symbol may be None or '-' to match any topmost symbol; the operation is a Operation or its spelling, one of 'clone', 'push <symbol> [1|2]', 'pop 1', 'pop 2', 'collapse'.

  • bottom (str) – the bottom-of-stack symbol, which no push may write.

  • initial_state (Optional[str]) – the control state of the initial configuration; the first rule’s state when omitted.

  • states (Iterable[str]) – further control states, if some appear in no rule.

  • symbols (Iterable[str]) – further stack symbols, likewise.

RESERVED = ':<>'#

characters the encoding uses to build tree labels

initial()[source]#

The initial configuration: the initial state over ⊥_2.

Return type:

Configuration

step(configuration)[source]#

Every successor of a configuration, as (label, configuration) pairs — the Python oracle the automata are checked against, and the obvious way to run the system. A collapsible pushdown system is nondeterministic, so there may be several, or none.

Return type:

List[Tuple[str, Configuration]]

Parameters:

configuration (Configuration)

reachable(bound=6)[source]#

The configurations reachable from the initial one in at most bound steps.

The unbounded reachability relation is tree-automatic too (Kartzow, Prop. 5.1) but is not built here, so this is a search rather than a decision procedure — useful for seeing a system run, and for checking the graph against small examples.

Return type:

List[Configuration]

Parameters:

bound (int)

configuration_graph(**kwargs)[source]#

The graph of all configurations under one step of the system.

Return type:

Level2CPG

static encode(configuration)[source]#

The tree encoding a configuration.

Return type:

Tree

Parameters:

configuration (Configuration)

static decode(tree)[source]#

The configuration a tree encodes.

Return type:

Configuration

Parameters:

tree (Tree)

class autstr.collapsible.Level2CPG(system, max_states=None)[source]#

Bases: object

The configuration graph of a Level2CPS, as a tree-automatic structure.

Vertices are all configurations — every control state over every level 2 collapsible stack — and there is a γ-labelled edge wherever one rule of the system takes one configuration to another. The domain is regular because the encoding is a bijection onto a regular set of trees; the edges are regular because every stack operation is a bounded rewrite at the end of the tree’s last path.

The presentation carries E (a step under any label), Edge… (one per label of the system), Eq, and — built on first use — the stack operations Clone, Push…, Pop1, Pop2, Collapse as relations of their own, the control-state predicates State…, and the predicates Top…, Level1, Level2 for the topmost letter.

Parameters:

  • system (Level2CPS) – the Level2CPS.

  • max_states (Optional[int]) – optional cap on the subset determinizations inside projection.

FIXED = ('U', 'Eq', 'E', 'Clone', 'Pop1', 'Pop2', 'Collapse', 'Level1', 'Level2')#

the relation names that do not depend on the system

reach_along(name, labels)[source]#

Install Reach_L: reachability along runs whose labels the given autstr.collapsible_reach.LabelAutomaton accepts.

Plain reachability is the case where every label word is allowed, and an ε-contraction is the case of any number of silent labels followed by one other — so this one relation covers both.

Parameters:

  • name (str) – the relation symbol to install it under.

  • labels – which sequences of labels a run may read.

Return type:

None

symbolic(signature=None)[source]#

A symbolic interface to the graph; write one step as x.adj(y) and configurations as Configuration values.

check(phi)[source]#
Return type:

bool

evaluate(phi)[source]#
get_relation_symbols()[source]#
is_deterministic()[source]#

Whether every configuration has at most one successor — a first-order property of the one-step relation, so it costs nothing beyond E.

Return type:

bool

autstr.collapsible_reach module#

Reachability in a level 2 collapsible pushdown graph.

Whether one configuration can reach another is decidable here, and that is the point of the whole encoding: over a Turing machine’s configuration graph the same question is halting. Kartzow proves the relation tree-automatic; this builds it.

Reach = A ; B ; C ; D. Every run splits into four stretches — words come off the stack, then letters, then letters go back on, then words — and all four relations are reflexive, so the composition excludes nothing. Reachability is therefore a first-order formula over the four rather than an automaton of its own, and Relations.reach writes it out. regular_reach gives Kartzow’s sharper Reach_L, along runs whose labels a finite automaton accepts, by building that automaton into a product system; an ε-contraction is the case of any number of silent labels followed by one other.

Each of the four is checked on four tapes: the two configurations, the summary annotation of one of them, and a guessed control state per node. The annotation is what lets a bottom-up automaton consult a computation that runs top-down — a node carries the summary of the word read from the root down to it, which is a local check — and both scaffolding tapes are quantified away afterwards.

The summaries are what all of that rests on. Four kinds of run matter (Kartzow 2013, §4), all concerned with what a stack can do before it drops below where it started:

  • a return takes a stack to the one below it,

  • a loop takes a stack back to itself, and splits into a high loop, which never drops a letter, and a low loop, which drops exactly one and writes it back,

  • a 1-loop takes a stack to one with the same topmost word and more words underneath.

The pivotal fact is that which of these exist depends only on the stack’s topmost word — not on anything below it. So each word w has a summary: four relations on the control states, saying between which states a return, a high loop, a low loop and a 1-loop of w exist. Kartzow’s Prop. 4.20 then says the summary of wσ is determined by the summary of w together with σ, which makes the summaries the states of a finite automaton reading a word bottom to top.

How this computes them. The paper’s own effectiveness argument routes through µ-calculus model checking on collapsible pushdown graphs, which is a decision procedure of its own. It is not needed: the decomposition lemmas the paper proves are already a closed system of rules, each saying how one kind of run is built from shorter ones:

return      = high loop, then a pop, or a drop into the word below
              followed by a return of it, or a pushed level 2 letter
              collapsed after a 1-loop
high loop   = (push, loop of the longer word, pop) and (clone, return),
              closed under composition
low loop    = drop a level 1 letter, loop of the word below, write it back
1-loop      = loop, clone, loop, clone, …
loop        = high loop, or high loop then low loop then high loop

The least fixpoint of those rules is the summary. The rules refer to the summaries of longer words, which is why this is one simultaneous fixpoint over the whole table rather than an induction on word length.

Why all four together. A level 2 letter pushed at width d carries a link to width d−1, and a clone copies the letter with its link, so collapsing it from the copy drops two words at once — overshooting the copy’s own return. Such a run is no composition of two returns, and what covers it is exactly a 1-loop: push the letter, let the stack grow underneath while the topmost word comes back, then collapse. Returns therefore need 1-loops, which need loops, which need returns.

Reference: A. Kartzow, Collapsible Pushdown Graphs of Level 2 are Tree-Automatic, LMCS 9(1), 2013, §4.

autstr.collapsible_reach.Relation#

a relation on control states

alias of FrozenSet[Tuple[str, str]]

autstr.collapsible_reach.Letter#

a symbol and a link level. The link value is always zero here — a summary is asked of a word on its own, where a link into the stack below means nothing.

Type:

a letter of a word, as the summaries see it

alias of Tuple[str, int]

autstr.collapsible_reach.compose(left, right)[source]#

The relational composition left ; right.

Return type:

FrozenSet[Tuple[str, str]]

Parameters:
autstr.collapsible_reach.closure(relation, states)[source]#

The reflexive transitive closure.

Return type:

FrozenSet[Tuple[str, str]]

Parameters:

relation (FrozenSet[Tuple[str, str]])

class autstr.collapsible_reach.Summary(symbol=None, level=0, ret=frozenset({}), hloop=frozenset({}), lloop=frozenset({}), oneloop=frozenset({}))[source]#

Bases: object

What the runs of one word are, between which control states.

Parameters:

  • symbol (Optional[str]) – the word’s topmost symbol.

  • level (int) – the link level of its topmost letter.

  • ret (FrozenSet[Tuple[str, str]]) – pairs (q, q’) with a return — a run to the stack below.

  • hloop (FrozenSet[Tuple[str, str]]) – pairs with a high loop — back to the same stack, never dropping the topmost letter.

  • lloop (FrozenSet[Tuple[str, str]]) – pairs with a low loop — dropping the topmost letter and writing it back.

  • oneloop (FrozenSet[Tuple[str, str]]) – pairs with a 1-loop — back to the same topmost word, with more words underneath.

symbol: str | None = None#
level: int = 0#
ret: FrozenSet[Tuple[str, str]] = frozenset({})#
hloop: FrozenSet[Tuple[str, str]] = frozenset({})#
lloop: FrozenSet[Tuple[str, str]] = frozenset({})#
oneloop: FrozenSet[Tuple[str, str]] = frozenset({})#
property loop: FrozenSet[Tuple[str, str]]#

a high loop, or a high loop, a low loop and a high loop in sequence (Kartzow, Cor. 4.17).

Type:

Every loop

relations()[source]#
autstr.collapsible_reach.EMPTY = Summary(symbol=None, level=0, ret=frozenset(), hloop=frozenset(), lloop=frozenset(), oneloop=frozenset())#

nothing below the bottom letter, so no run of any kind, and no letter to drop onto

Type:

the summary of the empty word

class autstr.collapsible_reach.Summaries(system, depth=3, limit=7)[source]#

Bases: object

The summaries of the words a system can build.

The rules for a word’s runs refer to the runs of longer words — pushing a letter and dropping it again is how a run stays where it is — so this is one simultaneous least fixpoint rather than an induction on length. The fixpoint is taken over the words themselves, up to a length bound, with everything longer treated as having no runs at all.

That makes the result an under-approximation: every run it reports is real, and one it misses would need a word longer than the bound to be written down. The bound is raised until the summaries stop changing, which is where the fixpoint has been reached — for the automaton of Kartzow’s Prop. 4.20 the summaries of long words repeat, so this terminates on the systems it is meant for, and converged says whether it did.

Parameters:

  • system (Level2CPS) – the collapsible pushdown system.

  • depth (int) – how many letters above the bottom to unroll before raising the bound; raised up to limit while the summaries keep growing.

  • limit (int) – the longest word the fixpoint will consider.

values: Dict[tuple, Summary]#
stable: set#

the words whose summary stopped growing when the bound last rose — a value can only grow, so agreeing twice means it is the truth

moves(symbol, key)[source]#
Return type:

FrozenSet[Tuple[str, str]]

Parameters:

symbol (str)

drops(letter)[source]#

The moves that remove the topmost letter: a pop of level 1, and a collapse when the link is of level 1 — a level 1 link always points at the preceding letter, so collapsing on one is popping it.

Return type:

FrozenSet[Tuple[str, str]]

Parameters:

letter (Tuple[str, int])

transitions()[source]#

The merged automaton, as _merge builds it, once it is closed.

Return type:

Tuple[Summary, Dict[Tuple[Summary, Tuple[str, int]], Summary]]

of_word(word)[source]#

The summary of a word, given as its letters from the bottom up.

Return type:

Summary

class autstr.collapsible_reach.Annotation(encoding, summaries)[source]#

Bases: object

The summary of the word from the root of an encoding tree to each node, written on a tape of its own.

Kartzow’s automata ask, at a node d, which returns and loops the stack that node stands for has — and that stack’s topmost word is the word read from the root down to d. A bottom-up automaton cannot read downwards, so the answer is carried on a second tape, where the check becomes local: a node’s annotation is its parent’s extended by the node’s own letter, and a separator carries its parent’s along unchanged.

The tape is scaffolding — the construction pushes it through a projection and then drops it, which is what autstr.utils.tree_automata_tools.restrict_alphabet is for.

Parameters:

  • encoding – the tree alphabet of the system, from autstr.collapsible.

  • summaries (Summaries) – the summaries of that system’s words.

START = '~start'#

the annotation of the root, where no letter has been read yet

table#

annotation letter -> letter -> annotation letter

extend(annotation, label)[source]#

The annotation a node carries, given its parent’s and its own label — or None where no encoding tree has that shape.

Return type:

Optional[str]

Parameters:

  • annotation (str)

  • label (str)

of_tree(tree, annotation=None)[source]#

The annotation of a configuration tree, as a tree of its own — the oracle the automaton is checked against.

Return type:

Tree

Parameters:

annotation (str | None)

automaton(alphabet=None)[source]#

Two tapes: a configuration tree, and its annotation.

Parameters:

alphabet – the alphabet to build over, when a construction has letters of its own beside these — an automaton can only be combined with others that read the same one.

Return type:

SparseTreeAutomaton

A node’s state is what a parent has to know about it — the annotation it carries and the label it carries — since the parent is where the two can be compared.

class autstr.collapsible_reach.Relations(system, summaries=None, extra_states=())[source]#

Bases: object

The relations whose composition is reachability.

Kartzow’s Remark 4.4 splits every run into four stretches: A drops whole words, B drops letters from the topmost word, C pushes letters back on, and D grows the stack again. All four are reflexive, so reachability is their composition and needs no automaton of its own —

Reach(x,y) ≡ ∃d ∃e ∃f. A(x,d) ∧ B(d,e) ∧ C(e,f) ∧ D(f,y)

which is a formula the engine evaluates once the four are installed.

Each is checked on four tapes — the two configurations, the summary annotation of the first, and a guessed control state per node — and the last two are projected away afterwards.

Parameters:

  • system (Level2CPS) – the collapsible pushdown system.

  • summaries (Optional[Summaries]) – its summaries; computed if not given.

  • extra_states (Sequence[str])

NONE = '@-'#

a node no run visits, and so carries no guessed states

BURIED = '@buried'#

a node one collapse takes away along with everything around it — told apart from an ordinary dropped letter on the tape, since the two inert regions would otherwise want the same entry

summary_of(annotation)[source]#

The summary an annotation letter stands for.

Return type:

Optional[Summary]

Parameters:

annotation (str)

drop_moves(symbol, level)[source]#

The transitions that take the topmost letter off: a pop of level 1, and a collapse when the link is of level 1.

Return type:

FrozenSet[Tuple[str, str]]

Parameters:
guessed(guess)[source]#

The pair of states a guess letter carries, or None.

Return type:

Optional[Tuple[str, str]]

Parameters:

guess (str)

walked(guess)[source]#

The two states and the kind of walk a D guess letter carries.

Return type:

Optional[Tuple[str, str, str]]

Parameters:

guess (str)

dropping(annotation, label, guess)[source]#

Whether a letter may be dropped as the guess says: a high loop of the word ending at it, then one transition that takes it off.

The word is the one read from the root down to this node, which is what the annotation names — so the check needs nothing but this node’s own four tapes.

Return type:

bool

Parameters:
b()[source]#

B: the topmost word loses letters, and nothing goes below what is left.

The two trees agree except along a tail of the first one’s last path, which is deleted; the second may gain a single separator where its own last word now ends. Climbing that tail is the run: at each letter a high loop and one drop, the state after one drop being the state before the next.

Return type:

SparseTreeAutomaton

without_scaffolding(checker, annotated=0)[source]#

A four-tape checker as a relation on two configurations.

The annotation is required to be the real one — that is what the annotation automaton says — and then both it and the guess are quantified away, leaving the alphabet to be narrowed back to the one the configurations are written in.

Parameters:

  • annotated (int) – which configuration the annotation belongs to. The words a run passes through are those of the longer of the two, which is the first tape where letters come off and the second where they go on.

  • checker (SparseTreeAutomaton)

Return type:

SparseTreeAutomaton

looping(annotation, guess)[source]#

Whether the guess is a high loop of the word this node names.

Return type:

bool

Parameters:

  • annotation (str)

  • guess (str)

push_moves(annotation, label)[source]#

The transitions that write label on a stack whose topmost word is the one annotation names.

A pop is guarded by the letter it takes off, so a node can check it alone; a push is guarded by the letter already on top, which is the one above the letter written — and which is not this node’s label when the letter goes below a separator. The summary knows it either way: it carries the topmost symbol of the word it names.

Return type:

FrozenSet[Tuple[str, str]]

Parameters:

  • annotation (str)

  • label (str)

c()[source]#

C: the topmost word gains letters, and the run never dips below where it started.

B read backwards, and the same tree shape with the two configurations exchanged: the second one’s last path is longer by a tail, and the first carries the one separator the second loses. The run is a high loop and a push at each letter gained — the loop belonging to the node that names its word, the push to the node above, which is where the letter it writes is still on top.

Return type:

SparseTreeAutomaton

a()[source]#

A: the stack loses whole words.

Kartzow’s Lemma 4.11 decomposes such a run into pieces that are returns (F1), a 1-loop then a level 2 collapse (F2), or a 1-loop then a pop that some later F2 closes off (F3). The words dropped are the encoding’s separators, and the run drops them from the last backwards — so within a subtree the chain runs through the right child’s separators, then the left child’s, then the node itself, which is reverse traversal order.

A collapse spans several words at once, which sounds like a link reaching across the tree. It is not: a level 2 link records the number of separators up to its letter, and the stack it points at is the tree’s prefix at that separator — which is exactly where the region being deleted begins. So an F3-F2 group is a chain climbing the top path inside that region, a 1-loop and a pop at each letter and a 1-loop and the collapse at the last, closed off by the region’s own root. Every check stays local, and the group then contributes a pair of states to the outer chain just as a return does.

Return type:

SparseTreeAutomaton

Whether the system can collapse on a level 2 link at all — the case that makes a need its F2 and F3 pieces rather than returns alone.

Return type:

bool

d()[source]#

D: the stack grows, and the run never dips below where it started.

Kartzow’s Cor. 4.10 walks the milestones of the stack being built, consecutive ones joined by a single operation and a loop, and the encoding lays them out one per node in traversal order. Measuring that walk gives three moves and no others:

to a left child push that letter to a right child clone back up a level pop, one per level, each node popping its own

with the clone that starts an ascent happening at the deepest node reached, not where the two words part. A separator carries no letter, so it pops nothing on the way out.

That makes one invariant per subtree: the run arrives at its root’s milestone in one state and leaves the subtree in another, having cloned at its deepest node and popped back up to the word its parent names. The run ends inside exactly one subtree, and there it leaves by simply stopping — which is the difference between the two kinds of walk state below.

Return type:

SparseTreeAutomaton

reach()[source]#

Reachability: a run of any length, between any two configurations.

Kartzow’s Remark 4.4 splits every run into four stretches — words come off, then letters, then letters go back on, then words — and each is reflexive, so no run is excluded by having to pass through all four. The relation is therefore the composition, which is a first-order formula over the four and needs no automaton of its own:

Reach(x,y) ≡ ∃u ∃v ∃w. A(x,u) ∧ B(u,v) ∧ C(v,w) ∧ D(w,y)

The quantifiers range over configurations, so the domain of the scratch structure is the encoding trees themselves.

Return type:

SparseTreeAutomaton

class autstr.collapsible_reach.LabelAutomaton(transitions, initial, final)[source]#

Bases: object

A finite automaton over a system’s edge labels.

It says which sequences of labels a run may read, which is what turns plain reachability into Kartzow’s regular reachability Reach_L.

Parameters:

  • transitions (Tuple[Tuple[str, str, str], ...]) – (state, label, state) triples; several may share a state and label, so the automaton need not be deterministic.

  • initial (str) – the state a run starts in.

  • final (FrozenSet[str]) – the states a run may end in.

transitions: Tuple[Tuple[str, str, str], ...]#
initial: str#
final: FrozenSet[str]#
static of_word(labels)[source]#

Runs reading exactly this sequence of labels.

Return type:

LabelAutomaton

static anything(labels)[source]#

Runs reading any sequence at all — plain reachability.

Return type:

LabelAutomaton

static contracting(labels, silent)[source]#

Runs reading any number of silent labels and then one other — the step relation of an ε-contraction.

Return type:

LabelAutomaton

property states#
autstr.collapsible_reach.product(system, labels)[source]#

The system whose runs are those of system whose labels labels accepts, its control state carrying both.

Kartzow builds the label automaton into the reachability automaton directly; as a product system it is the same thing said once, and it costs nothing beyond the states multiplying.

Return type:

Level2CPS

Parameters:
autstr.collapsible_reach.relabel_root(encoding, source, target)[source]#

Two configurations with the same stack, whose control states are the two given ones — the trees agree everywhere but at the root.

Return type:

SparseTreeAutomaton

Parameters:
autstr.collapsible_reach.regular_reach(system, labels, summaries=None)[source]#

Reach_L: reachability along runs whose labels labels accepts.

The label automaton goes into a product system, whose reachability is the ordinary one; what remains is to say that the two configurations are the plain ones underneath — same stack, control state tagged with the label automaton’s initial state at one end and an accepting one at the other:

Reach_L(x,y) ≡ ∃u ∃v. Tag_{p₀}(x,u) ∧ Reach(u,v) ∧ ⋁_f Tag_f(y,v)

Both kinds of configuration live in the same structure for the length of that formula, which is why the encoding carries root letters for both, and the alphabet is narrowed again once the tags are quantified away.

Return type:

SparseTreeAutomaton

Parameters:

autstr.composition module#

Composing automatic presentations.

Automatic structures over a common signature are closed under disjoint union and under direct products, and uniformly automatic classes under union and under the direct-product closure. Every one of these constructions is a statement about letters: re-express the factors over a common alphabet, then combine them with the Boolean operations the engine already has.

The letter work is done by autstr.sparse_automata.recode, which rewrites a transition diagram for a new alphabet in one pass over its nodes. Widening an alphabet therefore costs nothing that scales with the alphabet – and that is what makes products affordable, because the pair alphabet of a direct product has |A| * |B| letters but only bits_A + bits_B variables. Letters multiply; bits add.

autstr.composition.prefix(dfa, letters)[source]#

Accept exactly letters . w for the words w the automaton accepts.

letters gives one letter per tape, so a k-ary relation is prefixed by one symbol of its convolution. A fresh start state reads that symbol and hands over; every other first symbol is rejected. This is how a disjoint union tags which side an element came from.

Return type:

SparseDFA

Parameters:
autstr.composition.disjoint_union(left, right, tags=('<l>', '<r>'))[source]#

The disjoint union of two automatic structures over one signature.

An element of the left factor is encoded as tags[0] . w and one of the right factor as tags[1] . w, so the domains cannot collide and no tuple mixes the two sides – which is exactly right, since the relations of a disjoint union never cross it.

Note that a disjoint union is a relational construction: the disjoint union of two groups is not a group, because the multiplication becomes partial.

Return type:

AutomaticPresentation

Parameters:
autstr.composition.direct_product(left, right, kind='sync')[source]#

The direct product of two automatic structures over one signature.

An element is a pair, encoded over the pair alphabet: position i carries one letter of each component, the shorter one padded. Both products are then Boolean combinations of the factors embedded into that alphabet:

sync   R((a,b), (a',b'))  iff  R_A(a,a') and R_B(b,b')
async  R((a,b), (a',b'))  iff  (R_A(a,a') and b = b')
                                or (R_B(b,b') and a = a')

The synchronous product moves both coordinates at once; the asynchronous one moves exactly one and holds the other fixed. For a k-ary relation the equality side asks that all k tapes agree on the untouched half.

Parameters:
Return type:

AutomaticPresentation

autstr.composition.class_union(left, right, tags=('<l>', '<r>'), skip='<#>')[source]#

The union of two uniformly automatic classes over one signature.

A member of the result is a member of either class. What is tagged is the advice: an advice of the left class becomes tags[0] . alpha and one of the right class tags[1] . alpha, so the two advice languages are disjoint and each member is instantiated by exactly one of the factors.

Every tape of a convolution must be prefixed by one symbol, so the element tapes get the placeholder letter skip: an element w becomes skip . w. Use tagged_advice and tagged_element to build them.

Return type:

UniformlyAutomaticClass

Parameters:
autstr.composition.tagged_advice(advice, tag='<l>')[source]#

The advice of a factor, as an advice of the union.

autstr.composition.tagged_element(element, skip='<#>')[source]#

An element of a factor, as an element of the union.

autstr.composition.direct_product_closure(uniform, separator='<|>')[source]#

The class of all finite direct products of the class’s members.

The advice alpha_1 # ... # alpha_n presents the product of the members that alpha_1, ..., alpha_n present, and an element of that product is the tuple w_1 # ... # w_n of its components. Because an element of a member is never longer than its advice, the blocks line up positionally across every tape of a convolution, and a relation of the product is just the original relation holding in every block.

So each automaton – the domain and every relation alike – is the same block-reset wrapper of the original: read a block, and at a separator demand that the block was accepted and start the next one. The result has one more state than the original, where an encoding that interleaved the components would need one copy of the automaton per component.

This is the construction that takes the cyclic groups to the finite abelian groups (compare autstr.algebra.FiniteAbelianGroups, whose advice is a ‘#’-separated list of orders). Composed with class_union it mixes two families: direct_product_closure(class_union(C, D)) is the class of all finite products of members of either.

Requires every element to be no longer than its advice, which holds exactly when the members are finite; the construction cannot check it.

Return type:

UniformlyAutomaticClass

Parameters:
autstr.composition.blocks(*words, separator='<|>')[source]#

Concatenate advices or elements into one product advice/element.

Parameters:

separator (str)

autstr.graphs module#

Graphs of bounded tree-depth and bounded pathwidth as uniformly automatic classes.

Both classes present graphs over sets of vertices (as in MSO0), so first-order logic over the presentation is monadic second-order logic over the graph. The shared signature is

Sing(x) x is a singleton Subset(x,y) x is a subset of y E(x,y) x = {u}, y = {v} and u,v are adjacent

Tree-depth <= d (TreeDepthClass): the advice spells out a DFS traversal of an elimination forest of height <= d, one letter per vertex encoding (depth, adjacency profile to its ancestors).

Pathwidth <= w (PathWidthClass): the advice spells out a linear layout, one letter per vertex encoding (register in {0..w}, adjacency profile to the registers of its earlier neighbors). Introducing a vertex at register r replaces the previous occupant of r; edges may only reach current occupants, which is exactly the interval structure of a path decomposition of width w.

TreeDepthGraph / PathWidthGraph encapsulate the string representations of single graphs and convert from/to networkx.

class autstr.graphs.StringGraph(letters, nodes=None)[source]#

Bases: object

Base class for graphs encoded as strings of per-vertex letters.

Parameters:
property num_nodes: int#
edges()[source]#

Edge list (node names) decoded from the letters.

Return type:

List[Tuple]

encode_set(subset)[source]#

Encode a set of nodes as a {0,1}-word over the vertex positions.

Return type:

Tuple[str, ...]

to_networkx()[source]#

Convert back to a networkx graph (node names preserved).

to_graphviz(sets=None, filename=None, format='png', view=False)[source]#

Visualize the graph; sets maps labels to node sets that are highlighted (colored and annotated with the label).

Return type:

Graph

Parameters:
class autstr.graphs.TreeDepthGraph(letters, nodes=None)[source]#

Bases: StringGraph

A graph of bounded tree-depth in its string representation: the DFS traversal of an elimination forest, one (depth, profile) letter per vertex. profile[t-1] == 1 means the vertex is adjacent to its unique ancestor at depth t.

Parameters:
property height: int#

Height of the elimination forest (>= tree-depth of the graph).

edges()[source]#

Edge list (node names) decoded from the letters.

Return type:

List[Tuple]

classmethod from_networkx(graph, forest=None, exact_below=13)[source]#

Build the string representation from a networkx graph.

Parameters:

  • graph – undirected networkx graph

  • forest (Optional[Dict]) – optional elimination forest as a dict node -> parent (roots map to None or are absent). Every edge of the graph must connect a vertex to one of its forest ancestors.

  • exact_below (int) – for graphs with fewer vertices, an optimal elimination forest is computed by exhaustive search; larger graphs fall back to a DFS forest (always valid, possibly deeper than the tree-depth).

Return type:

TreeDepthGraph

class autstr.graphs.PathWidthGraph(letters, nodes=None)[source]#

Bases: StringGraph

A graph of bounded pathwidth in its string representation: a linear layout, one (register, profile) letter per vertex. Introducing a vertex at register r replaces the previous occupant of r; profile lists the registers of the vertex’s earlier neighbors (their current occupants).

Parameters:
property width: int#

Maximal register index (>= pathwidth of the graph).

edges()[source]#

Edge list (node names) decoded from the letters.

Return type:

List[Tuple]

classmethod from_networkx(graph, order=None, exact_below=13)[source]#

Build the string representation from a networkx graph.

Parameters:

  • graph – undirected networkx graph

  • order (Optional[Sequence]) – optional vertex ordering (linear layout). If omitted, a minimum vertex-separation ordering is computed exhaustively for graphs with fewer than exact_below vertices; larger graphs fall back to a BFS ordering (valid, possibly wider than the pathwidth).

  • exact_below (int)

Return type:

PathWidthGraph

class autstr.graphs.TreeDepthClass(d)[source]#

Bases: _SetGraphClass

The uniformly automatic class of graphs of tree-depth <= d, presented over set-valued elements (MSO0 style).

Parameters:

d (int)

advice(graph)[source]#

The advice string of a graph (its letters as alphabet symbols).

Return type:

List[str]

Parameters:

graph (TreeDepthGraph | Sequence[str])

class autstr.graphs.PathWidthClass(w)[source]#

Bases: _SetGraphClass

The uniformly automatic class of graphs of pathwidth <= w, presented over set-valued elements (MSO0 style).

Parameters:

w (int)

advice(graph)[source]#

The advice string of a graph (its letters as alphabet symbols).

Return type:

List[str]

Parameters:

graph (PathWidthGraph | Sequence[str])

autstr.groups module#

Uniformly automatic classes of finite groups.

Finite abelian groups (FiniteAbelianGroups): every finite abelian group is a direct sum of cyclic groups, so the advice is the ‘#’-separated list of their orders in LSB-first binary and addition is blockwise. This is the direct-product closure of the cyclic groups, made explicit – compare autstr.composition.direct_product_closure.

Groups with a cyclic subgroup of index <= 2 (IndexTwoCyclicGroups): every such group is <r, s | r^n, s^2 = r^w, s r s^-1 = r^u> with u^2 = 1 (mod n), and the classification yields six families over the cyclic part Z_n:

abelian Z_2 x Z_n u = 1 w = 0 cyclic C_2n u = 1 w = 1 dihedral D_n u = -1 w = 0 dicyclic Dic (Q_2n) u = -1 w = n/2 (n even) semidihedral SD_2n u = n/2 - 1 w = 0 (n = 2^k >= 4) modular M_2n u = n/2 + 1 w = 0 (n = 2^k >= 4)

The advice is one family symbol followed by the LSB-first binary digits of n; an element r^a s^e is encoded as the twist bit e followed by the digits of a. Multiplication obeys

(r^a s^e)(r^b s^f) = r^{a + u^e b + [e and f] w} s^{e xor f},

and every ingredient is regular: modular addition is the usual carry automaton, conjugation is the identity, negation, or +/-x + (x mod 2)*(n/2) (the n/2-shift is advice-recognizable), and w is an advice-definable constant. The relation M(x,y,z) is defined from these primitives by a first-order formula — the uniform analog of the Büchi-arithmetic bootstrap.

Extraspecial p-groups (ExtraspecialGroups(p), p a fixed prime): the Heisenberg-type group of order p^(1+2n) has elements (c, a, b) with c in Z_p, a, b in Z_p^n and multiplication

(c, a, b)(c’, a’, b’) = (c + c’ + <a, b’>, a + a’, b + b’).

For fixed p the bilinear correction <a, b’> pairs digits positionwise, so it is a running sum mod p in the automaton state — nilpotency class 2 with growing rank is uniformly automatic, in contrast to growing modulus (Heisenberg over Z_n interprets modular multiplication and is not).

Class-2 groups of bounded linear cut-rank (CutRankGroups(p, k, r)): the common generalization. A member is a central extension of Z_p^n by Z_p^k given by commutator labels [x_j, x_i] = y^B[j,i]; the advice spells out, cut by cut, a rank-<=r factorization of the crossing block of B, and the automaton carries r linear functionals of the digits read so far instead of the digits themselves. Bounded pathwidth, bounded vertex cover, the extraspecial matching and the complete graph (nothing commutes, pathwidth n-1, cut-rank 1!) are all special layouts.

class autstr.groups.IndexTwoCyclicGroups[source]#

Bases: SymbolicClassWrapper

The uniformly automatic class of finite groups with a cyclic subgroup of index <= 2, in one advice format. Signature: M(x,y,z) [z = x*y], T(x) [x is a twisted element r^a s], Eq(x,y), plus the primitives the bootstrap is built from (CAdd, Conj, IsW, family predicates, …).

FAMILY_SYMBOLS = {'abelian': 'fA', 'cyclic': 'fC', 'dicyclic': 'fQ', 'dihedral': 'fD', 'modular': 'fM', 'semidihedral': 'fS'}#
advice(family, n)[source]#

Advice string of the group in the given family over Z_n.

Return type:

List[str]

Parameters:
dihedral(n)[source]#

D_n of order 2n.

Return type:

List[str]

Parameters:

n (int)

dicyclic(n)[source]#

Dicyclic group of order 2n over Z_n (n even); n = 4 is Q_8.

Return type:

List[str]

Parameters:

n (int)

semidihedral(n)[source]#

SD of order 2n over Z_n, n = 2^k >= 4.

Return type:

List[str]

Parameters:

n (int)

modular(n)[source]#

Modular maximal-cyclic group of order 2n over Z_n, n = 2^k >= 4.

Return type:

List[str]

Parameters:

n (int)

cyclic(n)[source]#

C_2n presented over the index-2 subgroup Z_n.

Return type:

List[str]

Parameters:

n (int)

abelian(n)[source]#

Z_2 x Z_n.

Return type:

List[str]

Parameters:

n (int)

parameters(advice)[source]#

(family, n) described by an advice string.

Return type:

Tuple[str, int]

Parameters:

advice (Sequence[str])

encode(element, advice)[source]#

Encode r^a s^e, given as (e, a), for the group of the advice.

Return type:

List[str]

Parameters:
multiply(advice, g, h)[source]#

Reference implementation of the group law (for testing/decoding).

Return type:

Tuple[int, int]

Parameters:
evaluate(phi)[source]#
Return type:

Tuple[SparseDFA, List[str]]

check(phi, advice, **elements)[source]#

Model check against one group; free variables can be assigned elements as (twist, exponent) pairs.

Return type:

bool

Parameters:

advice (Sequence[str])

check_implicit(phi, advice, **elements)[source]#

Like check, evaluated implicitly (no query automaton).

Return type:

bool

Parameters:

advice (Sequence[str])

get_structure(advice)[source]#
Return type:

AutomaticPresentation

Parameters:

advice (Sequence[str])

class autstr.groups.ExtraspecialGroups(p)[source]#

Bases: SymbolicClassWrapper

For a fixed prime p, the uniformly automatic class of Heisenberg-type groups of order p^(1+2n): elements (c, a, b) with c in Z_p and a, b in Z_p^n, multiplied as (c,a,b)(c’,a’,b’) = (c + c’ + <a,b’>, a + a’, b + b’). Advice: the unary word 1^(n+1). Signature: M(x,y,z), Cen(x) [x is central], Eq(x,y).

Parameters:

p (int)

advice(n)[source]#

Advice string of the extraspecial group of order p^(1+2n).

Return type:

List[str]

Parameters:

n (int)

encode(element, n)[source]#

Encode (c, a_vector, b_vector) for the rank-n group.

Return type:

List[str]

Parameters:

n (int)

multiply(g, h)[source]#

Reference implementation of the group law.

Return type:

Tuple[int, Tuple[int, ...], Tuple[int, ...]]

evaluate(phi)[source]#
Return type:

Tuple[SparseDFA, List[str]]

check(phi, n, **elements)[source]#

Model check against the rank-n group; free variables can be assigned elements as (c, a_vector, b_vector) triples.

Return type:

bool

Parameters:

n (int)

check_implicit(phi, n, **elements)[source]#

Like check, evaluated implicitly (no query automaton).

Return type:

bool

Parameters:

n (int)

get_structure(n)[source]#
Return type:

AutomaticPresentation

Parameters:

n (int)

class autstr.groups.FiniteAbelianGroups(eager_equality=False)[source]#

Bases: SymbolicClassWrapper

The uniformly automatic class of all finite abelian groups, presented by their cyclic decompositions: the group Z_{n_1} ⊕ … ⊕ Z_{n_k} has advice bin(n_1)# … bin(n_k)# (LSB-first binary per block).

Parameters:

eager_equality (bool)

GRAPH = 'A'#

addition, not multiplication – these members are abelian by construction, and the class presents the operation as A(x, y, z).

OPERATOR = '+'#

the Python operator it binds to

EQUALITY = 'exists z0.(A(z0,z0,z0) and A(x,z0,y))'#

the identity is the unique idempotent, and x + 0 = y exactly when x = y. The witness may not be called e0: nltk reads e-names as event variables.

advice(orders)[source]#

Advice string of Z_{n_1} ⊕ … ⊕ Z_{n_k}.

Return type:

List[str]

Parameters:

orders (Sequence[int])

encode(element, orders)[source]#

Encode a group element (one value per cyclic factor).

Return type:

List[str]

Parameters:
evaluate(phi)[source]#
Return type:

Tuple[SparseDFA, List[str]]

check(phi, orders, **elements)[source]#

Model check against Z_{n_1} ⊕ … ⊕ Z_{n_k}; free variables can be assigned group elements (tuples with one value per factor, or a single int for a cyclic group).

Return type:

bool

Parameters:

orders (Sequence[int])

check_implicit(phi, orders, **elements)[source]#

Like check, evaluated implicitly (no query automaton).

Return type:

bool

Parameters:

orders (Sequence[int])

get_structure(orders)[source]#
Return type:

AutomaticPresentation

Parameters:

orders (Sequence[int])

class autstr.groups.CutRankGroups(p, k=1, r=1, d=1, factored=None)[source]#

Bases: SymbolicClassWrapper

For a fixed prime p, center dimension k, width r and ring depth d, the uniformly automatic class of class-2 groups over R = Z/p^d whose commutation form admits a linear layout of module cut-rank <= r (bounded linear rank-width over R). With d = 1 (the default) R is the field F_p and this is the original construction; d > 1 is the exponent-p^d (“Idea 2”) case, where the form is R-valued and the width is the module cut-rank of the crossing blocks (the streaming lifts unconditionally, carrying row-module generator interfaces).

A member is a form with labels B[j,i] in R^k for i < j, presenting x_j x_i = x_i x_j y^B[j,i]. Elements are (b, a) with b in R^k, a in R^n and

(b, a)(b’, a’) = (b + b’ + C(a, a’), a + a’), C(a, a’) = sum_{i<j} B[j,i] a_j a’_i,

a 2-cocycle because C is bilinear. The multiplication automaton never needs the digits it has read — only what the future consumes from them, which is the crossing block of B at the current cut. If every crossing block factors through rank r, the automaton can carry the r linear functionals w = V a’ instead of the digits. The advice letter at position t spells the factorization out — three matrices over Z_p:

T (r x r): basis change between cuts, w <- T w + v a’_t, v (r): coefficient of the new digit, R (k x r): read-off, sum_{i<t} B[t,i] a’_i = R w,

so the state is (deficit in Z_p^k, w in Z_p^r): p^(k+r) states however long the word. Every well-shaped advice presents some group in the class (the streamed cocycle is bilinear by construction), and advice compiles a form into letters, failing precisely when a cut exceeds rank r; linear_cut_rank measures the width a form needs.

Special layouts: a perfect matching is extraspecial (matching_form, cut-rank 1, compare ExtraspecialGroups); the complete graph — nothing commutes, pathwidth n-1 — also has cut-rank 1, its crossing blocks are all-ones (clique_form); a vertex cover of size c needs rank <= c. Signature: M(x,y,z), Eq(x,y); the center is first-order definable, Cen(x) := all y,z,w (M(x,y,z) and M(y,x,w) -> z = w).

factored=None (the default) enumerates one advice letter per (T, v, R) triple when that alphabet fits under 20000 letters (the original encoding, byte-identical) and otherwise switches to factored letters: each position becomes a marker ‘n’ followed by one letter per ring entry (T row-major, then v, then R row-major), with the element digit repeated along the stretch. The factored alphabet has q+1 advice letters however large r, k and d are – this is what makes width r >= 2 over the ring representable.

Parameters:
MARKER = 'n'#

marker letter opening each position’s entry stretch in factored mode

letters: Dict[str, tuple]#
entry_letters: Dict[str, int]#
property cls: UniformlyAutomaticClass#

the multiplication automaton is a 4-tape product over the full advice alphabet, so its construction is O(sigma^4) and only feasible for a small ring alphabet (essentially Z/4, width 1). The reference law, advice compiler, width measure and simulate do not need it and stay cheap for any q.

Type:

The uniformly automatic presentation, built lazily

linear_cut_rank(n, form)[source]#

The width the given layout of the form needs: the maximal module cut-rank over R = Z/p^d of its crossing blocks (the free rank of the saturated interface; the ordinary F_p rank when d = 1).

Return type:

int

Parameters:
advice(n, form)[source]#

Compile a form — {(j, i): label in Z_p^k, i < j} — into advice. Maintains a row basis V of each crossing block’s row space and expresses the next basis and the current read-off row over it; raises if some cut exceeds rank r.

Return type:

List[str]

Parameters:
clique_form(n, label=None)[source]#

Nothing commutes: [x_j, x_i] = y^label for every pair. Pathwidth n-1, but every crossing block is all-ones — cut-rank 1.

Return type:

Dict

Parameters:
matching_form(n)[source]#

Disjoint commutator pairs hitting the first center coordinate: the extraspecial layout, cut-rank 1.

Return type:

Dict

Parameters:

n (int)

multiply(n, form, g, h)[source]#

Reference implementation of the group law given by the form, over R = Z/p^d (both quotient and center coordinates range over R).

Parameters:
simulate(advice, gx, gy, gz)[source]#

Run the multiplication automaton directly over the tapes: True iff the advice accepts gx * gy = gz. Mirrors the M transition without building the 4-tape product DFA, so the streamed compile can be checked against the reference law for any ring alphabet (the full automaton is only buildable for small q). gx, gy, gz are (b, a) elements.

Return type:

bool

Parameters:

advice (Sequence[str])

identity(n)[source]#
Parameters:

n (int)

encode(element, n)[source]#

Encode (b, a) with b in R^k, a in R^n, R = Z/p^d. In factored mode each position’s digit is repeated along its entry stretch.

Return type:

List[str]

Parameters:

n (int)

decode(word)[source]#

Inverse of encode: an element word back to its (b, a) tuple.

Parameters:

word (Sequence[str])

evaluate(phi)[source]#
Return type:

Tuple[SparseDFA, List[str]]

check(phi, advice, **elements)[source]#

Model check against the member presented by the advice; free variables can be assigned elements as (b, a) tuples.

Return type:

bool

Parameters:

advice (Sequence[str])

property implicit_cls#

The fully implicit presentation of this class (functional atoms only, nothing compiled): an autstr.implicit.ImplicitClass over raw element words. check_implicit/evaluate_implicit add the (b, a)-tuple encoding on top of it.

check_implicit(phi, advice, **elements)[source]#

Like check, but evaluated implicitly (no query or base automaton) – the only viable model checker for the large-alphabet ring members whose cls cannot be built. See autstr.implicit.

Return type:

bool

Parameters:

advice (Sequence[str])

evaluate_implicit(phi, advice, **elements)[source]#

The satisfying set of phi on the member presented by the advice, computed implicitly: unassigned free variables stay open and are solved for. Yields assignments {var: (b, a)}; len is the exact solution count without enumeration. Works for members whose automata cannot be built.

Parameters:

advice (Sequence[str])

get_structure(advice)[source]#
Return type:

AutomaticPresentation

Parameters:

advice (Sequence[str])

class autstr.groups.InfiniteExtraspecialGroup(p=3)[source]#

Bases: object

The infinite extraspecial p-group: finitely supported vectors over F_p with a one-digit centre.

An element is a triple (a, b, c) with a, b finitely supported sequences over F_p and c in F_p, multiplied by

(a, b, c) * (a’, b’, c’) = (a + a’, b + b’, c + c’ + <a, b’>),

the central extension of F_p^(w) + F_p^(w) by F_p along the standard symplectic form. It is non-abelian – the commutator of (a, b, c) and (a’, b’, c’) is <a, b’> - <a’, b> – and unlike ExtraspecialGroups it is a single infinite structure rather than a class of finite ones, so its elements have an advice-free encoding and can be written as constants.

Encoding: the first letter carries the centre, and letter i + 1 carries the pair (a_i, b_i); trailing (0, 0) pairs are trimmed, so encodings are unique and equality is the diagonal.

Parameters:

p (int)

PAD = '*'#
encode(element)[source]#

(a, b, c) -> word. a and b are sequences of digits.

Return type:

List[str]

decode(word)[source]#
multiply(x, y)[source]#

The reference product, for checking the automaton against.

default_signature()[source]#
symbolic(signature=None)[source]#

A symbolic interface with * bound to the group product.

autstr.implicit module#

Implicit first-order evaluation, without compiling a query automaton.

The explicit path (presentations.AutomaticPresentation._build_automaton) turns a formula into a product automaton – intersection for AND, union for OR, complement for NOT, projection for EXISTS – and materialises it. That product blows up, and for the heavy group classes even the base multiplication automaton is infeasible to build (an O(sigma^4) product over the astronomical advice alphabet).

This module evaluates a formula implicitly instead: it keeps composite states and steps the base automata on the fly. Boolean connectives take the product of states; EXISTS is handled by an on-the-fly powerset (subset construction); NOT flips the acceptance test (exact, because every composite stays deterministic and total). The base automata are given by a small functional interface, so a class whose presentation cannot even be built is still checkable – this is the simulate methods of the group classes generalised to arbitrary first-order formulas.

Everything here works over a fixed input: an advice word/tree plus concrete assignments for some free variables; the remaining free variables are existentially closed and eliminated by the powerset construction. Because the advice is fixed input and quantifiers range over element tapes whose per-symbol alphabet is tiny, the subset construction never touches the huge advice alphabet; the cost is set by quantifier alternation, not alphabet size.

Two shapes, one combinator pattern:

  • ImplicitDFA – string automata, run left-to-right.

  • ImplicitTA – bottom-up tree automata, run post-order.

Beyond the boolean check_* entry points, the module offers the satisfying-set primitive: StringSolutionSet/TreeSolutionSet compute, for a formula with open free variables over a fixed advice, the exact number of satisfying assignments (a count DP over the reachable composite states — no enumeration) and lazily enumerate them. ImplicitClass/ImplicitTreeClass package atoms + element alphabet as a first-class fully implicit presentation: a uniformly automatic class given purely functionally, offering model checking and satisfying-set evaluation and never compiling anything.

class autstr.implicit.ImplicitDFA(tapes, initial, step, accepting)[source]#

Bases: object

A deterministic, total automaton over a set of named tapes, given functionally. A symbol is a dict {tape: value}; the automaton reads only its own tapes from it.

Parameters:
initial()[source]#
step(state, symbol)[source]#
Parameters:

symbol (Dict[str, object])

accepting(state)[source]#
Return type:

bool

autstr.implicit.dfa_atom(dfa, tapes)[source]#

Wrap an explicit SparseDFA as an implicit atom. tapes names the DFA’s tapes in the DFA’s own symbol order.

Return type:

ImplicitDFA

Parameters:

tapes (Sequence[str])

autstr.implicit.dfa_product(a, b, accept)[source]#
Return type:

ImplicitDFA

Parameters:
autstr.implicit.dfa_complement(a)[source]#
Return type:

ImplicitDFA

Parameters:

a (ImplicitDFA)

autstr.implicit.dfa_project(a, var, alphabet)[source]#

EXISTS var: subset construction. State is a frozenset of a-states; each step guesses var’s symbol over alphabet from every state in the set.

Return type:

ImplicitDFA

Parameters:
autstr.implicit.run_dfa(a, inputs, length)[source]#

Run over length synchronised positions; inputs gives a word for each of the automaton’s remaining tapes.

Return type:

bool

Parameters:
class autstr.implicit.ImplicitTA(tapes, step, accepting)[source]#

Bases: object

A deterministic bottom-up tree automaton over named tapes. step takes the node’s symbol dict and the child states (None for a missing child).

Parameters:
step(symbol, left, right)[source]#
accepting(state)[source]#
Return type:

bool

autstr.implicit.ta_atom(sta, tapes)[source]#

Wrap an explicit SparseTreeAutomaton as an implicit atom.

Return type:

ImplicitTA

Parameters:

tapes (Sequence[str])

autstr.implicit.ta_product(a, b, accept)[source]#
Return type:

ImplicitTA

Parameters:
autstr.implicit.ta_complement(a)[source]#
Return type:

ImplicitTA

Parameters:

a (ImplicitTA)

autstr.implicit.ta_project(a, var, alphabet)[source]#

EXISTS var: bottom-up subset construction. State is a frozenset of a-states; a missing child contributes the singleton {None}.

Return type:

ImplicitTA

Parameters:
autstr.implicit.run_ta(a, inputs)[source]#

Run over labelled trees (one per tape, all of the same shape).

Return type:

bool

Parameters:
class autstr.implicit.StringSolutionSet(a, inputs, length, solve_vars, alphabet_of)[source]#

Bases: object

The satisfying assignments for the open variables of an implicit string automaton over a fixed input.

One forward pass stores, per position, the reachable composite states with their outgoing edges (one per guessed symbol tuple); one backward pass counts the accepted suffixes per state. len is then the exact number of satisfying assignments without any enumeration, truthiness is non-emptiness, and iteration lazily yields {var: word} dicts (each word a list of element symbols, one per position). Deterministic composite states make the count exact: every assignment has exactly one run.

Parameters:
class autstr.implicit.TreeSolutionSet(a, inputs, solve_vars, alphabet_of)[source]#

Bases: object

The satisfying assignments for the open variables of an implicit bottom-up tree automaton over a fixed input; assignments are labelled trees of the input’s exact shape. A bottom-up pass counts, per node and reachable state, the subtree labelings that reach it; len sums the accepting root states, iteration re-derives the labelings top-down.

Parameters:
class autstr.implicit.MappedSolutions(base, mapper)[source]#

Bases: object

A solution set with a mapper applied to every assignment value (e.g. decoding element words/trees back to group elements).

autstr.implicit.check_string(phi, atoms, inputs, length, alphabet_of)[source]#

Implicitly decide a (relativized) formula over string automata.

Parameters:

  • atoms (Dict) – relation name -> an atom builder args -> ImplicitDFA (or a SparseDFA, wrapped via dfa_atom with the formula’s argument order).

  • inputs (Dict[str, Sequence]) – a word for every tape that survives to the top (advice and assigned variables).

  • alphabet_of – var name -> iterable of element symbols to guess for it.

  • length (int)

Return type:

bool

autstr.implicit.check_tree(phi, atoms, inputs, alphabet_of)[source]#

Implicitly decide a (relativized) formula over tree automata.

Parameters:

  • atoms (Dict) – relation name -> an atom builder args -> ImplicitTA (or a SparseTreeAutomaton, wrapped via ta_atom).

  • inputs (Dict[str, object]) – a labelled tree for every surviving tape (all same shape).

Return type:

bool

autstr.implicit.relativized_query(phi, assignments, relativize, variable_names, close_free=True)[source]#

Relativize to a fresh advice variable and add the Adv/Dom guards – the same query the explicit evaluate/check build, but returned as an expression for implicit evaluation. With close_free (the model-checking contract) unassigned free variables are existentially closed; without it (the satisfying-set contract) they stay open and are returned as the solve variables.

Parameters:

  • relativize – UniformlyAutomaticClass._relativize (static).

  • variable_names – UniformlyAutomaticClass._variable_names (static).

Returns:

(query expression, advice variable name, assigned variable names, solve variable names).

autstr.implicit.check_class_string(phi, advice, assignments, atoms, element_alphabet, relativize, variable_names)[source]#

Implicit model check over string automata: relativize then run. atoms maps each wrapped relation (Dom, Adv, and the class relations) to a SparseDFA or a functional builder args -> ImplicitDFA.

Return type:

bool

autstr.implicit.check_class_tree(phi, advice, assignments, atoms, element_alphabet, relativize, variable_names)[source]#

Implicit model check over tree automata: relativize then run bottom-up. atoms maps each wrapped relation to a SparseTreeAutomaton or a functional builder args -> ImplicitTA.

Return type:

bool

autstr.implicit.evaluate_class_string(phi, advice, assignments, atoms, element_alphabet, relativize, variable_names)[source]#

The satisfying set of a formula over the member presented by the advice, computed implicitly: unassigned free variables stay open and are solved for over the fixed advice. Returns a StringSolutionSet of {var: word} assignments (exact len without enumeration).

Return type:

StringSolutionSet

autstr.implicit.evaluate_class_tree(phi, advice, assignments, atoms, element_alphabet, relativize, variable_names)[source]#

Tree analog of evaluate_class_string: the satisfying assignments are labelled trees of the advice’s shape.

Return type:

TreeSolutionSet

class autstr.implicit.ImplicitClass(atoms, element_alphabet)[source]#

Bases: object

A uniformly automatic class given purely functionally – the fully implicit presentation. atoms maps every relation name (including the wrapped ‘Dom’ and ‘Adv’) to a builder args -> ImplicitDFA (or an explicit SparseDFA to wrap); element_alphabet lists the per-position element symbols quantifiers guess from. Nothing is ever compiled: the class offers implicit model checking and satisfying-set evaluation only, so it reaches members whose presentation automata cannot be built.

Parameters:
check(phi, advice, **assignments)[source]#

Model check against the member presented by the advice word; unassigned free variables are existentially closed.

Return type:

bool

evaluate(phi, advice, **assignments)[source]#

The satisfying set for the open free variables over the member presented by the advice word.

Return type:

StringSolutionSet

class autstr.implicit.ImplicitTreeClass(atoms, element_alphabet)[source]#

Bases: object

Tree analog of ImplicitClass: atoms are args -> ImplicitTA builders (or explicit SparseTreeAutomaton objects), members are advice trees.

Parameters:
check(phi, advice, **assignments)[source]#

Model check against the member presented by the advice tree; unassigned free variables are existentially closed.

Return type:

bool

evaluate(phi, advice, **assignments)[source]#

The satisfying set for the open free variables over the member presented by the advice tree.

Return type:

TreeSolutionSet

autstr.infinite_graphs module#

Infinite graphs as automatic structures.

A thin, engine-agnostic wrapper over an automatic or tree-automatic presentation whose signature has a domain U and a binary edge relation. It adds the graph vocabulary on top of the symbolic layer — x.adj(y) for adjacency, plus .eq — so every infinite-graph factory (ordinals, integer grids, the level-2 collapsible pushdown graphs, …) plugs into one surface, exactly as InfiniteExtraspecialGroup shares a presentation.

The wrapper decides nothing itself: it forwards to the presentation, which is where FO(∃^∞) is decided by synchronous projection. It works over either the string or the tree engine, since both presentations expose the same relational interface (symbolic, check, evaluate, relation, get_relation_symbols).

class autstr.infinite_graphs.InfiniteGraph(presentation, edge=None, directed=False, codec=None)[source]#

Bases: object

A graph presented by automata: a domain and a binary edge relation.

Parameters:

  • presentation – an AutomaticPresentation or TreeAutomaticPresentation carrying the domain U and the edge relation.

  • edge (Optional[str]) – the binary relation read as adjacency (default 'E').

  • directed (bool) – whether edges are directed. Undirected is the default; the edge automaton is expected to be symmetric, which is_symmetric checks.

  • codec – optional element codec, so vertices can be written as Python constants and solutions decoded.

EDGE = 'E'#

the default name of the edge relation

default_signature()[source]#

The signature symbolic() uses when none is given: .adj bound to the edge relation, and .eq when the graph declares equality.

symbolic(signature=None)[source]#

A symbolic interface to the graph. Build first-order formulas with x.adj(y) and the usual connectives / quantifiers; see autstr.symbolic.

is_symmetric()[source]#

Whether the edge relation is symmetric — decidable here, since it is a first-order question over an automatic structure. An undirected graph must satisfy it.

Return type:

bool

check(phi)[source]#

Truth of a formula over the graph (free variables existential).

Return type:

bool

evaluate(phi)[source]#

The relation of satisfying assignments of a formula.

get_relation_symbols()[source]#

All relation symbols of the graph (‘U’ is the domain).

class autstr.infinite_graphs.IntegerGrid(n=2)[source]#

Bases: object

The n-dimensional integer grid — the Cayley graph of ℤⁿ with the standard generators.

Vertices are points of ℤⁿ; two are adjacent iff they differ by ±1 in exactly one coordinate. That is precisely the asynchronous product of n copies of the two-way integer path (move one coordinate, hold the rest), so the grid is built by folding autstr.composition.direct_product over n integer paths rather than by authoring an automaton.

FO is decidable — it is an automatic structure. MSO is not: the grid interprets the halting problem, the tidiest illustration that FO and MSO are different questions.

Parameters:

n (int) – the dimension (n ≥ 1). IntegerGrid(1) is the two-way path.

encode(point)[source]#
Return type:

list

Parameters:

point (Sequence[int])

decode(word)[source]#
Return type:

Tuple[int, ...]

symbolic(signature=None)[source]#

A symbolic interface to the grid; write adjacency as x.adj(y) and vertices as Python n-tuples.

is_symmetric()[source]#
Return type:

bool

check(phi)[source]#
Return type:

bool

evaluate(phi)[source]#
class autstr.infinite_graphs.RegularTree(k=2)[source]#

Bases: object

The infinite k-ary tree \(T_k\), with its successors and the prefix order.

Vertices are the words over {0, …, k-1}: the root is the empty word, and x·i is the i-th child of x. So the tree is its own encoding, and the relations are small automata read straight off the word operations — appending one letter, and being a prefix — rather than derived from another structure.

The presentation carries S0 … S{k-1} (Si(x, y) iff y = x·i), their union Child, Prefix (the reflexive prefix order, i.e. ancestor-or-self), Eq, and the undirected child edge E, under which the tree is a graph: the root has degree k and every other vertex degree k+1.

\(T_k\) is the Cayley graph of the free monoid on k generators, and the 2k-regular version is the Cayley graph of the free group — the same object the pushdown graphs are unravelled from.

Parameters:

k (int) – the branching degree (k ≥ 1). RegularTree(1) is a ray.

encode(vertex)[source]#

The encoding of a vertex, written as a sequence of child indices — (0, 1, 1), or the string '011' — with the empty sequence for the root.

Return type:

list

decode(word)[source]#

The vertex encoded by a word, as a tuple of child indices.

Return type:

Tuple[int, ...]

symbolic(signature=None)[source]#

A symbolic interface to the tree; write the child edge as x.adj(y) and vertices as sequences of child indices. The successors and the prefix order are reached by name, through autstr.symbolic.SymbolicContext.rel.

is_symmetric()[source]#
Return type:

bool

check(phi)[source]#
Return type:

bool

evaluate(phi)[source]#
get_relation_symbols()[source]#

autstr.interpretations module#

First-order interpretations of automatic structures.

Automatic structures are closed under first-order interpretations, and AutStr can compute the interpreted presentation: presentation.evaluate(φ) already returns the automaton of an FO formula’s satisfying assignments, so an interpretation is orchestration, not a new engine. It is the FO counterpart of the set / MSO interpretations that build the Caucal hierarchy.

An element of the interpreted structure is a k-tuple of source elements satisfying the domain formula; each relation is defined by an FO formula over the source’s signature, with its free variables grouped k-per-argument. The formula automata are folded — every k consecutive coordinate tapes become one element tape over the product alphabet — so the result is a standard presentation whose elements are k-tuples.

For dimension == 1 (the default) this is just a definable reduct/expansion with a restricted domain: elements keep the source’s encoding, and the interpreted automata are the canonical minimal DFAs of the formulas — bit-for- bit what a hand-built presentation would produce. For k > 1 elements are encoded as k-tape convolutions; measurement shows this adds no states (the engine minimizes away a sparse domain’s redundancy) but a bounded ×k symbol-width overhead, intrinsic to representing tuples.

Quotient interpretations (elements as classes of a definable equivalence) are supported at every dimension and on either engine: pass quotient=ε, and the universe is restricted to one representative per class.

Both engines. The source may be an AutomaticPresentation or a TreeAutomaticPresentation, and the result is a presentation of the same kind; the orchestration is identical because both engines encode a convolution letter the same way. Over trees an element of a k-dimensional interpretation is a k-tuple of trees, which is one tree over k-tuples — the same fold, since the tree convolution already overlays the shapes.

Only the choice of representative differs. Over words it is the shortlex-least element of the class, and shortlex is a well-order, so that element exists. Over trees no automatic order is well-founded — growing a tree at the position where two differ makes it smaller — so a class need have no least element at all, and the representative is instead the least description: a member that reaches only so far past the positions the whole class shares. That is Kuske and Weidner’s construction; _tree_representatives gives it in full, including why the expensive half of their proof is not needed here. It is the one part of this module that can blow up — provably so — and it is worth passing max_states to the source presentation before asking for a large one.

autstr.interpretations.RelationSpec#

a relation is a formula, or a (formula, coordinate-order) pair; the coordinate order lists the free variables element-major (each element’s k coordinates together), and may be omitted when the sorted order already is

alias of str | Expression | Tuple[str | Expression, Sequence[str]]

autstr.interpretations.interpret(source, domain, relations, dimension=1, quotient=None)[source]#

The first-order interpretation of a structure in source.

Parameters:

  • source – the structure to interpret in — an AutomaticPresentation or a TreeAutomaticPresentation. The result is a presentation of the same kind.

  • domain (Union[str, Expression, Tuple[Union[str, Expression], Sequence[str]]]) – the domain formula δ(x̄) with dimension free variables — the coordinates of one element; the new universe is the tuples satisfying it. A (formula, coordinate-order) pair fixes which free variable is which coordinate when the sorted order will not do.

  • relations (Dict[str, Union[str, Expression, Tuple[Union[str, Expression], Sequence[str]]]]) – {name: spec} where spec is a formula or a (formula, coordinate-order) pair. A relation of arity r has dimension · r free variables; the coordinate order lists them element-major, so folding groups each argument’s coordinates.

  • dimension (int) – k — elements are k-tuples of source elements.

  • quotient (Union[str, Expression, Tuple[Union[str, Expression], Sequence[str]], None]) – an equivalence formula ε(x̄, ȳ) (a binary relation over elements, so 2 · dimension free variables). When given, elements are its equivalence classes: the universe is restricted to one representative of each class, and the relations are read on those representatives. The caller must ensure ε really is an equivalence and that every relation is ε-invariant. Over words the representative is the shortlex-least member of the class; over trees it is the least description, which is the same idea made to work without a well-order, and which may cost exponentially many states (_tree_representatives).

Returns:

a fresh presentation of the same kind as source. For k > 1 its alphabet is the source alphabet’s k-fold product.

autstr.mtbdd module#

A shared multi-terminal BDD store for transition symbols.

Sparse automata over convolution alphabets used to store transitions as flat (left, right, symbol) -> target rows. That representation forces every operation to enumerate symbols: cylindrification duplicates each row once per letter of every new tape, padding blankets multiply out, and a set quantifier over a wide convolution produces exception tables with millions of rows that all say the same thing about the same digits. This module replaces the symbol column by a decision diagram over the digits of the symbol, which is the representation MONA uses for the same reason.

Encoding. A symbol of a k-tape convolution over a base alphabet of size m is the integer sum_t digit_t * m**(k-1-t). Each letter is written in bits = ceil(log2 m) binary variables, most significant first, and the global variable order is tape-major: variable t*bits + j is bit j of tape t. A tape therefore occupies a contiguous block of variables, so existential projection quantifies a block, and cylindrification renames blocks.

Nodes. A node is either a terminal carrying an integer value (a state, or a subset id, or a class id — the callers decide) or an internal node (var, lo, hi) whose children test strictly larger variables. Nodes are reduced (lo != hi) and hash-consed in one process-wide store, so structurally equal transition functions are the same node: equality of behavior is an integer comparison, and the memo tables of apply are shared across pairs of states and across automata.

Invalid codes. When m is not a power of two some binary codes denote no letter. Every node built here maps those codes to the reserved terminal NONE, and every operation propagates it, so the reachable-target set of a node never contains a state that only an invalid code would reach — the counting arguments the flat representation needed (“does this pair except all m preimages of the symbol?”) disappear.

autstr.mtbdd.num_bits(m)[source]#

Binary variables per letter of an m-letter alphabet.

Return type:

int

Parameters:

m (int)

class autstr.mtbdd.ComputedTable(cap_log2=23, dict_limit=524288)[source]#

Bases: object

A memo for apply that is exact while small and lossy once large.

A dict memo for apply2 grows without bound: a set quantifier fills it with tens of millions of entries at roughly 180 bytes each, outweighing the nodes it caches. But most apply calls in a normal query are tiny, and a dict beats any hand-rolled table at that size.

So: a plain dict until it exceeds dict_limit entries, then a direct-mapped array of (key, value) pairs at 16 bytes per slot that simply overwrites on collision. Memory is bounded by the table; a miss only recomputes a pure function.

Correctness rests on apply’s terminal operations being deterministic functions of their arguments: recomputing an entry allocates no new state id or subset, it re-derives the same one. Only the computed tables may be lossy — the unique table NodeStore._node_ids must stay exact, or hash-consing breaks and node equality stops meaning function equality.

Parameters:

  • cap_log2 (int)

  • dict_limit (int)

mask#
shift#
keys#
vals#
get(key, default=None)[source]#
Parameters:

key (int)

remap(mapping)[source]#

A copy of this memo with every node id renumbered, dropping the entries whose operands or result did not survive a sweep.

Return type:

ComputedTable

Parameters:

mapping (Dict[int, int])

autstr.mtbdd.bits_of(mask)[source]#

The set bit positions of an integer bitset, ascending.

Subset constructions intern one set of states per union result — including every intermediate inside apply2 — so the sets are held as python ints: a bitset costs num_states/8 bytes and hashes in one pass, where a frozenset costs tens of bytes per member.

Return type:

List[int]

Parameters:

mask (int)

class autstr.mtbdd.NodeStore[source]#

Bases: object

Hash-consed multi-terminal BDD nodes with memoized operations.

A set quantifier can create millions of nodes, so the per-node cost is part of the algorithm: var/lo/hi/term are array(‘q’) (8 bytes each, against 36 for a python list slot holding a boxed int) and the unique table is keyed by a single packed integer rather than a 3-tuple.

terminal(value)[source]#
Return type:

int

Parameters:

value (int)

make(var, lo, hi)[source]#
Return type:

int

Parameters:
is_terminal(node)[source]#
Return type:

bool

Parameters:

node (int)

letter(tape, children, m, bits)[source]#

The binary decision tree over tape tape’s variable block that selects children[d] on digit d; codes d >= m lead to NONE.

Return type:

int

Parameters:
const(value, arity, m, bits)[source]#

The node mapping every valid symbol of an arity-tape convolution to value (and every invalid code to NONE).

Return type:

int

Parameters:
build_rows(symbols, targets, base, arity, m, bits)[source]#

The node of a transition function given as a base value plus a sorted list of symbol -> target deviations.

Return type:

int

Parameters:
map_letters(node, arity, old_m, old_bits, new_m, new_bits, source, fill)[source]#

Re-express a diagram over a different base alphabet.

source[d] names the old letter that the new letter d should behave like, or -1 to send it to fill. The map runs from the new alphabet to the old one, so it need not be injective: several new letters may share an old one. That is what embeds a factor into a product’s pair alphabet, where every pair (a, b) behaves like its own component.

Per tape, take the old block’s old_m cofactors and reassemble them at the new digits. One memoized pass over the nodes – widening an alphabet never rebuilds a transition table, which is why a direct product is affordable: the pair alphabet has |A| * |B| letters but its diagrams have bits_A + bits_B variables. Letters multiply; bits add.

Return type:

int

Parameters:
fold_tapes(node, arity, m, bits, k)[source]#

Group every k consecutive tapes into one tape over the product alphabet Sigma^k.

The result reads arity // k tapes whose letters are k-tuples, ordered lexicographically (mixed-radix, first component most significant) – which is the order encode_symbol gives a set of tuples, so the encodings line up. New digit D at element-tape e decodes to old digit (D // m**(k-1-i)) % m at old tape e*k + i.

Diagram surgery mirrors map_letters, but one new tape consumes k old tapes, so its cofactors range over all m**k combinations rather than m.

Return type:

int

Parameters:
recode_letters(node, arity, old_m, old_bits, new_m, new_bits, digit_map, fill)[source]#

Injective relabelling: old letter d becomes new letter digit_map[d]; new letters outside the image go to fill.

Return type:

int

Parameters:
set_path(node, assignment, value)[source]#

The node that agrees with node everywhere except on the single full variable assignment assignment, where it takes value.

Return type:

int

Parameters:
cofactor(node, var, bit)[source]#
Return type:

int

Parameters:
mux(var, on_high, on_low)[source]#

The node that behaves like on_high where var is 1 and like on_low where it is 0 — var may sit below the arguments’ roots, in which case they are pushed down.

Return type:

int

Parameters:
rename(node, varmap, cache)[source]#

Substitute variable v by variable varmap[v]. The map need not be monotone or injective: identifying two variables restricts the function to their diagonal (which is how a relation R(x, x) is built). Monotone maps cost one node per node.

Return type:

int

Parameters:
apply2(f, g, op, cache)[source]#

Pointwise combination of two nodes; op acts on terminal values.

cache is a memo keyed by the packed node pair: a dict, or a bounded ComputedTable when the pair space is large enough that an exact memo would outweigh the nodes it caches.

Return type:

int

Parameters:
apply1(f, fn, cache)[source]#

Relabel the terminals of a node.

Return type:

int

Parameters:
quantify_letter(node, tape, m, bits, op, cache)[source]#

Combine the m cofactors of node on tape tape’s letter with op — the tape’s variables no longer occur in the result.

Return type:

int

Parameters:
terminals(node)[source]#

The terminal values reachable in node, sorted, without NONE.

Return type:

Tuple[int, ...]

Parameters:

node (int)

reset()[source]#

Drop every node and memo. Only valid on a scratch store: node ids are indices, so any surviving holder of one is left dangling.

Return type:

None

collect(roots)[source]#

Mark-sweep this store down to the sub-DAG below roots. A subset construction abandons the set-valued diagram of every subset as soon as it has been relabelled, but hash-consing keeps it forever; on a scratch store those nodes can be reclaimed.

Node ids are indices, so a sweep renumbers everything. Returns the roots’ new ids together with the old -> new map of every surviving node, which the caller needs to translate its apply memos (they map ids to ids, and dropping them instead makes the sweep cost more in recomputation than it saves in memory).

export(roots)[source]#

Extract the sub-DAG below roots as standalone arrays, renumbered so that children precede parents. Returns (var, lo, hi, term, roots).

Return type:

Tuple[ndarray, ndarray, ndarray, ndarray, ndarray]

import_nodes(var, lo, hi, term, roots)[source]#

Re-intern an exported sub-DAG (children first) into this store.

Return type:

ndarray

size(roots)[source]#

Number of distinct nodes below the given roots.

Return type:

int

eval_batch(nodes, symbols, arity, m, bits)[source]#

Terminal value of each node at its symbol (batched descent).

Return type:

ndarray

Parameters:
autstr.mtbdd.var_tables(arity, m, bits)[source]#

Per-variable digit divisor and bit shift for symbol decoding.

Parameters:

autstr.ordinals module#

Ordinals as automatic structures, on both engines.

Delhommé’s theorem draws two lines. The word-automatic ordinals are precisely those below \(\omega^\omega\), and the tree-automatic ones precisely those below \(\omega^{\omega^\omega}\). Every ordinal below the first line lives in some \(\omega^n\) and every ordinal below the second in some \(\omega^{\omega^n}\), so two factories cover both classes exactly: Ordinal on the string engine and TreeOrdinal on the tree engine. Neither boundary ordinal is itself reachable — \(\omega^\omega\) is not word-automatic, \(\omega^{\omega^\omega}\) not tree-automatic — which is why both take an exponent rather than being a single structure.

Ordinal is derived, not authored. By Cantor normal form an ordinal \(\alpha < \omega^n\) is uniquely \(\sum_{i<n} \omega^i c_i\) with natural coefficients, so \(\omega^n\) is the set of n-tuples of naturals under reverse-lexicographic order — an n-dimensional first-order interpretation of Büchi arithmetic:

>>> W2 = Ordinal(2)                       # the ordinals below ω²
>>> S = W2.symbolic()
>>> a, b = S.vars("a b")
>>> a.lt(b).evaluate().contains(a=(0, 7), b=(1, 0))   # 7 < ω
True

Ordinals are written as Python tuples of Cantor coefficients in descending exponent order, so (3, 2, 5) in Ordinal(3) is \(\omega^2 \cdot 3 + \omega \cdot 2 + 5\) and tuples compare lexicographically exactly as the ordinals do. A plain integer is the finite ordinal of that value.

The signature carries the strict order .lt, equality .eq and the successor .succ. Everything else is first-order over those and can be defined on the spot: a limit ordinal is one that is neither zero nor a successor, and both structures have a definable least element but no greatest.

TreeOrdinal reaches past the word barrier by nesting the same idea: an ordinal below \(\omega^{\omega^n}\) is a finite sequence of blocks indexed by the leading exponent coefficient, each block an ordinal below \(\omega^{\omega^{n-1}}\), bottoming out at a natural number. That nesting is a tree, and it is authored rather than interpreted — see TreeOrdinal.

autstr.ordinals.OrdinalValue#

coefficients in descending exponent order, or an integer

Type:

a Python ordinal

alias of int | Sequence[int]

class autstr.ordinals.Ordinal(n=1)[source]#

Bases: object

The ordinals below \(\omega^n\), under their natural order.

Parameters:

n (int) – the exponent (n ≥ 1). Ordinal(1) is \((\omega, <)\), i.e. the naturals; Ordinal(2) is \((\omega^2, <)\).

The presentation carries Lt (the strict order), Eq and Succ (the graph of the successor function, Succ(x, y) iff y = x + 1).

encode(value)[source]#

The encoding of an ordinal written as its Cantor coefficients in descending exponent order (or as a plain integer, for a finite ordinal).

Return type:

list

Parameters:

value (int | Sequence[int])

decode(word)[source]#

The ordinal encoded by a word, as a tuple of Cantor coefficients in descending exponent order.

Return type:

Tuple[int, ...]

default_signature()[source]#

The signature symbolic() uses when none is given: .lt, .eq and .succ, with ordinals written as coefficient tuples.

symbolic(signature=None)[source]#

A symbolic interface to the order; write a.lt(b) and ordinals as Python coefficient tuples.

check(phi)[source]#

Truth of a formula over the ordinals (free variables existential).

Return type:

bool

evaluate(phi)[source]#

The relation of satisfying assignments of a formula.

get_relation_symbols()[source]#

All relation symbols of the structure (‘U’ is the domain).

is_total_order()[source]#

Whether Lt is a strict total order — decidable, being a first-order question. Well-foundedness is not first-order, so it is not checkable here; it holds by construction.

Return type:

bool

autstr.ordinals.CantorForm#

Cantor coefficients keyed by their exponent, itself an ordinal below omega^n written as a coefficient tuple

Type:

a Python ordinal below omega^(omega^n)

alias of int | Mapping[int | Sequence[int], int]

class autstr.ordinals.TreeOrdinal(n=1, max_states=None)[source]#

Bases: TreeAutomaticPresentation

The ordinals below \(\omega^{\omega^n}\), under their natural order — the tree-automatic ordinals, which reach exactly this far.

Parameters:

  • n (int) – the exponent (n ≥ 1). TreeOrdinal(1) is \((\omega^\omega, <)\), the first ordinal past the word barrier.

  • max_states (Optional[int]) – optional cap on the subset determinizations inside projection.

The encoding. By Cantor normal form an ordinal below \(\omega^{\omega^n}\) is a finite sum \(\sum \omega^{\beta_i} c_i\) with exponents \(\beta_i < \omega^n\) — and an exponent below \(\omega^n\) is an n-tuple of naturals, exactly what Ordinal orders. Splitting off the leading coefficient of the exponent turns that into a recursion: an ordinal below \(\omega^{\omega^n}\) is a sequence of blocks indexed densely by that leading coefficient, each block an ordinal below \(\omega^{\omega^{n-1}}\), and at n = 0 a natural number. So the encoding is a left spine of blocks whose payloads hang right and are themselves spines, bottoming out in binary chains — the shape the tree engine reads natively.

Indexing the blocks densely by position is what makes the order easy: two ordinals are aligned by construction, so the comparison is decided at the deepest position where they differ, and a single three-state automaton (less, equal, greater) computes it bottom-up at every level of the nesting at once. Deeper is more significant everywhere — a deeper spine node is a higher exponent, a deeper bit is a higher power of two — and a position one ordinal has and the other lacks is a term the other is missing, so present beats absent.

Authored, not interpreted. For n = 1 the trees coincide with Skolem arithmetic’s, since both encode a finitely supported map from \(\mathbb{N}\) to \(\mathbb{N}\). The order is not an interpretation of it: permuting the primes is an automorphism of \((\mathbb{N}_{>0}, \cdot)\), so no ordering of the exponent positions is definable there, while the encoding fixes one. The comparison automaton is small enough that authoring it is the honest route.

Ordinals are written as maps from exponent to coefficient:

>>> W = TreeOrdinal(1)                    # ordinals below ω^ω
>>> a, b = W.symbolic().vars("a b")
>>> a.lt(b).evaluate().contains(a={2: 5}, b={3: 1})   # ω²·5 < ω³
True

An exponent is written as Ordinal writes one — an integer, or a tuple of coefficients in descending order, left-padded to length n — and a plain integer ordinal is the finite ordinal of that value.

SPINE = 's'#

spine node, tree root, the two bits, and padding

ROOT = 'o'#

spine node, tree root, the two bits, and padding

PAD = '*'#

spine node, tree root, the two bits, and padding

LETTERS = frozenset({'*', '0', '1', 'o', 's'})#
default_signature()[source]#

The strict order as .lt, equality as .eq, the successor as .succ, and ordinals written as Cantor maps.

is_total_order()[source]#

Whether Lt is a strict total order — decidable, being first-order. Well-foundedness is not first-order, so it is not checkable here; it holds by construction.

Return type:

bool

encode(value)[source]#

The tree encoding an ordinal, written as a map from exponent to coefficient (or as a plain integer, for a finite ordinal).

Return type:

Tree

Parameters:

value (int | Mapping[int | Sequence[int], int])

decode(tree)[source]#

The ordinal a tree encodes, as a map from exponent tuple to coefficient; the empty map is the ordinal zero.

Return type:

Dict[Tuple[int, ...], int]

Parameters:

tree (Tree)

autstr.powerset module#

The finite subsets of the naturals – the structure MSO0.

Finite subsets of \(\mathbb{N}\) under \(\subseteq\), with singletons, the successor on singletons and their order. A finite set is a \(\{0,1\}\)-word, position i set iff i is a member, so by Büchi’s theorem first-order logic over this structure is exactly monadic second-order logic over \((\mathbb{N}, <)\): the definable sets of naturals are precisely the regular ones.

>>> M = MSO0().symbolic()
>>> x, y = M.vars("x y")
>>> ({0, 2}, {0, 1, 2}) in x.subset(y)
True

That correspondence is why the structure is called MSO0, and why quantifying over sets here costs no more than quantifying over elements elsewhere.

class autstr.powerset.MSO0[source]#

Bases: CompiledPresentation

The finite subsets of \(\mathbb{N}\) under \(\subseteq\), with singletons, successor and the order on singletons.

>>> M = MSO0()
>>> x, y = M.symbolic().vars("x y")
>>> ({0, 2} , {0, 1, 2}) in x.subset(y)
True
>>> (x + y).eq({0, 1}).check()          # union
True

By Büchi’s theorem, first-order logic over this structure is exactly monadic second-order logic over \((\mathbb{N}, <)\), so the definable sets are precisely the regular ones.

Parameters:

automata – dictionary containing the automata that recognize the domain and the relations of the structure. ‘U’ is reserved key for the universe. All other keys are assumed to recognize relations over L(U)^k. They can be addressed by their keys in first-order queries.

PADDING = '*'#

a set as a bitmask, position i set iff i is a member. The universe rejects trailing zeros, so the encoding is the CANONICAL one: {0} is 1, {0, 2} is 101, and the empty set is the empty word.

static encode(s)[source]#

The word encoding a finite set of naturals: position i carries 1 iff i is a member, up to the largest one.

Return type:

List[str]

static decode(word)[source]#

The set encoded by a word, ignoring padding.

Return type:

set

default_signature()[source]#

Union as +, intersection as *, difference as binary -, and the relations of the structure as methods, with sets written as Python sets.

autstr.presentations module#

class autstr.presentations.AutomaticPresentationSerializer[source]#

Bases: object

MAGIC = b'APRS'#
VERSION = 1#
HEADER_FORMAT = '4sB3sII'#
HEADER_SIZE = 16#
classmethod serialize(presentation, filename)[source]#

Serialize AutomaticPresentation to binary file

Return type:

None

Parameters:

filename (str)

classmethod deserialize(filename)[source]#

Deserialize AutomaticPresentation from binary file

Parameters:

filename (str)

class autstr.presentations.DeferredRelations[source]#

Bases: object

Relations declared up front and built on first use.

Equality is definable in most presentations here – from Leq in a lattice, from Subset on set-valued elements, from the operation in a group – but defining it costs an automaton construction that most queries never need, and for the wider graph classes that construction is expensive. So such a relation is registered rather than built, and materializes when something asks for it.

materialize() forces the construction, which is what you want before pickling or otherwise reusing a structure, and every constructor that registers deferred relations takes an eager flag for the same purpose.

Subclasses say where their relations live (_relations) and how to install one (_install_relation). A definition is either a formula string over the existing signature or a callable returning an automaton.

get_relation_symbols()[source]#

All relation symbols, including any not yet built.

Return type:

List[str]

relation(name)[source]#

The automaton for name, building it if it was deferred.

Parameters:

name (str)

materialize(*names)[source]#

Build the named deferred relations now, or all of them. Returns self, so it chains onto a constructor.

Parameters:

names (str)

class autstr.presentations.AutomaticPresentation(automata, padding_symbol='*', enforce_consistency=True)[source]#

Bases: DeferredRelations

A presentation of a possibly infinite structure by finite state machines.

Parameters:

  • automata (Dict[str, SparseDFA]) – dictionary containing the automata that recognize the domain and the relations of the structure. ‘U’ is reserved key for the universe. All other keys are assumed to recognize relations over L(U)^k. They can be addressed by their keys in first-order queries.

  • padding_symbol (any | None)

  • enforce_consistency (bool)

automatic_presentation_to_file(filename)[source]#
Return type:

None

Parameters:

filename (str)

classmethod automatic_presentation_from_file(filename)[source]#
Parameters:

filename (str)

symbolic(signature=None)[source]#

A symbolic interface to this structure: variables, relation and function symbols that build first-order expressions with Python operators instead of formula strings.

Parameters:

signature – declared functions, operators and element codec. Relation arities are read from the automata, so a structure with no functions needs no signature at all.

Returns:

a autstr.symbolic.SymbolicContext.

default_signature()[source]#

The signature symbolic() uses when none is given, or None for a structure that declares no operators and is addressed through its relation symbols. Structures that know their own vocabulary override this; see autstr.symbolic.operation_signature.

update(**kwargs)[source]#
Return type:

None

check(phi)[source]#

Checks if a given first-order formula holds on the presented structure. Free variables are assumed be implicitly existentially quantified.

Parameters:

phi (Expression | str) – the first order formula

Return type:

bool

Returns:

the truth value of the formula, if the formula where all free variables are existentially quantified.

evaluate(phi, updates=None, prepared_updates=None)[source]#

Evaluates a given first-order query on the presented structure. Returns a presentation of the set of all satisfying assignments.

Parameters:

  • phi (Union[str, Expression]) – the first order formula.

  • updates (Optional[Dict[str, Union[SparseDFA, str]]]) – Temporarily update the relations for the evaluation

  • prepared_updates (Optional[Dict[str, SparseDFA]]) – like updates, for automata already known to be restricted to the universe – results this presentation produced itself. They are only re-padded, skipping the domain intersection that _prepare_automaton would otherwise redo on every tape.

Return type:

SparseDFA

Returns:

The truth value of the formula, if the formula where all free variables are existentially quantified.

class autstr.presentations.CompiledPresentation[source]#

Bases: AutomaticPresentation

A presentation whose automata are compiled by a builder function.

Subclasses set _BUILD to that function and declare their vocabulary in default_signature, so the structure can be constructed with no arguments and addressed symbolically with no setup. The builder’s automata are adopted as they are rather than passed to AutomaticPresentation.__init__, which would restrict and pad relations the builder already restricted and padded.

Parameters:

automata – dictionary containing the automata that recognize the domain and the relations of the structure. ‘U’ is reserved key for the universe. All other keys are assumed to recognize relations over L(U)^k. They can be addressed by their keys in first-order queries.

autstr.sparse_automata module#

class autstr.sparse_automata.SparseDFASerializer[source]#

Bases: object

VERSION = 3#
HEADER_FORMAT = '4sB3sII'#
HEADER_SIZE = 16#
METADATA_FORMAT = 'IIIII'#
METADATA_SIZE = 20#
classmethod serialize(dfa, filename)[source]#

Serialize SparseDFA to binary file

Return type:

None

Parameters:
classmethod deserialize(filename)[source]#

Deserialize SparseDFA from binary file

Return type:

SparseDFA

Parameters:

filename (str)

classmethod to_bytes(dfa)[source]#

Serialize SparseDFA to bytes object

Return type:

bytes

Parameters:

dfa (SparseDFA)

classmethod from_bytes(data)[source]#

Deserialize SparseDFA from bytes object

Return type:

SparseDFA

Parameters:

data (bytes)

class autstr.sparse_automata.SparseDFA(num_states, default_states=(), exception_symbols=(), exception_states=(), is_accepting=(), start_state=0, symbol_arity=1, base_alphabet=None, nodes=None)[source]#

Bases: object

Deterministic automaton over a convolution alphabet.

Each state carries one shared multi-terminal BDD over the binary digits of the symbol (see autstr.mtbdd) instead of a default target plus a row of symbol -> target exceptions. 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 — which is what the pipeline used to spend its memory on.

The constructor still accepts the flat form, and default_states, exception_symbols and exception_states remain available as decoded views for inspection, rendering and serialization of narrow automata: the default of a decoded state is its most common target, so the view is the sparsest one (what sparsify used to compute).

Parameters:

  • num_states (int)

  • start_state (int)

  • symbol_arity (int)

  • base_alphabet (Set[int] | None)

property num_symbols: int#
property num_nodes: int#

Distinct diagram nodes carrying this automaton’s transitions.

encode_symbol(symbol_tuple)[source]#
Return type:

int

Parameters:

symbol_tuple (Tuple[int])

decode_symbol(symbol_enc)[source]#
Return type:

Tuple[int]

Parameters:

symbol_enc (int)

dense_next(max_entries=16777216)[source]#

The full (num_states, num_symbols) next-state table. Only for automata narrow enough to enumerate; the pipeline never calls it.

Return type:

ndarray

Parameters:

max_entries (int)

property default_states: ndarray#
property exception_symbols: ndarray#
property exception_states: ndarray#
property max_exceptions: int#
transition(state, symbol)[source]#
Return type:

int

Parameters:
compute(word)[source]#

Final state after reading the word (encoded symbols).

A word is a sequential dependency chain, so this cannot be vectorized. Narrow automata run off the dense table (one list index per symbol); wide ones descend the diagram, memoizing each (state, symbol) step.

Return type:

int

Parameters:

word (ndarray)

accepts(word)[source]#
Return type:

bool

accepts_batch(words)[source]#

Batched acceptance check for many equal-length words at once.

Parameters:

words – either an already-encoded integer array of shape (batch, length), or a sequence of equal-length words of symbol tuples (encoded like accepts()).

Return type:

ndarray

Returns:

boolean array of shape (batch,).

Uses JAX (jit + scan, GPU if available) when installed and the dense next-state table fits; otherwise a vectorized numpy fallback (over the table, or over the diagrams when the alphabet is too wide to enumerate).

successors(state)[source]#

All successor states of a state — the terminals of its diagram.

Return type:

ndarray

Parameters:

state (int)

reverse_transition(state, symbol)[source]#

The states that transition to state on symbol.

Return type:

ndarray

Parameters:
is_empty()[source]#
Return type:

bool

is_finite()[source]#
Return type:

bool

complement()[source]#

Flip acceptance — the transition diagrams are untouched.

Return type:

SparseDFA

intersection(other)[source]#
Return type:

SparseDFA

Parameters:

other (SparseDFA)

union(other)[source]#
Return type:

SparseDFA

Parameters:

other (SparseDFA)

alphabet_projection(projection_map)[source]#

Relabel symbols by projection_map, which may merge them and thus make the automaton nondeterministic (inspection-scale: it decodes).

Return type:

SparseNFA

Parameters:

projection_map (ndarray)

intersect_subtapes(other, tapes)[source]#

{x in L(self) | x[tapes] in L(other)}.

Expressed as a product with other cylindrified onto tapes, so no symbol is enumerated.

Return type:

SparseDFA

Parameters:
regular_right_quotient(other)[source]#

{u | uv in L(self) for some v in L(other)}: a state of self is accepting iff, paired with other’s start state, it can synchronously reach a pair of accepting states.

Return type:

SparseDFA

Parameters:

other (SparseDFA)

fill_defaults()[source]#

No-op: a diagram has no default slot to fill.

Return type:

SparseDFA

sparsify()[source]#

No-op: the diagram representation is already the sparse one (its decoded view picks each state’s most common target as the default).

Return type:

SparseDFA

minimize()[source]#

Moore partition refinement over the transition diagrams.

Relabelling a state’s diagram by the current partition yields the function symbol -> class of target; hash-consing means two states induce the same function exactly when the relabelled diagrams are the same node, so a refinement round is one apply1 per state.

Return type:

SparseDFA

show_diagram(filename='automaton', format='png', view=False)[source]#

Visualize the automaton using Graphviz, showing both default and exception transitions. This version ensures all transitions are properly displayed.

Return type:

Digraph

Parameters:
sparse_dfa_to_file(filename)[source]#
Return type:

None

Parameters:

filename (str)

classmethod sparse_dfa_from_file(filename)[source]#
Return type:

SparseDFA

Parameters:

filename (str)

autstr.sparse_automata.recode(dfa, new_alphabet, letter_map=None)[source]#

Re-express an automaton over a different base alphabet.

letter_map sends each of the automaton’s letters to a letter of new_alphabet (injectively; the identity by default). Letters of the new alphabet outside the image are rejected: a fresh dead state absorbs them, which is what the closure constructions want – a factor of a disjoint union must reject the other side’s letters, and a factor of a direct product must reject the tag letters.

The rewrite happens on the diagrams, one pass over the nodes, so widening the alphabet does not rebuild any transition table.

Return type:

SparseDFA

Parameters:

dfa (SparseDFA)

autstr.sparse_automata.reduce_set_nfa(store, nodes, subsets, is_accepting, start, arity, m, bits)[source]#

Shrink a set-valued NFA before determinizing it.

nodes[q] is a diagram from symbols to sets of successors (terminals are indices into subsets, whose entries are bitsets of states). Two reductions apply, both language-preserving and both cheap next to the subset construction that follows:

  • states that reach no accepting state, and states unreachable from start, are dropped: they enlarge every subset that contains them without ever affecting acceptance;

  • the remainder is quotiented by forward bisimulation — q and q’ merge when they agree on acceptance and, on every symbol, their successor sets have the same classes. Relabelling a state’s diagram so each terminal becomes the class bitset of its target set turns the state’s signature into a hash-consed node id, so a refinement round is one apply1 per state.

Determinizing the quotient explores subsets of classes, which are images of the subsets of states, so the state count can only shrink.

Returns:

(nodes, subsets, subset_ids, is_accepting, start) over the classes, or None when the language is empty.

Parameters:
class autstr.sparse_automata.SparseNFA(num_states, base_state=(), exception_symbols=(), exception_states=(), is_accepting=(), start_state=0, symbol_arity=1, base_alphabet=None, nodes=None, subsets=None)[source]#

Bases: object

Nondeterministic automaton whose states carry a diagram from symbols to sets of targets (terminals index self.subsets).

The flat constructor keeps the historical shape — a base target per state plus symbol -> target exception rows, where the exceptions of a symbol override the base rather than adding to it. That is the semantics determinize always implemented; running the NFA directly now follows the same reading.

Parameters:

  • num_states (int)

  • start_state (int)

  • symbol_arity (int)

  • base_alphabet (Set[int] | None)

subset_id(mask)[source]#

Intern a set of states, held as an integer bitset.

Return type:

int

Parameters:

mask (int)

compute(word)[source]#

Returns the set of states after processing the word

Return type:

ndarray

Parameters:

word (ndarray)

accepts(word)[source]#
Return type:

bool

Parameters:

word (ndarray)

determinize()[source]#

Subset construction on the diagrams: a subset’s transition is the union of its members’ diagrams, and the union of two set-valued diagrams is one apply. No symbol is enumerated.

The NFA is first pruned and quotiented by forward bisimulation (see reduce_set_nfa), which is cheap and shrinks the subset space.

Return type:

SparseDFA

show_diagram(filename='nfa', format='png', view=False)[source]#

Visualizes the NFA using Graphviz

Return type:

Digraph

Parameters:

autstr.sparse_tree_automata module#

Sparse bottom-up tree automata.

The tree analog of autstr.sparse_automata: deterministic bottom-up automata over binary trees (general trees embed via the first-child/next-sibling encoding), stored sparsely and processed with batched numpy throughout.

States. Real states are 0..num_states-1; the virtual absent state BOT = num_states represents a missing child, so a single transition table covers leaves (both children absent), unary and binary nodes:

state(node) = delta(state(left) or BOT, state(right) or BOT, label(node)).

Sparsity. Transitions are stored as a sorted table from the child pair (left, right) to a shared multi-terminal BDD over the binary digits of the symbol (see autstr.mtbdd); pairs absent from the table map every symbol to the global default_state. Nothing in the pipeline ever enumerates the convolution alphabet: a symbol is a variable assignment, so a transition that ignores a tape simply does not test that tape’s variables. Boolean combinations are pairwise apply on the diagrams, complementation relabels acceptance and touches no diagram at all, and hash-consing makes two states with the same transition function share one node.

class autstr.sparse_tree_automata.Tree(label, left=None, right=None)[source]#

Bases: object

An immutable labelled binary tree (convenience representation).

Parameters:

  • left (Tree | None)

  • right (Tree | None)

label#
left#
right#
size()[source]#
Return type:

int

autstr.sparse_tree_automata.tree_to_arrays(tree, base_alphabet, arity=1)[source]#

Convert a Tree with tuple/symbol labels to the post-order array format (labels encoded as integers over base_alphabet^arity).

Parameters:
autstr.sparse_tree_automata.convolve_trees(trees, base_alphabet, padding_symbol)[source]#

Overlay k trees into one tree over the tuple alphabet: the domain is the union of the domains, absent positions are padded.

Return type:

Tree

Parameters:
class autstr.sparse_tree_automata.SparseTreeAutomaton(num_states, default_state, exc_left=(), exc_right=(), exc_symbol=(), exc_target=(), is_accepting=(), symbol_arity=1, base_alphabet=None, pd_left=(), pd_right=(), pd_target=(), pair_keys=None, pair_nodes=None)[source]#

Bases: object

Deterministic bottom-up tree automaton with MTBDD transitions.

The constructor takes the transition function in the flat form that is convenient to write down by hand — a global default, optional per-pair defaults, and (left, right, symbol) -> target exceptions — and compiles it into one decision diagram per child pair.

Parameters:

  • num_states (int) – number of real states (0..num_states-1); the virtual absent-child state is BOT = num_states.

  • default_state (int) – target of every transition not listed below.

  • exc_target (exc_left, exc_right, exc_symbol,) – parallel arrays of exception transitions delta(exc_left, exc_right, exc_symbol) = exc_target. Children may be BOT; targets are real states.

  • is_accepting – boolean array over the real states (acceptance is checked at the root).

  • pd_target (pd_left, pd_right,) – parallel arrays of pair defaults delta(pd_left, pd_right, *) = pd_target for symbols without an exception. Pairs not listed fall back to the global default.

  • pair_nodes (pair_keys,) – the compiled form (sorted packed pair keys and their diagram roots); passed by the pipeline instead of the flat arrays.

  • symbol_arity (int)

  • base_alphabet (Set | None)

property BOT: int#
property num_symbols: int#
property num_nodes: int#

Distinct diagram nodes carrying this automaton’s transitions.

pair_node(left, right)[source]#

Batched lookup of the diagram of each child pair.

Return type:

ndarray

transitions(left, right, symbol)[source]#

Batched transition lookup: find each pair’s diagram, then descend it along the symbol’s digits.

Return type:

ndarray

dense_delta(max_entries=10000000)[source]#

The full transition table (BOT+1, BOT+1, num_symbols). For inspection and for reference oracles on small automata.

Return type:

ndarray

Parameters:

max_entries (int)

exceptions(max_entries=10000000)[source]#

The transitions that differ from the global default, as flat (left, right, symbol, target) arrays (inspection only).

Parameters:

max_entries (int)

run(labels, lefts, rights)[source]#

State at the root of a post-order array tree.

Adaptive evaluation: children resolve before parents in post-order, so each vectorized round computes every node whose children are already known — one round per tree level, ideal for bushy trees. Long unary chains (e.g. string-like spines) are inherently sequential, so when a round stops being productive the remaining nodes are finished by a scalar post-order sweep instead of degenerating to O(n^2).

Return type:

int

accepts(*trees)[source]#

Does the automaton accept the convolution of the given trees? Accepts Tree objects (one per tape) or a single pre-encoded array tree given as the tuple (labels, lefts, rights).

Return type:

bool

complement()[source]#

Flip acceptance — the transition diagrams are untouched.

Return type:

SparseTreeAutomaton

intersection(other)[source]#
Return type:

SparseTreeAutomaton

union(other)[source]#
Return type:

SparseTreeAutomaton

reachable_states()[source]#

Boolean mask of states reachable by some tree (bottom-up fixpoint). The targets of an available child pair are the terminals of its diagram; the global default joins as soon as some available pair is absent from the table.

Return type:

ndarray

is_empty()[source]#
Return type:

bool

co_reachable_states(available=None)[source]#

Boolean mask of states that can occur in an accepting run: a state is co-reachable if it is accepting (as the root) or it is a child in some transition whose target is co-reachable and whose sibling subtree exists. The top-down companion to reachable_states.

Return type:

ndarray

Parameters:

available (ndarray | None)

is_finite()[source]#

Whether the automaton accepts finitely many trees.

A state that can occur strictly below itself pumps: the context between the two occurrences can be repeated without bound. So the language is infinite exactly when the “child of” graph, restricted to states that are both reachable and co-reachable, has a cycle.

Return type:

bool

class autstr.sparse_tree_automata.SparseTreeAutomatonSerializer[source]#

Bases: object

Binary serialization for SparseTreeAutomaton.

The tree counterpart of autstr.sparse_automata.SparseDFASerializer, and the same payload idea: the compiled form is a sorted table of child pairs with one diagram root each, so storing it is storing the pair keys plus the sub-DAG below their roots.

MAGIC = b'STAU'#
VERSION = 1#
HEADER_FORMAT = '4sB3sII'#
HEADER_SIZE = 16#
METADATA_FORMAT = 'IIIIII'#

num_states, num_nodes, num_pairs, default_state, symbol_arity, alphabet

METADATA_SIZE = 24#
classmethod serialize(automaton, filename)[source]#
Return type:

None

Parameters:
classmethod deserialize(filename)[source]#
Return type:

SparseTreeAutomaton

Parameters:

filename (str)

classmethod to_bytes(automaton)[source]#
Return type:

bytes

Parameters:

automaton (SparseTreeAutomaton)

classmethod from_bytes(data)[source]#
Return type:

SparseTreeAutomaton

Parameters:

data (bytes)

autstr.tree_algebra module#

The countable atomless boolean algebra, as a tree-automatic structure.

There is exactly one countable atomless boolean algebra up to isomorphism — Cantor’s back-and-forth argument again — and it is the infinite counterpart of the autstr.algebra.FiniteBooleanAlgebras class, carrying the same signature Leq, Meet, Join, Compl, Atom. The same formula runs against both, and the one that separates them is the definition of the name: over a finite algebra exists x. Atom(x) is true, and here it is false.

Elements are clopen subsets of Cantor space. A clopen subset of \(2^\omega\) is a finite union of cylinders, so it is decided by finitely many bits of a point — that is, by a finite binary decision tree with leaves labelled in or out. Making the tree reduced (no split whose two sides are the same constant) makes the encoding a bijection, which matters here: a non-canonical encoding would need a quotient, and quotients are exactly what the tree engine cannot yet supply (see autstr.interpretations).

One authored automaton. Reduction is what makes the order cheap. In a reduced tree a subtree is constant exactly when it is a leaf, so at any position the comparison is already decided unless both sides split there:

x is 0 here            -> fine, nothing of x to contain
y is 1 here            -> fine, y contains everything
x is 1, y is not       -> y misses a point of x
y is 0, x is not       -> x has a point y misses
both split             -> recurse

Nothing below a leaf is ever consulted, so Leq is a two-state bottom-up automaton. Everything else — Meet, Join, Compl, Atom, and equality — is first-order over it and is defined rather than authored, built the first time a query asks for it.

>>> B = AtomlessBooleanAlgebra()
>>> x, y = B.symbolic().vars("x y")
>>> (x * y).eq({'00'}).check()          # some meet is the cylinder 00
True
>>> B.check('exists x.(Atom(x))')       # atomless, by construction
False

A clopen set is written as the set of binary strings whose cylinders it contains: {'0', '10'} is everything starting 0 or 10, set() is empty and {''} is everything. Any covering set may be given — {'0','1'} and {''} denote the same element — and decode returns the canonical one.

autstr.tree_algebra.Clopen#

a clopen set, as the binary strings whose cylinders it contains

alias of Iterable[str]

class autstr.tree_algebra.AtomlessBooleanAlgebra(max_states=None)[source]#

Bases: TreeAutomaticPresentation

The unique countable atomless boolean algebra.

Parameters:

max_states (Optional[int]) – optional cap on the subset determinizations inside projection.

Elements are the clopen subsets of Cantor space, encoded as reduced binary decision trees: '0' and '1' label leaves that are out and in, and 'n' labels a split on the next bit of a point.

SPLIT = 'n'#

split, out-leaf, in-leaf, padding

OUT = '0'#

split, out-leaf, in-leaf, padding

IN = '1'#

split, out-leaf, in-leaf, padding

PAD = '*'#

split, out-leaf, in-leaf, padding

LETTERS = frozenset({'*', '0', '1', 'n'})#
default_signature()[source]#

Meet as *, join as +, complement as unary -, the order as .leq and equality as .eq.

The lattice operations are terms, not connectives: &, | and ~ already mean conjunction, disjunction and negation of formulas, so binding them here would make x & y ambiguous — the same reason Büchi arithmetic spells its divisibility relation divided_by_power.

is_atomless()[source]#

Whether every non-empty element strictly contains a non-empty one — decidable, being first-order, and the property that pins the algebra down to isomorphism.

Return type:

bool

encode(clopen)[source]#

The reduced decision tree of a clopen set, written as the binary strings whose cylinders it contains. Any covering set is accepted and canonicalized.

Return type:

Tree

Parameters:

clopen (Iterable[str])

decode(tree)[source]#

The clopen set a tree encodes, as its canonical cylinders.

Return type:

FrozenSet[str]

Parameters:

tree (Tree)

autstr.tree_arithmetic module#

Skolem arithmetic: the multiplicative monoid of the naturals.

\((\mathbb{N}_{>0}, \cdot)\) is not string-automatic, but it is tree-automatic, and the prime factorization is why: multiplicatively the structure is the direct sum of countably many copies of \((\mathbb{N}, +)\), one per prime, and a tree bundles the finitely many nonzero summands. So multiplication becomes addition of exponents, carried out in parallel across the primes.

>>> S = skolem_arithmetic().symbolic()
>>> x, y = S.vars("x y")
>>> (6, 35, 210) in (x * y).eq(S.vars("z")[0])
True

This is the tree-engine counterpart of autstr.arithmetic, whose additive structures the string engine can present directly.

class autstr.tree_arithmetic.SkolemArithmetic(max_states=None)[source]#

Bases: TreeAutomaticPresentation

(N_{>0}, ·, =) presented by tree automata.

Encoding: n = prod_i p_i^{e_i} is a left spine of ‘p’-labelled nodes, one per prime index up to the largest with e_i > 0 (so no trailing zero exponents); spine node i carries e_i as a right-hanging chain of bits with the least significant bit at the top and the most significant (always ‘1’) at the bottom; e_i = 0 is an absent chain. n = 1 is the single node ‘p’.

Relations: M(x, y, z) iff x·y = z, and equality E. Multiplication is positionwise addition of the exponent vectors, so its automaton runs a binary addition automaton independently on every exponent branch of the 3-tape convolution; a single further state rides down the spine and checks that every branch accepted.

Parameters:

max_states (int | None)

LETTERS = frozenset({'*', '0', '1', 'p'})#
PAD = '*'#
default_signature()[source]#

Multiplication as *, equality as .eq, and positive integers as elements – so (x * y).eq(12) says what it reads as.

classmethod encode(n)[source]#
Return type:

Tree

Parameters:

n (int)

classmethod decode(tree)[source]#
Return type:

int

Parameters:

tree (Tree)

autstr.tree_arithmetic.skolem_arithmetic(max_states=None)[source]#
Return type:

SkolemArithmetic

Parameters:

max_states (int | None)

autstr.tree_graphs module#

Graphs of bounded tree-width and bounded clique-width as uniformly tree-automatic classes.

The class presents graphs over sets of vertices (as in MSO0), so first-order logic over the presentation is monadic second-order logic over the graph — evaluating an MSO query once yields a tree automaton that decides it on every member graph in linear time (Courcelle’s theorem).

Practical envelope. Transitions are decision diagrams over the symbol’s digits (autstr.mtbdd), so the width of the convolution alphabet no longer drives the cost: a query with several free tapes is as cheap as the digits its transitions actually test. What remains is the subset explosion of determinizing an existential quantifier. Element (path) quantifiers project onto small subset automata and are cheap; set quantifiers (MSO proper) determinize over subsets of the intermediate automaton’s states, and each such subset carries its own diagram. Two-colourability compiles at w = 1; deeper set-quantifier nesting is bounded by memory, not by the alphabet. Deciding a compiled automaton on a graph is always linear and fast — compilation is the bottleneck.

The signature is shared with the string graph classes:

Sing(x) x is a singleton Subset(x,y) x is a subset of y E(x,y) x = {u}, y = {v} and u,v are adjacent

Tree-width <= w (TreeWidthClass): the advice is a binary tree with one node per vertex, labelled (register in {0..w}, adjacency profile), plus a structural letter ‘n’ that introduces no vertex (used to route branch points). Introducing a vertex at register r replaces the nearest occupant of r above; the profile lists registers of the vertex’s neighbors among the current occupants on its root path. The live registers along any path form bags of size <= w+1 — exactly a tree decomposition of width w — and every graph of tree-width <= w arises this way from a nice decomposition.

Clique-width <= k (CliqueWidthClass): the advice is a k-expression – leaves create a labelled vertex, u takes a disjoint union, r{i}{j} relabels, and e{i}{j} joins every label-i vertex to every label-j vertex. The vertices are the leaves. Adjacency is much cheaper to recognize than for tree-width: two vertices are joined exactly when some e{i}{j} node sees one holding label i and the other label j, so the automaton need only carry each marked vertex’s current label. The advice alphabet is correspondingly small, and MSO queries compile far faster – two-colourability is a 9-state automaton at k = 2, against a minute at tree-width 1.

Rank-width <= r (RankWidthClass): the advice is a rank decomposition (a binary tree whose leaves are the vertices) annotated with the GF(2) factorization data of its cuts – the graph analog of the bounded-rank-width group classes, compiled with the same chain_ring linear algebra at p = 2, d = 1. Each node carries a basis-change matrix per child and each binary node the bilinear form of its sibling block; adjacency of x and y is w_y^T Q w_x at the node where their subtrees meet, so the E automaton only carries the marked vertices’ r-bit interface vectors. Rank-width lower-bounds clique-width (rw <= cw <= 2^{rw+1} - 1) and is bounded on dense graphs where tree-width is not (cliques have rank-width 1).

Vertex sets are encoded synchronously over the advice: the element tree is the union of the root paths to the set’s members, labelled ‘1’ on members and ‘0’ on the way (the empty set is the single node ‘0’). For tree-width every node is a vertex; for clique-width and rank-width only the leaves are. TreeWidthGraph, CliqueWidthGraph and RankWidthGraph encapsulate single graphs and convert to networkx.

class autstr.tree_graphs.TreeWidthGraph(letters, nodes=None)[source]#

Bases: object

A graph in its tree representation: a binary tree with one (register, profile) letter per vertex (and ‘n’ for structural nodes). A vertex’s profile lists the registers of its already-introduced neighbors, resolved to the nearest writer above on the root path.

Parameters:
property num_nodes: int#
property width: int#

Maximal register index (>= tree-width of the graph).

edges()[source]#

Edge list (node names) decoded from the letters.

Return type:

List[Tuple]

encode_set(subset)[source]#

Encode a set of nodes as a marked tree over the advice shape.

Return type:

Tree

to_networkx()[source]#

Convert back to a networkx graph (node names preserved).

classmethod from_networkx(graph, decomposition=None)[source]#

Build the tree representation from a networkx graph.

Parameters:

  • graph – undirected networkx graph (at least one vertex).

  • decomposition – optional tree decomposition as a networkx tree whose nodes are frozensets of vertices (bags). If omitted, the min-fill-in heuristic computes one (valid, possibly wider than the tree-width).

Return type:

TreeWidthGraph

class autstr.tree_graphs.TreeWidthClass(w, max_states=None)[source]#

Bases: SymbolicClassWrapper

The uniformly tree-automatic class of graphs of tree-width <= w, presented over set-valued elements (MSO0 style).

Parameters:

  • w (int)

  • max_states (int | None)

GRAPH = None#

elements are vertex sets and E is the edge relation, not equality

EQUALITY = 'Subset(x,y) and Subset(y,x)'#

extensional equality of sets

advice(graph)[source]#

The advice tree of a graph (its letters as alphabet symbols).

Return type:

Tree

Parameters:

graph (TreeWidthGraph | Tree)

evaluate(phi)[source]#

Evaluate an MSO query over the class; see UniformlyTreeAutomaticClass.evaluate. Variables range over vertex sets.

check(phi, graph, **sets)[source]#

Model check an MSO query against a single graph.

Parameters:

  • phi – formula over Sing/Subset/E; free variables can be assigned via sets (name = set of nodes), unassigned ones are quantified existentially.

  • graph (Union[TreeWidthGraph, Tree]) – a TreeWidthGraph (or a raw advice tree).

  • sets – assignments for free variables, as sets of nodes.

Return type:

bool

get_structure(graph)[source]#

The MSO0-style tree-automatic presentation of a single graph.

Return type:

TreeAutomaticPresentation

class autstr.tree_graphs.CliqueWidthGraph(expression, k)[source]#

Bases: object

A graph given by a k-expression, held as a binary tree.

The expression’s leaves create vertices, so the vertices are the leaves, numbered left to right. Inner nodes are the three clique-width operations:

u disjoint union of the two children r{i}{j} relabel every label-i vertex to label j e{i}{j} join: add every edge between label i and label j

u is binary; r and e are unary (left child only).

Parameters:
vertices: List[int]#
edges: Set[frozenset]#
encode_set(subset)[source]#

The set as a tree of marks: ‘1’ at the chosen leaves, ‘0’ on the paths above them, absent elsewhere. The empty set is a single ‘0’.

Return type:

Tree

to_networkx()[source]#
classmethod clique(n)[source]#

K_n, clique-width 2: absorb each new vertex into label 0.

Return type:

CliqueWidthGraph

Parameters:

n (int)

classmethod complete_bipartite(left, right)[source]#

K_{left,right}, clique-width 2: join the two colour classes once.

Return type:

CliqueWidthGraph

Parameters:
classmethod path(n)[source]#

P_n, clique-width 3: label 0 is the growing end, 1 the new vertex, 2 the settled interior.

Return type:

CliqueWidthGraph

Parameters:

n (int)

classmethod cycle(n)[source]#

C_n, clique-width 4: as the path, but the first vertex keeps label 3 so the closing edge can be added at the root.

Return type:

CliqueWidthGraph

Parameters:

n (int)

class autstr.tree_graphs.CliqueWidthClass(k, max_states=None)[source]#

Bases: SymbolicClassWrapper

The uniformly tree-automatic class of graphs of clique-width <= k, presented over set-valued elements (MSO0 style).

The advice is a k-expression (see CliqueWidthGraph); the vertices are its leaves, and a vertex set is encoded synchronously as the union of the root paths to its members, ‘1’ on members and ‘0’ on the way.

Adjacency is far simpler here than for tree-width: two vertices are joined exactly when some e{i}{j} node sees one of them holding label i and the other label j. A bottom-up automaton therefore only has to remember the current label of each marked vertex, and whether the join has happened.

Parameters:

  • k (int)

  • max_states (int | None)

GRAPH = None#

elements are vertex sets and E is the edge relation, not equality

EQUALITY = 'Subset(x,y) and Subset(y,x)'#

extensional equality of sets

advice(graph)[source]#

The advice tree of a graph (its k-expression).

Return type:

Tree

Parameters:

graph (CliqueWidthGraph | Tree)

evaluate(phi)[source]#

Evaluate an MSO query over the class; variables range over vertex sets. See UniformlyTreeAutomaticClass.evaluate.

check(phi, graph, **sets)[source]#

Model check an MSO query against a single graph.

Return type:

bool

Parameters:

graph (CliqueWidthGraph | Tree)

get_structure(graph)[source]#

The MSO0-style tree-automatic presentation of a single graph.

Return type:

TreeAutomaticPresentation

class autstr.tree_graphs.RankWidthGraph(shape, edges)[source]#

Bases: object

A graph with a rank decomposition: a binary layout tree whose leaves are the vertices (numbered left to right), plus an edge set.

The width of the decomposition is the maximum, over all subtrees S, of the GF(2) rank of the bipartite adjacency matrix between the leaves inside S and the leaves outside (the cut-rank); the rank-width of the graph is the minimum over decompositions. This is the graph analog of the module cut-rank of the bounded-rank-width group classes, and the class compiler below reuses the same linear algebra (autstr.chain_ring at p = 2, d = 1). Unary layout nodes are allowed (they do not change the cuts).

Parameters:

shape (Tree)

edges: Set[frozenset]#
span: Dict[int, Tuple[int, int]]#
cut_matrix(node)[source]#

The bipartite adjacency block of the node’s cut: rows the outside vertices, columns the inside leaves (left-to-right).

Return type:

ndarray

Parameters:

node (Tree)

property width: int#

the maximum GF(2) cut-rank over all proper subtrees.

Type:

The rank-width of this decomposition

encode_set(subset)[source]#

The set as a tree of marks: ‘1’ at the chosen leaves, ‘0’ on the paths above them, absent elsewhere. The empty set is a single ‘0’.

Return type:

Tree

encode_set_padded(subset, pad='*')[source]#

The set as a mark tree of the decomposition’s exact shape, pad outside the trimmed domain – what the implicit evaluator needs (it runs all tapes synchronously over the advice shape).

Return type:

Tree

Parameters:

pad (str)

decode_set(tree)[source]#

The vertex set of a mark tree (trimmed or full-shape/padded).

Return type:

Set[int]

Parameters:

tree (Tree)

to_networkx()[source]#
static caterpillar(n)[source]#

The linear (caterpillar) decomposition: leaves 0..n-1 hang left to right off a left-deep spine.

Return type:

Tree

Parameters:

n (int)

classmethod clique(n)[source]#

K_n: every crossing block is all ones – rank-width 1 on any decomposition.

Return type:

RankWidthGraph

Parameters:

n (int)

classmethod path(n)[source]#

P_n in path order: one edge crosses each caterpillar cut – rank-width 1.

Return type:

RankWidthGraph

Parameters:

n (int)

classmethod cycle(n)[source]#

C_n: two edges cross the middle caterpillar cuts – width 2 on this decomposition (and rank-width 2 for n >= 5).

Return type:

RankWidthGraph

Parameters:

n (int)

classmethod complete_bipartite(left, right)[source]#

K_{left,right}, one part then the other: identical rows on every cut – rank-width 1.

Return type:

RankWidthGraph

Parameters:
class autstr.tree_graphs.RankWidthClass(r, max_states=None)[source]#

Bases: SymbolicClassWrapper

The uniformly tree-automatic class of graphs of rank-width <= r, presented over set-valued elements (MSO0 style: Sing, Subset, E).

The advice is a rank decomposition annotated with the GF(2) factorization data of its cuts, exactly as the bounded-rank-width group classes annotate theirs: each node carries a basis-change matrix per child (w <- T w) and each binary node the bilinear form Q of its sibling block, so that two vertices x in the left and y in the right subtree are adjacent iff w_y^T Q w_x over F_2, where w is the vertex’s interface vector (its column in the saturated basis of the cut, composed through the T maps). The letters are

leaf: ‘a’ + w (r bits) – the vertex’s interface vector unary: ‘b’ + T (r*r bits) binary: ‘d’ + TL + TR + Q (3 r*r bits)

and every well-shaped advice presents some graph of rank-width <= r. Vertex sets are encoded as union-of-root-path marks (see RankWidthGraph.encode_set); the E automaton carries each marked vertex’s interface vector – O(2^{2r}) states however large the graph.

advice(graph) compiles a RankWidthGraph whose decomposition has width <= r into the annotated advice (chain_ring.saturate / solve_left / factor_two_sided at p = 2, d = 1); check_implicit and evaluate_implicit run over the functional atoms without building any automaton. The flat letter alphabet caps r at 2: it grows as 2^{3r^2} binary letters, unlike the factored letters used by the group classes.

Parameters:

  • r (int)

  • max_states (int | None)

GRAPH = None#

elements are vertex sets and E is the edge relation, not equality

EQUALITY = 'Subset(x,y) and Subset(y,x)'#

extensional equality of sets

property cls: UniformlyTreeAutomaticClass#

The presentation, built lazily (the r = 2 E automaton enumerates a few million transitions).

advice(graph)[source]#

Compile a rank decomposition into the annotated advice; raises if some cut exceeds rank r. A pre-compiled advice tree passes through.

Return type:

Tree

Parameters:

graph (RankWidthGraph | Tree)

evaluate(phi)[source]#

Evaluate an MSO query over the class; variables range over vertex sets. See UniformlyTreeAutomaticClass.evaluate.

check(phi, graph, **sets)[source]#

Model check an MSO query against a single graph.

Return type:

bool

Parameters:

graph (RankWidthGraph | Tree)

property implicit_cls#

The fully implicit presentation (functional atoms only).

check_implicit(phi, graph, **sets)[source]#

Like check, evaluated implicitly (no automaton is built). Set assignments are padded to the advice shape (the implicit evaluator runs all tapes synchronously).

Return type:

bool

Parameters:

graph (RankWidthGraph | Tree)

evaluate_implicit(phi, graph, **sets)[source]#

The satisfying set of phi on the graph, computed implicitly: unassigned free variables stay open. Yields assignments {var: vertex set} when a graph object is given (raw mark trees for a bare advice); len is the exact solution count.

Parameters:

graph (RankWidthGraph | Tree)

get_structure(graph)[source]#

The MSO0-style tree-automatic presentation of a single graph.

Return type:

TreeAutomaticPresentation

autstr.tree_groups module#

Tree-indexed generalizations of the extraspecial p-groups as a uniformly tree-automatic class.

The advice is an arbitrary binary shape tree. It presents a class-2 group G_t with one generator pair x_w, y_w per inner node w, one central generator z_v per leaf v, exponent-p relations, and commutators

[x_w, y_w] = prod over the leaves v below w of z_v,

all other generator pairs commuting. The commutator supports form the laminar family of the tree: a spine advice (every inner node with a single child, one leaf at the bottom) makes every commutator hit the same z, which is exactly the extraspecial group p^(1+2n) of exponent p (p odd); general shapes interpolate between that and the direct sum of Heisenberg groups.

Concretely G_t = { (a, b, c) : a, b assign F_p to inner nodes, c assigns F_p to leaves } with the central-extension law

(a1,b1,c1)(a2,b2,c2) = (a1+a2, b1+b2, c), c(v) = c1(v) + c2(v) + sum over inner w < v of a1(w)*b2(w) (mod p).

Elements are encoded as trees of the advice’s exact shape: inner node w is labelled ‘i{a(w)}{b(w)}’, leaf v is labelled ‘l{c(v)}’. The multiplication automaton is the running-sum trick evaluated along all paths of the tree: a bottom-up state in F_p tracks the deficit c_z - c_x - c_y still owed by the ancestors, each inner node subtracts its commutator contribution a_x(w)*b_y(w), and siblings must agree on the owed amount when their branches merge — p + 1 states in total, independent of the shape.

Bounded rank-width (CutRankTreeGroups(p, k, r)): the tree analog of autstr.groups.CutRankGroups. A member is a class-2 central extension of Z_p^n by Z_p^k whose commutation form admits a tree layout in which every subtree’s crossing block has rank <= r over F_p; the advice spells out the factorizations node by node, and a spine layout is exactly the word class.

class autstr.tree_groups.TreeExtraspecialGroups(p, max_states=None)[source]#

Bases: SymbolicClassWrapper

The uniformly tree-automatic class of tree-indexed extraspecial p-groups (advice = shape tree, elements = coordinate labellings).

Parameters:

  • p (int)

  • max_states (int | None)

static spine(n)[source]#

Shape with n inner nodes over a single leaf: presents the extraspecial group p^(1+2n).

Return type:

Tree

Parameters:

n (int)

advice(shape)[source]#

Normalize a shape tree to advice (labels forced to ‘s’).

Return type:

Tree

Parameters:

shape (Tree)

encode(shape, a=(), b=(), c=())[source]#

The element (a, b, c) of G_shape as a tree. Coordinates are given per node address (’’ = root, then ‘0’/’1’ for left/right children); omitted coordinates are 0.

Return type:

Tree

Parameters:
evaluate(phi)[source]#

Evaluate a first-order query over the class; see UniformlyTreeAutomaticClass.evaluate.

check(phi, shape, **elements)[source]#

Model check a formula against the group G_shape. Free variables can be assigned element trees (see encode); unassigned ones are quantified existentially.

Return type:

bool

Parameters:

shape (Tree)

check_implicit(phi, shape, **elements)[source]#

Like check, evaluated implicitly (no query tree automaton).

Return type:

bool

Parameters:

shape (Tree)

get_structure(shape)[source]#

The tree-automatic presentation of the single group G_shape.

Return type:

TreeAutomaticPresentation

Parameters:

shape (Tree)

class autstr.tree_groups.CutRankTreeGroups(p, k=1, r=1, d=1, factored=None)[source]#

Bases: SymbolicClassWrapper

For a fixed prime p, center dimension k, width r and ring depth d, the uniformly tree-automatic class of class-2 groups over R = Z/p^d whose commutation form admits a tree layout of module cut-rank <= r (bounded rank-width over R) — the tree analog of autstr.groups.CutRankGroups, which is recovered exactly on spine layouts. With d = 1 (the default) R is the field F_p; d > 1 gives an exponent-p^d center. The tree merge is the step where the ring case genuinely differs from the field one: it needs the sibling block to factorise as V_R^T Q V_L, which requires the carried bases to be saturated free interfaces (chain_ring.factor_two_sided).

Generators are the post-order positions 1..n of a binary layout tree; the form is a dict {(j, i): label in Z_p^k, i < j} presenting x_j x_i = x_i x_j y^B[j,i], and the group law is the same bilinear cocycle as in the word class. Elements are (b, a) encoded as digit labellings of the advice’s shape; the k center digits live on a chain of ‘c’ nodes above the layout root.

Bottom-up, the state at a subtree S is (s, wx, wy): the correction accumulated by pairs inside S, and r linear functionals w = V·(digits of S) of each factor’s digits, where V is a row basis of S’s crossing block. Two vectors are needed because a crossing pair can be consumed in two ways: its larger endpoint is an ancestor of S (the read-off pairs y-functionals of S with that ancestor’s x-digit), or the pair is split between siblings (the merge pairs the right child’s x-functionals against the left child’s y-functionals — in post-order the left subtree lies entirely below the right one). The advice letter at a node holds the factorization data over R = Z/p^d (each entry as d base-p digits):

leaf:   'a' + v (r)
unary:  'b' + T (r x r) + v (r) + R (k x r)
binary: 'd' + T_L, T_R (r x r) + v (r) + R_L, R_R (k x r)
            + Q (k x (r x r))

with w <- T_L w_L + T_R w_R + v*digit (both factors), correction s <- s_L + s_R + x_t*(R_L wy_L + R_R wy_R) + wx_R^T Q_l wy_L, and the ‘c’ chain consuming s coordinate by coordinate: z_c - x_c - y_c = s. That is q^(k+2r) layout states however large the tree. advice compiles (shape, form) into letters — saturated free bases of the crossing blocks plus solving the consistency systems, including the two-sided factorization V_R^T Q V_L of the sibling block — and fails precisely when some subtree’s module cut-rank exceeds r; tree_cut_rank measures the width a layout needs. Every well-shaped advice presents some group in the class: the streamed cocycle is bilinear by construction.

The multiplication automaton is a product over the whole letter alphabet, so building it is only feasible for a small ring alphabet; cls is therefore lazy and simulate runs the transition directly over the tapes for larger q.

Signature: M(x,y,z), Eq(x,y); the center is first-order definable.

factored=None (the default) enumerates one advice letter per factorisation tuple when that alphabet fits under 20000 letters (the original encoding, byte-identical) and otherwise switches to factored letters: each layout node becomes a bare marker (‘a’ leaf / ‘b’ unary / ‘d’ binary) followed by a unary chain of one letter per ring entry, with the element digit repeated along the stretch. The factored alphabet has q+4 letters however large r, k and d are – this is what makes width r >= 2 over the ring representable.

Parameters:
MARKERS = ('a', 'b', 'd')#

leaf, unary, binary layout node

Type:

factored-mode node markers

n_entries#

ring entries per stretch, by node kind. Over the ring (d > 1) the binary stretch carries, instead of the k bilinear forms Q, the k full pairing tables over the register space: q^{2r} entries each.

property cls: UniformlyTreeAutomaticClass#

the tree multiplication automaton is a product over the whole letter alphabet, so its construction is only feasible for a small ring alphabet. The reference law, advice compiler, width measure and simulate never need it and stay cheap for any q.

Type:

The uniformly tree-automatic presentation, built lazily

static spine(n)[source]#

The word layout: a left chain, post-order = bottom-up.

Return type:

Tree

Parameters:

n (int)

static balanced(n)[source]#

A balanced binary layout with n nodes.

Return type:

Tree

Parameters:

n (int)

tree_cut_rank(shape, form)[source]#

The width the given tree layout needs: the maximal module cut-rank over R = Z/p^d of the crossing blocks of its subtrees (the free rank of the saturated interface; the ordinary F_p rank when d = 1).

Return type:

int

Parameters:
advice(shape, form)[source]#

Compile a layout and a form into the advice tree; raises if some subtree’s crossing block exceeds rank r. In factored mode each node becomes its bare marker with the ring entries chained above it.

Return type:

Tree

Parameters:
clique_form(n, label=None)[source]#

Nothing commutes; every crossing block is all-ones — cut-rank 1 on every layout.

Return type:

Dict

Parameters:
matching_form(n)[source]#

Disjoint commutator pairs of post-order neighbours: the extraspecial layout.

Return type:

Dict

Parameters:

n (int)

multiply(n, form, g, h)[source]#

Reference implementation of the group law over R = Z/p^d (identical to the word class: the group depends on the form, not the layout).

Parameters:
identity(n)[source]#
Parameters:

n (int)

simulate(advice, gx, gy, gz)[source]#

Run the multiplication automaton directly over the convolved trees: True iff the advice accepts gx * gy = gz. A bottom-up pass of the shared _m_step transition, without building the product tree automaton, so the saturated tree merge can be checked against the reference law for any ring alphabet. gx, gy, gz are (b, a) elements over the advice shape.

Return type:

bool

Parameters:

advice (Tree)

encode(element, shape)[source]#

Encode (b, a) over a layout shape (an advice tree is accepted too — its center chain is stripped). a is indexed by post-order. In factored mode each node’s digit is repeated along its entry stretch (so the element tree has the advice’s exact shape).

Return type:

Tree

Parameters:

shape (Tree)

evaluate(phi)[source]#
check(phi, advice, **elements)[source]#

Model check against the member presented by the advice; free variables can be assigned elements as (b, a) tuples.

Return type:

bool

Parameters:

advice (Tree)

decode(tree, advice)[source]#

Inverse of encode over the member’s advice: an element tree back to its (b, a) tuple (a indexed by post-order layout positions).

Parameters:
property implicit_cls#

The fully implicit presentation of this class (functional atoms only, nothing compiled): an autstr.implicit.ImplicitTreeClass over raw element trees. check_implicit/evaluate_implicit add the (b, a)-tuple encoding on top of it.

check_implicit(phi, advice, **elements)[source]#

Like check, but evaluated implicitly (no query or base tree automaton) – the only viable model checker for the large-alphabet ring members whose cls cannot be built. See autstr.implicit.

Return type:

bool

Parameters:

advice (Tree)

evaluate_implicit(phi, advice, **elements)[source]#

The satisfying set of phi on the member presented by the advice, computed implicitly: unassigned free variables stay open and are solved for. Yields assignments {var: (b, a)}; len is the exact solution count without enumeration. Works for members whose automata cannot be built.

Parameters:

advice (Tree)

get_structure(advice)[source]#
Return type:

TreeAutomaticPresentation

Parameters:

advice (Tree)

autstr.tree_presentations module#

Tree-automatic presentations: structures whose elements are finite trees and whose relations are recognized by sparse bottom-up tree automata reading tree convolutions.

Mirrors autstr.presentations.AutomaticPresentation with the tree pipeline underneath. The pipeline invariant also mirrors the string engine: stored relation automata are padding-saturated (accept their canonical convolutions with arbitrary all-padding regions attached below, via attach_padding), so expand may widen them to more tapes; intersections and unions preserve saturation; complements are re-intersected with the domain product; and project — which produces the canonical (trimmed) language — is followed by re-saturation, the tree analog of the string pipeline’s pad/unpad dance.

autstr.tree_presentations.tree_one(symbol_arity=1, base_alphabet=None)[source]#

Automaton accepting every tree.

Return type:

SparseTreeAutomaton

Parameters:

symbol_arity (int)

autstr.tree_presentations.tree_zero(symbol_arity=1, base_alphabet=None)[source]#

Automaton rejecting every tree.

Return type:

SparseTreeAutomaton

Parameters:

symbol_arity (int)

class autstr.tree_presentations.TreeAutomaticPresentationSerializer[source]#

Bases: object

Binary serialization for TreeAutomaticPresentation.

Mirrors autstr.presentations.AutomaticPresentationSerializer, but stores each automaton’s payload as raw bytes with a length prefix rather than as a JSON list of integers – which costs roughly four bytes of file per byte of data.

MAGIC = b'TPRS'#
VERSION = 1#
HEADER_FORMAT = '4sB3sII'#
HEADER_SIZE = 16#
classmethod serialize(presentation, filename)[source]#
Return type:

None

Parameters:

filename (str)

classmethod deserialize(filename)[source]#
Return type:

TreeAutomaticPresentation

Parameters:

filename (str)

class autstr.tree_presentations.TreeAutomaticPresentation(automata, padding_symbol='*', enforce_consistency=True, max_states=None)[source]#

Bases: DeferredRelations

A presentation of a structure by tree automata.

Parameters:

  • automata (Dict[str, SparseTreeAutomaton]) – ‘U’ is the domain automaton (symbol arity 1); every other key R presents a relation of arity k by an automaton of symbol arity k over convolutions of element trees.

  • padding_symbol – base letter used to pad convolutions.

  • max_states (Optional[int]) – optional cap for the subset determinizations inside projection (a clear error instead of an exponential blowup).

  • enforce_consistency (bool)

automatic_presentation_to_file(filename)[source]#

Write the presentation – domain, every built relation, alphabet – to a file. Deferred relations that have not been built are not stored; call materialize first to include them.

Return type:

None

Parameters:

filename (str)

classmethod automatic_presentation_from_file(filename)[source]#

Read a presentation written by automatic_presentation_to_file.

The signature is not stored – a codec is Python code, not data – so the result is a bare structure until symbolic is given one.

Parameters:

filename (str)

symbolic(signature=None)[source]#

A symbolic interface to this structure: variables, relation and function symbols that build first-order expressions with Python operators instead of formula strings.

Elements are trees, so a signature’s codec encodes Python values to Tree objects. Enumeration is shortlex by node count, which orders by encoding size rather than by any notion of value.

Parameters:

signature – declared functions, operators and element codec.

Returns:

a autstr.symbolic.SymbolicContext.

default_signature()[source]#

The signature symbolic() uses when none is given, or None for a structure addressed through its relation symbols. See autstr.symbolic.operation_signature.

update(**automata)[source]#

Install or replace relations. Values may be automata (saturated and domain-restricted like at construction time) or formula strings over the current signature.

Return type:

None

check(phi)[source]#

Truth of phi (free variables existentially quantified).

Return type:

bool

evaluate(phi, updates=None)[source]#

Automaton of all satisfying assignments (tapes = sorted free variables; padding-saturated form).

Parameters:

  • phi – the first-order formula.

  • updates (Optional[Dict[str, Union[SparseTreeAutomaton, str]]]) – relations to install for this evaluation only. Values may be automata or formula strings over the current signature, and are prepared exactly as at construction time – so a spliced automaton is padding-saturated and domain-restricted before any projection sees it.

Return type:

SparseTreeAutomaton

autstr.tree_uniform module#

Uniformly tree-automatic classes of structures.

The tree analog of autstr.uniform: a single tuple of tree automata presents a whole class of structures. Every automaton carries one additional tape (tape 0) holding an advice tree that is read convolution-synchronously with the element encodings. Fixing an advice tree t instantiates one member structure S_t:

universe(S_t) = { x | t ⊗ x ∈ L(U) } R^{S_t} = { x̄ | t ⊗ x̄ ∈ L(R) }

First-order queries are evaluated once for the entire class; model checking a sentence against a member structure then reduces to running its advice tree through the query automaton. Because the advice may be a tree, the member universes can live on tree-shaped skeletons — the setting for bounded tree-width graph classes and tree-indexed algebraic families.

The formula layer (relativization of quantifiers to Dom(advice, ·), the advice as one more first-order variable, Adv as the projection of the domain onto the advice tape) is inherited unchanged from the string implementation; only the automaton operations differ.

autstr.tree_uniform.sta_from_delta(sigma, states, arity, delta, finals, dead='dead', tapes=None)[source]#

Build a SparseTreeAutomaton from a bottom-up transition function.

Parameters:

  • delta – delta(left_state, right_state, symbol_tuple) -> state, where an absent child is passed as None. dead names the sink (stored as the sparse global default); dead children are never enumerated, so delta need not handle them.

  • tapes – optional per-tape alphabets. A convolution tape usually ranges over a small part of the base alphabet – the advice tape reads advice letters, an element tape reads element letters – and every mixed tuple is dead. Enumerating sigma^arity therefore spends almost all of its time confirming that nonsense is dead: for clique-width at k = 4 only 207 of 17576 triples are meaningful. Naming the tapes’ alphabets restricts the enumeration to their product; every other symbol falls to the global default, which is the dead sink. Defaults to sigma on every tape.

Return type:

SparseTreeAutomaton

Each child pair’s majority target becomes its pair default (ties prefer the dead sink), and only deviations are stored as exceptions — states that loop on most symbols stay cheap over large alphabets. With tapes given, the unenumerated symbols already outnumber the rest, so the dead sink is the majority everywhere and no pair defaults are emitted.

class autstr.tree_uniform.UniformlyTreeAutomaticClass(automata, padding_symbol='*', max_states=None)[source]#

Bases: UniformlyAutomaticClass

A uniformly tree-automatic presentation of a class of structures.

Parameters:

  • automata (Dict[str, SparseTreeAutomaton]) – dictionary of SparseTreeAutomatons. ‘U’ is reserved for the domain automaton of symbol arity 2 (advice tape, element tape). Every other key R presents a relation of arity r with an automaton of symbol arity 1 + r (advice tape first, then the element tapes).

  • padding_symbol – base letter used to pad the convolutions.

  • max_states (Optional[int]) – optional cap for the subset determinizations inside projections (a clear error instead of an exponential blowup).

check(phi, advice, **assignments)[source]#

Model check a formula against the member structure S_advice.

Parameters:

  • phi (Union[str, Expression]) – a formula over the class signature. Free variables can be assigned concrete elements via assignments (name = element tree); unassigned free variables are existentially quantified.

  • advice (Tree) – the advice tree.

Return type:

bool

check_implicit(phi, advice, **assignments)[source]#

Model check a formula against the member S_advice without compiling a query tree automaton: the formula is evaluated bottom-up on the fly over the base tree automata. Scales to classes whose query automaton is infeasible. See autstr.implicit.

Unlike check, the on-the-fly evaluator is synchronous: it walks the advice tree and every assigned element tree in lockstep and does not convolve or pad mismatched shapes, so the assigned trees must already be padded to the advice’s shape.

Return type:

bool

Parameters:

advice (Tree)

evaluate_implicit(phi, advice, **assignments)[source]#

The satisfying set of phi on the member S_advice, computed implicitly (no query tree automaton): unassigned free variables stay open and are solved for over the fixed advice. Returns a TreeSolutionSet of {var: tree} assignments (trees of the advice’s shape) — its len is the exact solution count, iterating lazily yields the assignments. See autstr.implicit.

Parameters:

advice (Tree)

define(name, phi)[source]#

Define a new class relation by a first-order formula over the existing signature. The relation’s arguments are the free variables of phi in sorted order; the advice moves back to tape 0.

Return type:

SparseTreeAutomaton

Parameters:

  • name (str)

  • phi (str | Expression)

get_structure(advice)[source]#

Instantiate the member structure S_advice as an ordinary tree-automatic presentation (the advice tape is fixed to the given tree and projected out).

Return type:

TreeAutomaticPresentation

Parameters:

advice (Tree)

autstr.turing module#

Turing machines and their configuration graphs.

The configuration graph of a Turing machine is the standard example of an automatic structure that is genuinely about computation: a configuration is a word, and one step of the machine rewrites that word locally, at the head, so the step relation is recognized by a small synchronous automaton — one whose size depends only on the transition table, not on the tape.

That makes the first-order theory of the graph decidable, and this module lets you ask it:

>>> machine = TuringMachine(
...     transitions={('q', '1'): ('q', '1', 'R'),
...                  ('q', '_'): ('halt', '1', 'S')},
...     blank='_')
>>> graph = machine.configuration_graph()
>>> graph.check('all x.(all y.(all z.((E(x,y) & E(x,z)) -> Eq(y,z))))')
True

The boundary lesson. Reachability — “does some sequence of steps lead from this configuration to a halting one?” — is exactly the halting problem, so it is undecidable, and therefore not first-order definable over this graph. Nothing here provides it, and nothing can: the transitive closure of E is outside FO. A decidable first-order theory is not a decidable graph. It is the same lesson as the random graph in reverse — there, a decidable theory without an automatic presentation; here, an automatic presentation whose decidable theory still cannot express the one question you would most like to ask.

Encoding. The tape is one-way infinite, to the right. A configuration is the word left · (state, symbol) · right: the tape contents, with the cell under the head replaced by a symbol naming both the state and what is written there. Trailing blanks are dropped, so each configuration has exactly one word. A step changes the word only at the head and, at most, by one cell at the right end, which is why a synchronous automaton can read it. A left move off cell 0 has no successor, as does a configuration whose (state, symbol) pair the transition table does not list — those are the halting configurations, and Halt is defined from E rather than authored.

autstr.turing.DIRECTIONS = ('L', 'R', 'S')#

how a transition may move the head

class autstr.turing.Configuration(state, tape, head=0)[source]#

Bases: object

A machine configuration: the control state, the tape, and where the head is.

Parameters:

  • state (str) – the control state.

  • tape (Tuple[str, ...]) – the tape contents from cell 0, as a tuple of tape symbols.

  • head (int) – the index of the cell under the head.

state: str#
tape: Tuple[str, ...]#
head: int = 0#
class autstr.turing.TuringMachine(transitions, blank='_', states=None, tape_alphabet=None)[source]#

Bases: object

A deterministic single-tape Turing machine with a one-way infinite tape.

Parameters:

  • transitions (Dict[Tuple[str, str], Tuple[str, str, str]]) – {(state, read): (state, write, direction)}, with direction one of 'L', 'R', 'S'. A pair the table omits is halting.

  • blank (str) – the blank symbol, which fills the tape beyond what has been written.

  • states (Optional[Sequence[str]]) – the control states. Read off the table when omitted.

  • tape_alphabet (Optional[Sequence[str]]) – the tape symbols. Read off the table when omitted; the blank always belongs.

canonical(configuration)[source]#

The configuration with trailing blanks past the head dropped — the one word that stands for it.

Return type:

Configuration

Parameters:

configuration (Configuration)

step(configuration)[source]#

The successor configuration, or None if there is none — the transition table does not cover this (state, symbol) pair, or the head would move off the left end of the tape.

This is the Python oracle the automaton is checked against, and the obvious way to run the machine.

Return type:

Optional[Configuration]

Parameters:

configuration (Configuration)

run(configuration, limit=1000)[source]#

The run from a configuration: it, then its successors, stopping when the machine halts or after limit steps.

Parameters:
configuration_graph()[source]#

The graph of configurations under one step of the machine.

Return type:

ConfigurationGraph

encode(configuration)[source]#

The word encoding a configuration.

Return type:

list

Parameters:

configuration (Configuration)

decode(word)[source]#

The configuration a word encodes.

Return type:

Configuration

class autstr.turing.ConfigurationGraph(machine)[source]#

Bases: object

The configuration graph of a TuringMachine: configurations as vertices, one machine step as a directed edge.

The presentation carries E (one step), Eq, and Halt — the configurations with no successor, defined as not exists y. E(x,y) rather than authored, since the engine can compute it.

Reachability is deliberately absent; see the module docstring.

Parameters:

machine (TuringMachine)

symbolic(signature=None)[source]#

A symbolic interface to the graph; write one step as x.adj(y) and configurations as Configuration values.

check(phi)[source]#
Return type:

bool

evaluate(phi)[source]#
get_relation_symbols()[source]#
is_deterministic()[source]#

Whether every configuration has at most one successor — a first-order question, and so decidable here, unlike reachability.

Return type:

bool

autstr.uniform module#

Uniformly automatic classes of structures.

A uniformly automatic presentation describes a whole class of structures with a single tuple of automata: every automaton carries one additional tape (tape 0) holding an advice string that is read synchronously with the element encodings. Fixing an advice string α instantiates one member structure S_α:

universe(S_α) = { x | α ⊗ x ∈ L(U) } R^{S_α} = { x̄ | α ⊗ x̄ ∈ L(R) }

First-order queries are evaluated once for the entire class; model checking a sentence against a member structure then reduces to running its advice string through the query automaton.

autstr.uniform.dfa_from_delta(sigma, states, arity, delta, initial, finals, tapes=None, dead=None)[source]#

Build a SparseDFA from a transition function over the full symbol space sigma^arity. Convenience for constructing presentation automata.

Parameters:

  • tapes – optional per-tape alphabets (the string analog of sta_from_delta’s parameter). A convolution tape usually ranges over a small part of the base alphabet — the advice tape reads advice letters, an element tape reads element letters — and every mixed tuple is dead. Naming the tapes’ alphabets restricts the enumeration to their product; every other symbol falls to dead, which must then be named and becomes every state’s sparse default.

  • dead – name of the sink state (required with tapes); delta must map it to itself on every enumerated symbol.

Return type:

SparseDFA

class autstr.uniform.SymbolicClassWrapper[source]#

Bases: object

Mixin for the family wrappers that present a class through .cls.

The wrappers (the group and algebra families) hold their uniformly automatic class in .cls and otherwise offer a domain-specific API. This forwards the symbolic interface to that class and supplies the family’s operator vocabulary, so ExtraspecialGroups(3).symbolic() works directly instead of reaching into .cls.

Subclasses set GRAPH and OPERATOR; the default is a multiplicative group, since that is what most of these families are.

GRAPH = 'M'#

the ternary relation R(x, y, z) meaning x op y = z

OPERATOR = '*'#

the Python operator it binds to

EQUALITY = None#

how equality is defined when the class does not ship it, as a formula over the existing signature; None if the class already has one

default_signature()[source]#
symbolic(signature=None)[source]#

A symbolic interface to this family; see UniformlyAutomaticClass.symbolic. Element codecs are not used over a class – an element’s encoding depends on the advice – so constants and decoded solutions come from get_structure(advice).symbolic().

class autstr.uniform.UniformlyAutomaticClass(automata, padding_symbol='*')[source]#

Bases: DeferredRelations

A uniformly automatic presentation of a class of structures.

Parameters:

  • automata (Dict[str, SparseDFA]) – dictionary of SparseDFAs. ‘U’ is reserved for the domain automaton of symbol arity 2 (advice tape, element tape). Every other key R presents a relation of arity r with an automaton of symbol arity 1 + r (advice tape first, then the element tapes).

  • padding_symbol – symbol used to pad the shorter tapes of a convolution.

symbolic(signature=None)[source]#

A symbolic interface to this class. Expressions are written over the class signature exactly as for a single structure; the advice tape is added and quantifiers relativized to the member domain during compilation, and results carry the advice under the tape name 'advice'.

Parameters:

signature – declared functions and operators. An element codec has no advice-free meaning here and is not used.

Returns:

a autstr.symbolic.SymbolicContext.

default_signature()[source]#

The signature symbolic() uses when none is given, or None for a class addressed through its relation symbols. See autstr.symbolic.operation_signature.

evaluate(phi)[source]#

Evaluate a first-order query over the class.

Parameters:

phi (Union[str, Expression]) – formula over the class signature; quantifiers range over the elements of the member structures.

Return type:

Tuple[SparseDFA, List[str]]

Returns:

(dfa, variables) where dfa presents all satisfying assignments — its tapes are the advice followed by the free variables of phi — and variables names the tapes in order.

check(phi, advice, **assignments)[source]#

Model check a formula against the member structure S_advice.

Parameters:

  • phi (Union[str, Expression]) – a formula over the class signature. Free variables can be assigned concrete elements via assignments (name = encoded word of the same length as the advice); unassigned free variables are existentially quantified.

  • advice (List) – the advice string (sequence of base alphabet symbols).

Return type:

bool

check_implicit(phi, advice, **assignments)[source]#

Model check a formula against the member S_advice without compiling a query automaton: the formula is evaluated on the fly over the base automata (implicit product / on-the-fly powerset / acceptance flip). Same contract as check; scales to classes whose query automaton is infeasible to build. See autstr.implicit.

Return type:

bool

evaluate_implicit(phi, advice, **assignments)[source]#

The satisfying set of phi on the member S_advice, computed implicitly (no query automaton): unassigned free variables stay open and are solved for over the fixed advice. Returns a StringSolutionSet of {var: word} assignments — its len is the exact solution count (no enumeration), iterating lazily yields the assignments. See autstr.implicit.

define(name, phi)[source]#

Define a new class relation by a first-order formula over the existing signature (the uniform analog of a Büchi-style bootstrap). The relation’s arguments are the free variables of phi in sorted order; the advice stays on tape 0.

Return type:

SparseDFA

Parameters:

  • name (str)

  • phi (str | Expression)

get_structure(advice)[source]#

Instantiate the member structure S_advice as an ordinary automatic presentation (the advice tape is fixed and projected out).

Parameters:

advice (List) – the advice string (sequence of base alphabet symbols).

Return type:

AutomaticPresentation

Module contents#

Contents