autstr package#
Subpackages#
- autstr.buildin package
- autstr.utils package
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:
objectCanonical 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.
- class autstr.algebra.Z1pLocalization(p)[source]#
Bases:
objectFactory-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:
- 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:
- Parameters:
- add(x, y)[source]#
Return x + y in canonical form.
- Return type:
- Parameters:
x (Z1pElement)
y (Z1pElement)
- neg(x)[source]#
Return -x in canonical form.
- Return type:
- Parameters:
x (Z1pElement)
- sub(x, y)[source]#
Return x - y in canonical form.
- Return type:
- Parameters:
x (Z1pElement)
y (Z1pElement)
- equals(x, y)[source]#
Semantic equality in Z[1/p] (canonical reps compare directly).
- Return type:
- Parameters:
x (Z1pElement)
y (Z1pElement)
- 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).
- autstr.algebra.z1p_localization(p)[source]#
Return a fixed-prime localization factory for Z[1/p].
- Return type:
- Parameters:
p (int)
- class autstr.algebra.FiniteBooleanAlgebras[source]#
Bases:
objectThe 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.
- check(phi, n, **subsets)[source]#
Model check against the algebra with n atoms; free variables can be assigned subsets of {0, …, n-1}.
autstr.arithmetic module#
- class autstr.arithmetic.Term[source]#
Bases:
ABCAbstract class representing a term over the (base 2) Büchi arithmetic over the integers \(\mathbb{Z}\)
- arithmetic = <autstr.presentations.AutomaticPresentation object>#
- abstractmethod update_presentation(recursive=True)[source]#
Updates the internal presentation of the term.
- Parameters:
recursive – If True, recursively updates the presentation of all sub-relations
- Return type:
- Returns:
- class autstr.arithmetic.RelationalAlgebraTerm[source]#
-
- drop(variables)[source]#
Drop variables.
- Parameters:
variables (
List[Union[str,VariableETerm]]) – The variables to drop- Return type:
- Returns:
projection of the current relation onto the variables self.get_variables without variables
- ex(variables)[source]#
Create Existential quantification term :type variables:
List[Union[str,VariableETerm]] :param variables: The variables that should be quantified :return: projection of the current relation onto the variables self.get_variables without variables- Parameters:
variables (List[str | VariableETerm])
- exinf(variable)[source]#
Represents the relation of the form \(\{\bar{x} | \exists \infty\text{-many } y: R(\bar{x}, y)\}\) for some base relation \(R\).
- Parameters:
variable (
Union[str,VariableETerm]) – Variable that should be \(\exists^\infty\)-quantified- Returns:
- class autstr.arithmetic.ExInfRATerm(term, variable)[source]#
Bases:
RelationalAlgebraTerm- Parameters:
term (RelationalAlgebraTerm)
variable (Union[str, VariableETerm])
- class autstr.arithmetic.BaseRATerm(relation_symbol, terms)[source]#
Bases:
RelationalAlgebraTermRepresents a term of the form \(R(t_1,...,t_n)\) for elementary terms \(t_1,...,t_n\)
- update_presentation(recursive=True, **kwargs)[source]#
Updates the internal presentation of the term.
- Parameters:
recursive – If True, recursively updates the presentation of all sub-relations
- Return type:
- Returns:
- to_fo()[source]#
Creates the a translation of the atomic formula \(R(t_1(\bar{x}), ..., t_n(\bar{x}))\) into a relational first-order formula with new predicates for \(T_1,..., T_n\) for the graphs of \(t_1,...,t_n\). The result will be of shape \(\exists y_1,...,y_n.(T_1(\bar{x}, y_1) \wedge ... \wedge T_n(\bar{x}, y_n) \wedge R(y_1,...y_n))\). The method guarantees that the newly created relation symbols \(T_1,...,T_n\) do not collide with already defined relation symbols.
- Return type:
Tuple[str,Dict[str,ElementaryTerm]]- Returns:
The relational formula and the mapping of new relation symbols to terms
- class autstr.arithmetic.BinaryRATerm(left, right)[source]#
Bases:
RelationalAlgebraTerm,ABCAbstract class that represents binary relational algebra terms.
- Parameters:
left (RelationalAlgebraTerm)
right (RelationalAlgebraTerm)
- class autstr.arithmetic.IntersectionRATerm(left, right)[source]#
Bases:
BinaryRATermIntersection of two relations.
- Parameters:
left (RelationalAlgebraTerm)
right (RelationalAlgebraTerm)
- class autstr.arithmetic.UnionRATerm(left, right)[source]#
Bases:
BinaryRATermUnion of two relations.
- Parameters:
left (RelationalAlgebraTerm)
right (RelationalAlgebraTerm)
- class autstr.arithmetic.ComplementRATerm(relation)[source]#
Bases:
RelationalAlgebraTermThe complement of a relation
- Parameters:
relation (RelationalAlgebraTerm)
- class autstr.arithmetic.DropRATerm(relation, variables)[source]#
Bases:
RelationalAlgebraTermRelation of the shape \(\{(x_1,...,x_n) | (x_1,...,x_n,y_1,...,y_m) \in R\}\) where \(y_1,\ldots,y_m\) are the dropped variables.
- class autstr.arithmetic.ElementaryTerm[source]#
-
Elementary term. These terms are evaluated in the base structure, i.e. the yield integers.
- classmethod to_term(x)[source]#
Classmethod for converting str and int into variables and constants, respectively.
- Parameters:
x (
Union[str,int,ElementaryTerm]) – The input parameter- Return type:
- Returns:
the term tht presents x
- eq(other)[source]#
Creates the relation \(\textrm{self} == \textrm{other}\).
- Parameters:
other (
ElementaryTerm) – the rhs of the equality- Return type:
- Returns:
- lt(other)[source]#
Creates the relation \(\textrm{self} < \textrm{other}\).
- Parameters:
other – The term on the rhs
- Return type:
- Returns:
- class autstr.arithmetic.ConstantETerm(n)[source]#
Bases:
ElementaryTerm- Parameters:
n (int)
- class autstr.arithmetic.VariableETerm(name)[source]#
Bases:
ElementaryTermInitialization.
- Parameters:
name (
str) – The name of the variable
- class autstr.arithmetic.NegatedETerm(term)[source]#
Bases:
ElementaryTerm- Parameters:
term (ElementaryTerm)
- class autstr.arithmetic.AdditionETerm(left, right)[source]#
Bases:
ElementaryTerm- Parameters:
left (ElementaryTerm)
right (ElementaryTerm)
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.valuation(x, p, d)[source]#
The p-adic valuation v(x) in {0, .., d} of x in R; v(0) = d.
- autstr.chain_ring.is_unit(x, p, d)[source]#
A unit of R is a valuation-0 element (x not divisible by p).
- autstr.chain_ring.to_digits(x, p, d)[source]#
An R-element as its d base-p digits, least significant first.
- autstr.chain_ring.from_digits(digits, p)[source]#
Reassemble an R-element from base-p digits, least significant first.
- 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.
- autstr.chain_ring.smith_normal_form(M, p, d)[source]#
Diagonalise M over R = Z/p^d.
Returns
(exps, Winv)whereexpsare the valuations of the nonzero invariant factors (each < d) in order, andWinvis a unimodular n x n matrix whose firstlen(exps)rows are a free basis of the saturation ofrowsp(M): concretelyrowsp(M) == rowsp(diag(p^exps) @ Winv[:t]).
- 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, andexpsthe valuations withrowsp(M) == rowsp(diag(p^exps) @ basis). The free rankrho = 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.
- autstr.chain_ring.module_cut_rank(M, p, d)[source]#
The free rank rho of the saturation of
rowsp(M)(module cut-rank).
- 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.
- autstr.chain_ring.right_inverse(V, p, d)[source]#
A right inverse Y (n x r) with
V @ Y == I_rover R, for a right-invertible V (r x n). Raises if V is not right-invertible.
- autstr.chain_ring.solve_left(V, B, p, d)[source]#
The general ring solve
XwithX @ V == Bover R = Z/p^d.Vis (r x m) and may be rank-deficient (e.g. a padded basis with zero rows);Bis (s x m); the resultXis (s x r). Every row of B must lie inrowsp(V)– otherwise there is no solution and a ValueError is raised. Free coordinates of the solution are set to 0.Solves
A @ Y = CwithA = V^T(m x r) andC = B^Tby Smith-style diagonalisation of A: row operations are mirrored on C and column operations are accumulated inWcso the solution maps back asY = Wc @ Z. This is the ring generalisation of the field solverautstr.groups._solve_xa_eq_b(X A = B) used by the linear layout compiler, and drives the saturated streaming update over the chain ring.
- 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 saturatedVbar(r x m’) and a saturatedWbar(r’ x m) such that every row of X lies inrowsp(Vbar)and every column of X lies incolsp(Wbar^T), returnsQ(r’ x r) withX == 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 = XthenQ 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.
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:
objectA 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 > 1is 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_widthis 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.- 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)
- 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 > 1the sites and the form labels live over the chain ring R = Z/p^d.
- 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 > 1the sites live over the chain ring R = Z/p^d (the tensor keeps unit coefficients; the center gains exponent p^d).
- 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 > 1the sites live over the chain ring R = Z/p^d.
- 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).
- class autstr.cocycle_groups.CocycleRankWidthGroups(p, r=1, d=1)[source]#
Bases:
objectThe 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.
- 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:
- Parameters:
sites (CocycleSites)
T (Dict)
- encode(element, sites, advice)[source]#
Element tree of the advice’s shape: each site’s digit repeats along its instruction stretch.
- Return type:
- Parameters:
sites (CocycleSites)
advice (Tree)
- 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.
- multiply(sites, T, g, h)[source]#
- Parameters:
sites (CocycleSites)
T (Dict)
- simulate(advice, tx, ty, tz)[source]#
Run the transition function over the convolved trees, with an explicit stack (instruction stretches can be long).
- property cls#
- check(phi, sites, advice, **elements)[source]#
- Return type:
- Parameters:
sites (CocycleSites)
advice (Tree)
- property implicit_cls#
- check_implicit(phi, sites, advice, **elements)[source]#
First-order model checking over the functional atoms.
- Return type:
- Parameters:
sites (CocycleSites)
advice (Tree)
- evaluate_implicit(phi, sites, advice, **elements)[source]#
The satisfying set of phi, computed implicitly; yields assignments {var: (b, a)}.
- Parameters:
sites (CocycleSites)
advice (Tree)
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 . wfor the wordswthe 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.
- 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] . wand one of the right factor astags[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:
- Parameters:
left (AutomaticPresentation)
right (AutomaticPresentation)
tags (Sequence)
- 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:
kind (
str) –'sync'or'async'.left (AutomaticPresentation)
right (AutomaticPresentation)
- Return type:
- 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] . alphaand one of the right classtags[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
wbecomesskip . w. Use tagged_advice and tagged_element to build them.- Return type:
- Parameters:
left (UniformlyAutomaticClass)
right (UniformlyAutomaticClass)
tags (Sequence)
skip (str)
- 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_npresents the product of the members thatalpha_1, ..., alpha_npresent, and an element of that product is the tuplew_1 # ... # w_nof 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:
- Parameters:
uniform (UniformlyAutomaticClass)
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:
objectBase class for graphs encoded as strings of per-vertex letters.
- class autstr.graphs.TreeDepthGraph(letters, nodes=None)[source]#
Bases:
StringGraphA 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.
- 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:
- class autstr.graphs.PathWidthGraph(letters, nodes=None)[source]#
Bases:
StringGraphA 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).
- 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:
- class autstr.graphs.TreeDepthClass(d)[source]#
Bases:
_SetGraphClassThe uniformly automatic class of graphs of tree-depth <= d, presented over set-valued elements (MSO0 style).
- Parameters:
d (int)
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:
objectThe 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'}#
- check(phi, advice, **elements)[source]#
Model check against one group; free variables can be assigned elements as (twist, exponent) pairs.
- check_implicit(phi, advice, **elements)[source]#
Like check, evaluated implicitly (no query automaton).
- class autstr.groups.ExtraspecialGroups(p)[source]#
Bases:
objectFor 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)
- 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.
- class autstr.groups.FiniteAbelianGroups[source]#
Bases:
objectThe 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).
- 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).
- check_implicit(phi, orders, **elements)[source]#
Like check, evaluated implicitly (no query automaton).
- class autstr.groups.CutRankGroups(p, k=1, r=1, d=1, factored=None)[source]#
Bases:
objectFor 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.
- MARKER = 'n'#
marker letter opening each position’s entry stretch in factored mode
- 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).
- 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.
- 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.
- matching_form(n)[source]#
Disjoint commutator pairs hitting the first center coordinate: the extraspecial layout, cut-rank 1.
- 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).
- 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.
- 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.
- check(phi, advice, **elements)[source]#
Model check against the member presented by the advice; free variables can be assigned elements as (b, a) tuples.
- 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.
- 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.
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:
objectA 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:
- 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:
- Parameters:
- autstr.implicit.dfa_product(a, b, accept)[source]#
- Return type:
- Parameters:
a (ImplicitDFA)
b (ImplicitDFA)
- autstr.implicit.dfa_complement(a)[source]#
- Return type:
- 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:
- Parameters:
a (ImplicitDFA)
var (str)
alphabet (Sequence)
- 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.
- class autstr.implicit.ImplicitTA(tapes, step, accepting)[source]#
Bases:
objectA 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:
- autstr.implicit.ta_atom(sta, tapes)[source]#
Wrap an explicit SparseTreeAutomaton as an implicit atom.
- Return type:
- Parameters:
- autstr.implicit.ta_product(a, b, accept)[source]#
- Return type:
- Parameters:
a (ImplicitTA)
b (ImplicitTA)
- autstr.implicit.ta_complement(a)[source]#
- Return type:
- 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:
- Parameters:
a (ImplicitTA)
var (str)
alphabet (Sequence)
- autstr.implicit.run_ta(a, inputs)[source]#
Run over labelled trees (one per tape, all of the same shape).
- Return type:
- Parameters:
a (ImplicitTA)
- class autstr.implicit.StringSolutionSet(a, inputs, length, solve_vars, alphabet_of)[source]#
Bases:
objectThe 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.
- class autstr.implicit.TreeSolutionSet(a, inputs, solve_vars, alphabet_of)[source]#
Bases:
objectThe 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.
- class autstr.implicit.MappedSolutions(base, mapper)[source]#
Bases:
objectA 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 builderargs -> 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:
- autstr.implicit.check_tree(phi, atoms, inputs, alphabet_of)[source]#
Implicitly decide a (relativized) formula over tree automata.
- 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:
- 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:
- 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:
- 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:
- class autstr.implicit.ImplicitClass(atoms, element_alphabet)[source]#
Bases:
objectA 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.- check(phi, advice, **assignments)[source]#
Model check against the member presented by the advice word; unassigned free variables are existentially closed.
- Return type:
- class autstr.implicit.ImplicitTreeClass(atoms, element_alphabet)[source]#
Bases:
objectTree analog of ImplicitClass: atoms are
args -> ImplicitTAbuilders (or explicit SparseTreeAutomaton objects), members are advice trees.- check(phi, advice, **assignments)[source]#
Model check against the member presented by the advice tree; unassigned free variables are existentially closed.
- Return type:
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.
- class autstr.mtbdd.ComputedTable(cap_log2=23, dict_limit=524288)[source]#
Bases:
objectA 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.
- mask#
- shift#
- keys#
- vals#
- 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/8bytes and hashes in one pass, where a frozenset costs tens of bytes per member.
- class autstr.mtbdd.NodeStore[source]#
Bases:
objectHash-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.
- 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.
- 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).
- 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 -> targetdeviations.
- 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 havebits_A + bits_Bvariables. Letters multiply; bits add.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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:
- 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).
autstr.presentations module#
- class autstr.presentations.AutomaticPresentationSerializer[source]#
Bases:
object- MAGIC = b'APRS'#
- VERSION = 1#
- HEADER_FORMAT = '4sB3sII'#
- HEADER_SIZE = 16#
- class autstr.presentations.AutomaticPresentation(automata, padding_symbol='*', enforce_consistency=True)[source]#
Bases:
objectA 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)
- get_relation_symbols()[source]#
Returns list of all defined relation symbols. The symbol ‘U’ must always be defined and denotes the Universe.
- check(phi)[source]#
Checks if a given first-order formula holds on the presented structure. Free variables are assumed be implicitly existentially quantified.
- evaluate(phi, updates=None)[source]#
Evaluates a given first-order query on the presented structure. Returns a presentation of the set of all satisfying assignments.
- Parameters:
- Return type:
- Returns:
The truth value of the formula, if the formula where all free variables are existentially quantified.
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#
- 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:
objectDeterministic 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 -> targetexceptions. 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).
- 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.
- 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.
- 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:
- 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).
- alphabet_projection(projection_map)[source]#
Relabel symbols by projection_map, which may merge them and thus make the automaton nondeterministic (inspection-scale: it decodes).
- 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.
- 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.
- 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:
- 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:
- 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.
- 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.
- 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:
objectNondeterministic 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 -> targetexception 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.- 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:
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:
objectAn immutable labelled binary tree (convenience representation).
- label#
- left#
- right#
- 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).
- 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.
- 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:
objectDeterministic 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) -> targetexceptions — 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 isBOT = 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_targetfor 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)
- transitions(left, right, symbol)[source]#
Batched transition lookup: find each pair’s diagram, then descend it along the symbol’s digits.
- Return type:
- 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.
- 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:
- 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:
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:
objectA 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.
- encode_set(subset)[source]#
Encode a set of nodes as a marked tree over the advice shape.
- Return type:
- 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:
- class autstr.tree_graphs.TreeWidthClass(w, max_states=None)[source]#
Bases:
objectThe uniformly tree-automatic class of graphs of tree-width <= w, presented over set-valued elements (MSO0 style).
- advice(graph)[source]#
The advice tree of a graph (its letters as alphabet symbols).
- Return type:
- 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:
- class autstr.tree_graphs.CliqueWidthGraph(expression, k)[source]#
Bases:
objectA 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).
- 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:
- classmethod clique(n)[source]#
K_n, clique-width 2: absorb each new vertex into label 0.
- Return type:
- Parameters:
n (int)
- classmethod complete_bipartite(left, right)[source]#
K_{left,right}, clique-width 2: join the two colour classes once.
- Return type:
- 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:
- Parameters:
n (int)
- class autstr.tree_graphs.CliqueWidthClass(k, max_states=None)[source]#
Bases:
objectThe 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.
- advice(graph)[source]#
The advice tree of a graph (its k-expression).
- Return type:
- 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:
- Parameters:
graph (CliqueWidthGraph | Tree)
- class autstr.tree_graphs.RankWidthGraph(shape, edges)[source]#
Bases:
objectA 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)
- cut_matrix(node)[source]#
The bipartite adjacency block of the node’s cut: rows the outside vertices, columns the inside leaves (left-to-right).
- 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:
- 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).
- static caterpillar(n)[source]#
The linear (caterpillar) decomposition: leaves 0..n-1 hang left to right off a left-deep spine.
- classmethod clique(n)[source]#
K_n: every crossing block is all ones – rank-width 1 on any decomposition.
- Return type:
- Parameters:
n (int)
- classmethod path(n)[source]#
P_n in path order: one edge crosses each caterpillar cut – rank-width 1.
- Return type:
- 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:
- Parameters:
n (int)
- class autstr.tree_graphs.RankWidthClass(r, max_states=None)[source]#
Bases:
objectThe 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.
- 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:
- 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:
- 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:
- 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)
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:
objectThe uniformly tree-automatic class of tree-indexed extraspecial p-groups (advice = shape tree, elements = coordinate labellings).
- static spine(n)[source]#
Shape with n inner nodes over a single leaf: presents the extraspecial group p^(1+2n).
- 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.
- 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.
- check_implicit(phi, shape, **elements)[source]#
Like check, evaluated implicitly (no query tree automaton).
- class autstr.tree_groups.CutRankTreeGroups(p, k=1, r=1, d=1, factored=None)[source]#
Bases:
objectFor 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.
- 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
- 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).
- 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.
- clique_form(n, label=None)[source]#
Nothing commutes; every crossing block is all-ones — cut-rank 1 on every layout.
- matching_form(n)[source]#
Disjoint commutator pairs of post-order neighbours: the extraspecial layout.
- 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).
- 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.
- 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).
- check(phi, advice, **elements)[source]#
Model check against the member presented by the advice; free variables can be assigned elements as (b, a) tuples.
- 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).
- 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.
- 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)
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:
- Parameters:
symbol_arity (int)
- autstr.tree_presentations.tree_zero(symbol_arity=1, base_alphabet=None)[source]#
Automaton rejecting every tree.
- Return type:
- Parameters:
symbol_arity (int)
- class autstr.tree_presentations.TreeAutomaticPresentation(automata, padding_symbol='*', enforce_consistency=True, max_states=None)[source]#
Bases:
objectA 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)
- 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:
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^aritytherefore 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:
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:
UniformlyAutomaticClassA 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.
- 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.
- 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:
- Parameters:
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:
- class autstr.uniform.UniformlyAutomaticClass(automata, padding_symbol='*')[source]#
Bases:
objectA 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.
- 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:
- 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:
- 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:
- 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.