Release v4.0.0 - #46
Merged
Merged
Conversation
Formula strings are awkward to build programmatically and give no help with arities or variable names. `autstr/symbolic/` adds variables, relation and function symbols that compose with Python operators, over both a single structure (`AutomaticPresentation.symbolic`) and a uniformly automatic class (`UniformlyAutomaticClass.symbolic`). It is a frontend that lowers to nltk expressions, not a fourth engine, so `presentations`, `uniform`, `tree_presentations` and `implicit` consume it unchanged. Signature declares which relations are function graphs, which operators they bind to, and how Python values encode as elements; arities come from the automata, so a wrong-arity application is an error rather than a silently wrong query. Terms are flattened locally per atom. Cross-atom common subexpression elimination measured only ~9%, and hoisting witnesses is sound only for total functions -- not worth making correctness depend on an undeclared assumption. Two supporting fixes: * `evaluate(prepared_updates=...)` skips re-intersecting automata that this presentation already produced and that are known to be restricted to the universe. Re-injection had been re-preparing them: ~22% of runtime, 38% faster on a 328-state case, identical output. * `automata_tools.canonical()` keeps only convolutions with no all-padding column. `pad`/`unpad` deliberately leave the all-padding self-loops in place, so every non-empty relation looked infinite to a word-level cycle test. Finiteness is a question about tuples, not about words. Variables are renamed during compilation because nltk treats only `[a-df-z][0-9]*` as an individual variable and silently drops anything else from the free-variable list -- `R(foo,y)` yields free vars `['y']`, corrupting tape order with no error. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`autstr/arithmetic.py` becomes a signature plus an encoder/decoder: 803 lines down to 108. The old `VariableETerm`/`Term` API is gone -- the symbolic layer subsumes it, and keeping a second term algebra alongside it would mean two compilers to keep in agreement. The deleted per-term deepcopy was ugly but not slow: `deepcopy` of a `BuechiArithmeticZ` measures 0.13 ms and never appeared in the profile. The cost it was blamed for was the re-preparation now handled by `prepared_updates`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds an overview section on symbolic expressions, and migrates the README
snippet and the media script off the deleted `VariableETerm` API.
The arithmetic notebook claimed integer linear systems are "NP-hard in
general". They are not: whether Ax = b has an integer solution is decidable in
polynomial time via the Hermite or Smith normal form. Hardness needs *bounded*
variables -- that is integer linear programming. Reframed accordingly, with
subset sum as the smallest NP-complete case.
Each item is encoded as a variable constrained to {0, a_i} rather than as
a_i * e_i with e_i in {0,1}. The two-way choice is the bound, and it avoids
scalar multiplication entirely, which lowers to repeated addition over the
coefficient's bit length and dominates everything else: n=2 with 4-bit
coefficients goes from 16.6s/1.29GB to 0.09s/63MB, and the feasible size
moves from n=2 to n=4.
The instance is small on purpose and the text says so -- three items have
eight subsets. The point is that the automaton is built rather than searched,
so the unsolvable target is certified, not merely unsolved; the construction's
blow-up in the number of items is where the NP-completeness shows up.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The repository keeps notebooks output-free and the docs build executes them (`nb_execution_mode = 'force'`), but nothing enforced it. `pre-commit` was already a dev dependency with no configuration; this adds one. `--keep-id` matters: without it nbstripout renumbers every cell id to 0, 1, 2, ... and rewrites all five notebooks. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`FunctionCodec.encode` coerced its encoder's output with `list(...)`, which bakes the word-shaped engines into the generic layer: a tree encoding dies with "'Tree' object is not iterable" before it ever reaches a backend. The codec's output is only ever handed back to the backend that asked for it, so this layer has no reason to interpret it. `ElementCodec` now says so, and `FunctionCodec` returns the encoder's output unchanged. Behaviour-preserving for the string engines: both existing encoders already return lists. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`TreeAutomaticPresentation.symbolic()` gives the tree engine the same
expression language as the string engines. `Backend` was the right seam: the
compiler, the expression AST and `SymbolicContext` are unchanged, and a
signature's codec now encodes Python values to `Tree`s.
Three operations have no tree counterpart yet and raise with the reason
rather than quietly answering a different question:
* enumeration -- `iterate_language` walks word positions, and enumerating a
tree language in a well-defined order is a separate construction;
* finiteness -- needs the tree analogue of `automata_tools.canonical`, since
padding-saturated automata accept every tuple in infinitely many spellings;
* constants -- spliced in as a temporary relation, which the tree
presentation's `evaluate` does not yet accept.
Each message is asserted by a test, so none of them can start answering a
different question unnoticed.
Skolem arithmetic (N_{>0}, ·) is the oracle: products against Python
multiplication, nested terms, commutativity as a sentence, a non-square
witness, and divisibility against `b % a == 0`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two of the three gaps the tree symbolic layer shipped with. They land together because the backend and the test file each span both. **Constants.** `TreeAutomaticPresentation.evaluate` gains `updates`, mirroring the string version: relations installed for one evaluation only, prepared exactly as at construction time, so a spliced automaton is padding-saturated and domain-restricted before any projection sees it. Two deliberate differences: the restore sits in a `finally` (the string version restores on the success path only, so a query that raises leaves the temporaries installed -- a latent bug there, not copied here), and there is no `prepared_updates` fast path, which re-pads without re-restricting to the domain and is sound only because string `unpad` yields already-restricted automata. **Finiteness.** Three pieces: * `tree_automata_tools.canonical` -- the tree analog of the string version: keep only trees with no all-padding node. `attach_padding` accepts each tuple with arbitrary padding regions hanging below, so a saturated automaton's *tree* language is infinite whenever the relation is non-empty. Built from nine diagram entries rather than enumerating m^k symbols. * `SparseTreeAutomaton.co_reachable_states` -- the top-down companion that `reachable_states` lacked. * `SparseTreeAutomaton.is_finite` -- a state that occurs strictly below itself pumps, so the language is infinite exactly when the "child of" graph over reachable and co-reachable states has a cycle. Unlisted child pairs fall to the global default, so the analyses enumerate pairs over available states: quadratic, and documented as such, because a conservative over-approximation would invent cycles and wrongly report "infinite". Verified against an exhaustive oracle (60 random automata, splitting 28 finite / 32 infinite, so neither branch passes vacuously) using an exact bound: an accepted tree taller than the state count repeats a state and pumps, and an infinite language forces unbounded height since a binary tree's size is bounded by its height. Plus the Skolem oracle -- divisor pairs finite, multiples infinite -- and a test pinning both halves of why `canonical` is needed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The last two gaps. As with the previous pair, they land together because the backend and the symbolic test file each span both. **Enumeration.** `iterate_trees` yields accepted trees in shortlex order: by node count, then by labels in pre-order. Two things make it work at all, and both come from the finiteness step: * it builds trees only at states that are reachable *and* co-reachable -- trees at dead states can never become witnesses and otherwise dominate the cost; * a finite language has an acyclic "child of" graph, so the largest accepted tree has a computable size and the generator stops. Without that it climbed sizes forever after having yielded everything, which is how the first version ran into a timeout on the six divisors of 12. `canonical` comes first, or the saturated automaton would spell one tuple infinitely many ways and never reach the second. Shortlex orders by *encoding size*, which is what the string engine's length-lexicographic order does too -- there it coincides with increasing |n| only because a Buechi word is ceil(log2|n|) letters. A Skolem tree is the prime index plus the exponents' bit lengths, so 128 = 2^7 is enumerated before the prime 7. Value order belongs to the codec: for Skolem the magnitude order is not even recognizable, since every tree-automatic structure has a decidable theory while (N, *, <) does not. **Exists-infinity.** "k letters longer than every reference" becomes "k nodes deeper on one root-to-leaf path", with the same pigeonhole: pumping in a bottom-up tree automaton happens along a path via a context, and a tree's domain is closed under parents, so the reference-free nodes form a suffix of each path. The converse holds because a binary tree's size is bounded by its height, so infinitely many witnesses force one with a long enough path. `k_deeper_automaton` counts only nodes where the witness tape is present. `attach_padding` hangs all-padding regions below every tree, and those nodes have the references padded too -- counting them would invent depth carrying no witness and make exists-infinity true for finite fibres. That guard is load-bearing: removing it makes the automaton accept padding-only depth. It is pinned by a unit test, because the end-to-end tests could not tell the two implementations apart. Verified: enumeration against exhaustive filtering on 25 random automata; divisor pairs exactly, without repeats, terminating; infinite relations streaming lazily with every triple a true product; and for exists-infinity the discriminating pair on one relation -- every element has infinitely many multiples, no element has infinitely many divisors -- plus agreement with `is_finite` on the same fibre. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`UniformlyTreeAutomaticClass.symbolic()` needs no tree-specific backend, and this commit is the evidence rather than the implementation. `ClassBackend` reads `class_automata` for the arities and otherwise delegates to check / check_implicit / evaluate_implicit / get_structure, all of which the tree class already provides -- so the string class backend serves both engines unchanged. Verified side by side: identical tape order (['x', 'y', 'advice']), identical arities, identical refusals. That works because everything which would have to know about trees -- constants, enumeration, finiteness -- has no advice-free meaning over a class and is refused there for both engines. `get_structure` then hands back a TreeAutomaticPresentation whose own `symbolic()` supplies exactly those, via the tree structure backend. Six tests pin it against the string class, plus a comment on the class saying why no TreeClassBackend exists -- without it, adding one is the obvious next move for a reader. The symbolic layer now covers all four combinations: string structure, string class, tree structure, tree class. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`SymbolicContext.vars` splits a whitespace-separated string; `_names`, which
backs `.all()`, `.drop()` and `.exinf()`, did not. So `.all('x y z')` bound a
single variable literally named 'x y z', which occurs nowhere -- x, y and z
stayed free, and `check` existentially closes free variables. The query
answered a different question, with no error anywhere.
Found by cross-checking group commutativity against the formula-string API
after adding operator signatures: the symbolic layer called extraspecial
Z/3 abelian and the string engine did not. The string engine was right.
The layer's own test was complicit: `test_multiplication_is_commutative` used
`.all('x y z')` and passed, because Skolem multiplication really is
commutative -- the right answer for the wrong reason. The new regression tests
use `x + y = y`, where the universal is false and the existential true, so a
mis-bound quantifier cannot pass.
`_names` now splits like `vars`, and quantifying a variable that is not free
in the body raises instead of silently doing nothing -- the check `exinf`
already had.
That guard makes vacuous binders illegal, which
`test_substitution_avoids_capture_by_inner_binders` relied on to plant an
inner binder named '_v0'. It now conjoins a trivially true `v0.eq(v0)` so the
name genuinely occurs: same semantics, same intent, and the binder is still
there for substitution to dodge.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Only Buechi Z shipped a signature, so every other structure gave relations but no operators -- `(x * y).eq(z)` was unavailable everywhere. Worse, the family wrappers did not forward `symbolic()` at all: reaching the interface meant going through `.cls`. `symbolic()` now falls back to `default_signature()` on the presentation or class, and `SymbolicClassWrapper` gives the group and algebra families both the forwarding and their operator vocabulary. The families name their operation consistently, so the mapping is mechanical: M -> `*` for the non-abelian families, A -> `+` for FiniteAbelianGroups. Skolem arithmetic also gets its codec, so `(x * y).eq(12)` enumerates the divisor pairs. The operator follows the signature symbol, not member-by-member commutativity: IndexTwoCyclicGroups mixes abelian and non-abelian families in one class, so it gets `*` throughout. Not bound: `&`, `|` and `~` already mean the formula connectives, so lattice operations must stay methods -- the reason arithmetic spells `B` as `divided_by_power`. Inverse is not a relation of these classes, so no operator is wired to it. Known gap: FiniteAbelianGroups declares no equality relation, so `+` builds terms that cannot become formulas. Equality is missing from five families altogether; that is the next change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Equality is definable in most presentations here, but defining it costs an automaton construction that most queries never need, and for the wider graph classes that construction is expensive. `DeferredRelations` lets a structure register such a relation instead of building it: `get_relation_symbols` reports it immediately, and it materializes when something first asks. `materialize()` forces the construction -- what you want before pickling or reusing a structure -- and the constructors that register one take an eager flag for the same purpose. The query paths materialize whatever a formula mentions, so the formula-string API sees the relation transparently, and the symbolic backends now read arities through `relation()` rather than the automata dict, which is what triggers the build. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Five families declared none at all: FiniteAbelianGroups, FiniteBooleanAlgebras, and the six set-valued graph classes. Without one a term cannot become a formula -- `(x + y).eq(z)` is the only way to say what a term denotes -- so the operators added in the previous commit were unusable there. Each is defined from what the family already has, and registered rather than built: * FiniteAbelianGroups -- the identity is the unique idempotent, so `exists z0.(A(z0,z0,z0) and A(x,z0,y))`. The witness may not be called e0: nltk reads e-names as event variables and drops them silently. * FiniteBooleanAlgebras -- antisymmetry of the order, `Leq(x,y) and Leq(y,x)`. * the graph classes and MSO0-style set classes -- mutual inclusion, `Subset(x,y) and Subset(y,x)`, which is extensional equality of the vertex sets they take as elements. Skolem arithmetic and TreeExtraspecialGroups called equality 'E'; they now install it as 'Eq' and keep 'E' as an alias, so formulas written against the old signature still parse. That standardisation removes a live hazard. `operation_signature` had been guessing equality from the relation names, trying 'Eq' then 'E' -- but 'E' is the *edge* relation in every graph class, so the guess would have bound `.eq` to adjacency and silently answered "are these adjacent?" for "are these equal?". The name is now passed in explicitly and never inferred. `test_equality_is_not_adjacency` pins it on a graph where the two vertices are adjacent and not equal, so the two relations must disagree. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The docs build runs with -W, so these fail it. Two are the same RST mistake in docstrings I added: `Tree`s. Inline markup cannot be followed directly by a letter, so docutils reads the backtick as an unterminated start-string. Reworded to "`Tree` objects". The third was a cross-reference ambiguity on `Function`, and my first attempt at it was wrong: I spelled the reference out in the docstring, which changed nothing, because the annotation `Dict[str, Function]` generates a reference too. Reproducing the build locally showed the real cause -- `Function` is in `autstr.symbolic.__all__`, which makes autodoc document it a second time as `autstr.symbolic.Function`, so every bare reference has two targets. Dropping it from `__all__` leaves one target and resolves both references. The name stays importable from `autstr.symbolic`; only `import *` and autodoc are affected, and a signature's functions are built with `Signature.function` rather than by constructing one directly. A comment on `__all__` records why, so it does not get re-added. Verified by running the build the way CI does (sphinx -W --keep-going, with notebook execution off): 0 warnings, exit 0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
… into symbolic-interfaces
`AutomaticPresentation.evaluate(updates=...)` installs relations for one evaluation and restored them only on the success path, so a query that raised mid-build left the temporaries installed and every later evaluation silently answered against them. I noticed this while writing the tree engine's `evaluate` and said so in that commit message -- "a latent bug there, not copied here" -- but left it in place. Flagging a known bug is not fixing it. The regression test runs a failing query with `updates=` and asserts the relations are unchanged afterwards, which is what catches a restore that happens on only one path. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`InfiniteExtraspecialGroup(p)`: finitely supported a, b over F_p with a
one-digit centre, multiplied by
(a, b, c) * (a', b', c') = (a + a', b + b', c + c' + <a, b'>).
Unlike `ExtraspecialGroups` this is a single infinite structure rather than a
class of finite ones, so its elements have an advice-free encoding and can be
written as constants.
The multiplication automaton needs no guessing: the first letter carries the
centres, which fixes the pairing value the run must produce as c_z - c_x - c_y;
the rest of the word accumulates the sum of a_i * b'_i and acceptance compares
the two. Encodings trim trailing (0, 0) pairs, so they are unique and equality
is the diagonal.
It fills a real gap in what the library can test. Distinguishing `a * x` from
`x * a` -- the reflected-operand bug just fixed in `Term.__rmul__` -- needs a
structure that is both non-commutative and carries a codec, so that a plain
Python value can stand on the left. Skolem arithmetic has a codec but
commutes; the group classes do not commute but refuse constants, since a class
element's encoding depends on the advice. This structure is the first with
both, and reverting `__rmul__` to the unswapped form fails two of its tests.
Validated against a reference `multiply()` on 40 random pairs, with the
non-abelian sentence checked directly.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Symbolic interfaces
The first piece of the infinite-graph phase: a thin, engine-agnostic wrapper over an automatic or tree-automatic presentation that carries a domain U and a binary edge relation. It adds the graph vocabulary on top of the symbolic layer -- x.adj(y) for adjacency, plus .eq -- so every graph factory to come (ordinals, integer grids, the level-2 collapsible pushdown graphs) plugs into one surface, exactly as InfiniteExtraspecialGroup shares a presentation. The wrapper decides nothing itself; it forwards to the presentation, where FO(exists-infinity) is decided by synchronous projection. It works over either engine because both presentations expose the same relational interface. * `graph_signature` (next to `operation_signature`) binds `.adj` to the edge and `.eq` to equality. The edge name is passed in, never guessed -- `E` is the edge here but equality in Skolem, the hazard operation_signature already guards. * `InfiniteGraph` validates the edge exists and is binary, exposes `symbolic`, a decidable `is_symmetric` (so undirected-ness is checked, not assumed), and thin check/evaluate passthroughs. Vertices are Python values when a codec is supplied. Tested against Büchi arithmetic over Z with a formula-defined edge (x != y, the complete graph on Z), so the wrapper's mechanics are exercised without authoring any automaton; the concrete factories and their oracles follow. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The first genuine infinite graph on the new wrapper. Vertices are points of
Z^n; two are adjacent iff they differ by +/-1 in exactly one coordinate --
which is precisely the *asynchronous* product of n integer paths (move one
coordinate, hold the rest). So the grid is built by folding
`composition.direct_product(..., kind='async')` over n copies of a minimal
integer path, not by authoring an automaton.
* The path is a minimal {U, E, Eq} presentation cut from Buechi arithmetic;
its +/-1 edge is the FO formula `exists o. One(o) and (x+o=y or y+o=x)`,
where One is the least power of two. (This edge is, in miniature, a
one-dimensional FO-interpretation of the path in (Z, +) -- the pattern a
first-class `interpret` operation would package.)
* Vertices are Python n-tuples through a codec that handles the left-nested
pair encoding the fold produces; round-trips tested over [-3,3]^n.
* Async product of Eq comes out as full equality, so the grid keeps a correct
Eq for free.
FO is decidable (it is automatic); MSO is not (the grid interprets halting) --
the tidiest FO-vs-MSO contrast.
Tested against the ground truth sum(|delta_i|) == 1 across n = 1, 2, 3, plus
symmetry, no self-loops, codec round-trips, and Z^1 being 2-regular as a
first-order counting sentence.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Automatic structures are closed under FO-interpretations, and AutStr can *compute* the interpreted presentation because `evaluate(phi)` already returns the automaton of an FO formula's satisfying assignments -- so an interpretation is orchestration, not a new engine. It is the FO counterpart of the set / MSO interpretations that build the Caucal hierarchy, and the operation many structures (the grid, config graphs) are really instances of. `interpret(source, domain, relations)`: the new universe is the source elements satisfying the domain formula; each relation is an FO formula over the source's signature, permuted to its declared argument order. ~30 lines. Efficiency was the gate, and it is met for this phase: because elements keep the source's own encoding, the interpreted automata are the canonical minimal DFAs of the formulas. Measured -- interpreting the path in (Z, +) reproduces the hand-built grid path's automaton exactly, 15 states, and the test pins that equality. The k-dimensional case (elements as k-tuples) is deliberately not here: measurement showed it costs no extra states (minimization collapses the sparse-domain redundancy) but a bounded x-k symbol-width overhead, which wants an optional alphabet-pruning pass -- a separate, measured Phase 2. Tested: reconstructs the grid path (same canonical automaton), domain restriction (the even integers with induced order), argument-order permutation, and the validation guards. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Elements of the interpreted structure may now be k-tuples of source elements.
Gated on the measurement you asked for: a sparse domain does NOT blow up --
the diagonal {(a,a)} of Z^2, isomorphic to Z, gives a successor relation of the
same 10 states as the one-dimensional native encoding, because minimization
collapses the redundancy. The only cost is a bounded x-k symbol width,
intrinsic to representing tuples.
New primitive `NodeStore.fold_tapes` (+ `automata_tools.fold_tapes`): group
every k consecutive tapes into one tape over the product alphabet Sigma^k, by
cofactor reassembly -- the same shape as `map_letters`, but one new tape
consumes k old ones, so its cofactors range over all m**k combinations. This is
the piece that turns the many-tape automaton of a k-dimensional formula into a
structure whose elements are k-tuples. It is NOT a free regroup: for a
non-power-of-two alphabet num_bits(m**k) < k*num_bits(m), so the diagram is
genuinely rebuilt over fewer bits. Oracle-tested in isolation first (m=3,
k=2..3): 2400 acceptance checks, 0 mismatches.
`interpret` gains `dimension=k`. dimension 1 is exactly Phase 1 (the fold is a
no-op); for k>1 the formula automata are ordered coordinate-major and folded.
Decisive cross-check: a 2-dimensional interpretation of the grid reproduces the
composition-built IntegerGrid(2) exactly -- 51 states, same canonical automaton
from two independent constructions -- with the sparse-domain case pinned as a
regression.
Quotient interpretations (elements as classes of a definable equivalence)
remain the one deferred tier.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`_build_automaton` collapses a sentence to an all-accepting or all-rejecting
one-state automaton, but built it with `one()` / `zero()` and no alphabet, so
the marker carried the size-1 default. An enclosing connective then intersects
it with the domain, and the product fails with "requires same base alphabet"
on any structure whose alphabet is larger than the default -- every
product-alphabet presentation.
Latent until now because such presentations are new: `IntegerGrid(2).check('not
(exists x. E(x,x))')` triggers it, while the equivalent `all x.(not E(x,x))`
takes a different branch and worked. Threading `self.sigma` into the markers
fixes it. Found while building quotient interpretations.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`interpret(..., quotient=ε)`: elements become the classes of a definable equivalence. Built in two stages -- the plain interpretation carrying ε as a relation, then a one-dimensional interpretation restricting the universe to the shortlex-least representative of each class, "x is canonical iff x <= every y equivalent to it". So the whole thing stays first-order over the engine. New `automata_tools.shortlex_order`: the binary automaton for x <= y in shortlex order (length first, then lexicographic, trailing padding ignored) -- a well-order, so every class has a unique least element. Length is the primary key, so a lexicographic verdict on the common prefix must stay overridable by a later length difference; that needs five states, not three. Oracle-tested (7500 checks) and used to pick representatives. Verified: the quotient of Z by "x - y even" has exactly two classes. k-dimensional quotients are refused for now (a clear NotImplementedError): the representative predicate is a nested-quantifier sentence over folded relations, and folded (k>1) automata currently misbehave under the diagonal/complement those sentences use -- the domain and relations come out right, but the sentences do not. That fold bug is the next thing to chase; membership and simple queries on k-dim interpretations are unaffected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`_prepare_automaton` intersected tapes 0..arity-2 with `U` and left the last one alone, so a unary relation was never restricted at all. The tree engine's counterpart always did every tape; this was an off-by-one. The consequence is not a wrong relation but a wrong *sentence*. Quantifiers restrict a bound variable to `U`, so `all x. phi` asks whether `U` is contained in phi -- and an unrestricted relation disagrees with `U` on encodings that are not elements. In Buechi arithmetic over Z, `N0` accepted the single letter '0', which `U` rejects: interpreting a structure with domain `N0` therefore admitted a non-element into its universe, and `all x. Id(x,x)` came out False for literal identity `Id`. That is what blocked k-dimensional quotient interpretations. `fold_tapes` was never at fault -- it was suspected because k-dim interpretations were the first construct to build a universe out of `evaluate`, which is where the leak shows. The guard is lifted in the next commit. Three relations change: `N0` in Buechi arithmetic over Z, and `In` and `Subset` in MSO0 -- the unary and last-tape cases. The two serialized presentations carrying them are rebuilt, since the loaders deserialize with enforce_consistency=False; `scripts/gen_builtin_presentations.py` is the maintenance script for that. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Lift the dimension-1 restriction on `interpret(..., quotient=eps)`: with the universe leak fixed, the representative predicate -- "x is canonical iff x <= every y equivalent to it" -- is exact at every dimension, and the construction needed no change. Test: Z built from N alone, as N^2 quotiented by "same difference", with the order read off the representatives. It comes out a discrete unbounded total order that is not dense. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A subformula with no free variables evaluates to the all/none marker, whose single tape is a placeholder rather than a variable. The conjunction and disjunction branches renamed their operands' tapes into the enclosing formula's order, which is meaningless for a marker and, when the enclosing formula is itself a sentence, impossible: there is no tape to rename to, so `(all x. phi) & (all y. psi)` raised IndexError. Both branches now go through `_operand_automaton`, which remakes a sentence at the enclosing arity instead: false becomes the empty relation, true the product of universes -- not every word, so a true disjunct still admits no non-elements. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Kartzow's reachability construction decomposes every run into returns (a run from a stack to the one below it), loops (a run from a stack back to itself) and 1-loops, and everything downstream is a claim about which of these exist. This searches for them directly, by a bounded walk over configurations that prunes whatever each definition forbids -- the ground truth the computed sets will be checked against. Being bounded it under-approximates, which is the right direction: what it finds really is there, so every pair it exhibits must show up in a construction that claims to find them all. Two conventions worth naming, both forced by how the decomposition uses these sets. Asking for returns and loops of a WORD rather than of a stack means zeroing the level 2 links, which also makes them unusable -- exactly what the definition of a return demands, since a return may not use the links stored in the topmost word. And the run of length zero is a loop, so ExLoop and ExHLoop contain every (q,q); that is what makes "one operation followed by some loop" cover the bare operation too. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The summary of a word -- between which control states it has a return, a high
loop, a low loop and a 1-loop -- is what Kartzow's reachability construction is
built on, since which of those exist depends only on a stack's topmost word.
This computes them.
The paper's own effectiveness argument routes through mu-calculus model
checking on collapsible pushdown graphs, which is a decision procedure of its
own and no use to us. It is not needed. The decomposition lemmas the paper
proves are already a closed system of rules saying how each kind of run is
built out of shorter ones, and the least fixpoint of those rules is the
summary. The rules reach for the summaries of LONGER words -- pushing a letter
and dropping it again is how a run stays where it is -- so it is one
simultaneous fixpoint rather than an induction on length, taken over words up
to a bound that is raised until the summaries stop moving.
Two rules were not obvious and both came from the oracle disagreeing:
- a return may end with a pop AFTER pushing letters (the paper's condition is
that the word is a PREFIX of the topmost word, not equal to it), and since
pushing does not change the width, a return of the longer word lands
exactly where a return of this one has to;
- a 1-loop may grow the stack above, by pushing a letter and growing under
the longer word before dropping it again, or below, by dropping this letter
and growing under the word beneath -- not only by cloning the word itself.
Checked against the oracle on 400 random systems x 5 words x 5 sets: nothing
the search finds is missing from the computed summaries. That sweep also found
two bugs in the ORACLE, which are fixed here -- a high loop may push and pop
above the word freely and must only never drop below it, and a low loop may not
drop a level 2 letter at all, since the definition of a loop forbids passing
pop_1 except through level 1 links.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The reachability construction annotates a configuration tree with the summary of the word read from the root down to each node, which is how a bottom-up automaton consults a top-down computation: the check is local, and the annotation is quantified away afterwards. But the annotation needs letters of its own, and once it is gone the automaton is left reading a wider alphabet than the structure it has to be installed in. This narrows it again. Every letter kept must be one the automaton already reads, and what it did on the letters being dropped goes away with them -- one memoized pass over the diagrams, narrowing the digit blocks rather than rebuilding any transition table. The string engine's `recode` covers the opposite direction, widening, where a fresh dead state has to absorb the new letters; here nothing is new, so nothing has to absorb. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Kartzow's automata ask, at a node of an encoding tree, which returns and loops the stack that node stands for has -- and that stack's topmost word is the word read from the root DOWN to the node. A bottom-up automaton cannot read downwards, so the answer travels on a second tape, where the check is local: a node's annotation is its parent's extended by the node's own letter, and a separator carries its parent's along unchanged. A node's state is what its parent has to know about it, which is the annotation and the label, since the parent is where the two can be compared. Merging words into automaton states needed care. Two words with the same summary must have the same successors -- that is what makes the summaries the states of an automaton -- but the fixpoint is taken over words up to a bound, and a word at the edge has its own extensions pinned empty, so what it says about a letter is short of the truth. Comparing a word at the edge with an interior word then looks like an inconsistency in the theory when it is only an artifact of the bound. The criterion that works is not depth but growth: a summary can only grow as the bound rises, so one that agreed across two consecutive bounds has stopped growing and is the truth. Only those words are merged, and the merge is then checked against the fixpoint it came from -- walking the merged automaton must reproduce the summary of every stable word. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The first of the four relations reachability decomposes into. Kartzow's characterisation makes the run a walk up the tree's last path -- a high loop, then one pop or level 1 collapse, repeated -- so every check is local if the guess at a letter carries the states the run is in BEFORE and AFTER dropping it. The state after one drop is the state before the next, which is what the parent compares; the high loop comes from the summary the annotation names, so a node needs nothing but its own four tapes. The shape had to be measured rather than guessed. Encoding pop_1^k(s) is encoding s with a tail of the last path deleted, and -- this is the part I got wrong twice -- with a separator added exactly when one is deleted, never otherwise and never more than one. Letting the separator appear freely made a CLONE look like a chain of pops, since cloning also just hangs a separator at the end; requiring it to pair with a deleted one is what tells the two apart. The last word's divergence from the word below it moves up, and that is the whole content of the added separator. The two scaffolding tapes come off afterwards: the annotation is pinned to the real one by intersecting with its own automaton, both are projected away, and the alphabet is narrowed back to the one configurations are written in. Checked against a brute-force search over arbitrary configurations -- not just reachable ones, since the relation is about all of them -- on 15 systems, 12 of them random, some 11000 pairs, no disagreements. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
B read backwards, and the same tree shape with the two configurations exchanged. What is not symmetric is the guard. A pop is guarded by the letter it takes off, so the node that loses it can check the move alone; a push is guarded by the letter already on top, which is the one ABOVE the letter written. So the chain carries each node's label up to its parent, and the push is checked there. That is still not enough, because the letter may go below a separator -- the last word of a stack whose last two words agree hangs under one -- and then the guarding symbol is not the parent's label either, but the nearest letter above it. The annotation already knows: a summary carries the topmost symbol of the word it names, so the guard comes from the annotation rather than from any label. The high loop belongs to the node naming its word, the push to the node above. Both directions of failure showed up on the way and each pointed at one of these: taking the pushed letter as its own guard accepted runs that do not exist, and reading the guard off the label rejected runs that do. Checked against the search on the same 15 systems as B, some 22000 pairs in all, no disagreements. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The third relation, and the first that is not finished. Kartzow's decomposition allows a run of A three kinds of piece: a return, a 1-loop then a level 2 collapse, and a 1-loop then a pop that some later collapse closes off. This builds the returns. That turns out to be more than it sounds. A collapse that drops a SINGLE word is already inside a return -- the summaries count a pushed link collapsed after a 1-loop as one, which is the escape rule Phase A needed -- so what is missing is only the collapse that spans several words at once, which is what the other two pieces exist for. Measured: exact on systems that never collapse on a level 2 link, exact on one that collapses over a single word, and 38 pairs short on one that pushes a link, clones, and then collapses over all of it. Nothing is ever invented, in any of them, so the relation stays inside the truth and `collapses_on_links` says when it may fall short of it. The words dropped are the encoding's separators, and the run pops them from the last backwards -- so within a subtree the chain runs through the right child's separators, then the left child's, then the node itself, which is reverse traversal order. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The piece of Kartzow's decomposition that looked hardest turns out to be local
after all. A level 2 collapse drops the stack to the width its link records,
which sounds like a link reaching across the tree -- but the link records the
number of separators up to its letter, and the stack it points at is the
tree's prefix at that separator, which is exactly where the region being
deleted begins. So a 1-loop-and-pop group followed by a 1-loop-and-collapse is
a chain climbing that region's own top path, closed off by its root, and it
then contributes a pair of states to the outer chain just as a return does.
The encoding is what makes this work, and it is why Kartzow chose it.
Three things had to be right and none of them was, at first:
- The 1-loop before a step may leave the stack where it was. A collapse
straight off the top is not a return -- it drops more than one word -- so
nothing would have covered it.
- The chain's next node may hang to either side: a letter's continuation is
its left child, a separator its right, and the last path takes whichever
is there. Assuming the left one silently lost every case where a word ends
at the letter being collapsed on.
- Where no word comes off at all, A and B admit only the empty run, since
their condition already fails at step zero -- the stack a run starts on is
a substack of itself. A loop that stays put belongs to C, whose condition
excludes only the PROPER substacks. My oracle had this wrong for A and read
38 real absences as failures; C had it wrong the other way and needed the
high loop added.
Checked on a system whose only rule is a collapse, so that no return exists
anywhere in it, and where the stack still drops two words in one step: nothing
but this piece can account for it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The fourth relation and the formula that puts the four together. The formula is
the easy half: reachability is A;B;C;D, all four reflexive, so it is
Reach(x,y) = exists u,v,w. A(x,u) & B(u,v) & C(v,w) & D(w,y)
evaluated over a scratch structure whose domain is the encoding trees. It
builds -- 41 to 117 states on the systems tried, a second or two -- and is only
ever as good as the four it composes.
D is not there yet, and this commit records where. Kartzow's Cor. 4.10 walks
the milestones of the stack being built, which the encoding puts in traversal
order, one per node; the run only ever moves forward through them, which is
what decides where each operation goes. Two readings of that have now been
wrong in opposite directions:
- cloning where the two words part lets a word be shorter than the copy it
came from for nothing, which no system need allow;
- cloning at the deepest point and popping back up loses the plain clone,
because the step from the last shared node into the new word is then never
paid for.
What both miss is the GENERALISED milestones: between one word and the next the
run passes through the previous word cloned WHOLE, and only then pops it down
to where the two part. That intermediate stack is not the LeftStack of any
node, which is exactly why Kartzow carries a second correspondence for it, and
why guessing a state per node is not enough on its own.
A, B and C are unaffected and stay checked against the search. The failing case
is kept as an xfail rather than deleted, so the next attempt has something to
aim at.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The last of the four relations, and with it Reach = A;B;C;D actually works:
checked against breadth-first search, and -- the test that mattered --
reflexive and transitive as first-order properties of the relation built.
D walks the milestones of the stack being built. Measuring that walk rather
than reasoning about it gave three moves and no others: a push to a left child,
a clone to a right child, and an ascent that clones at the DEEPEST node reached
and then pops one letter per level, each node giving up its own, a separator
having none to give. Cloning at the deepest point rather than where the words
part is the whole of it -- the other way round lets a word be shorter than the
copy it came from for nothing.
Five bugs, each found by a check the one before it could not have caught:
- The run only ever moves forward through the milestones, so there is no
walking back up and cloning afterwards.
- A leaf can be the run's end or a pass-through, and a table has one entry
per key; which of the two it is belongs on the tape.
- Likewise which state the run began in: two starts wanted the same entry
and the second was quietly winning.
- The state comes up from the child, so it is the CHILD's label an ascent
names, not the parent's.
- The loop after a pop belongs to the word the PARENT names.
Three more came out of Reach itself, none of them in D:
- B missed the letter that is dropped but not deleted -- when the word below
shares it, the letter stays and only the separator moves up.
- The summaries' merged automaton has to be CLOSED, every reachable summary
having a transition for every letter, all witnessed by words that have
stopped growing. Short of that a real word has no summary, which surfaces
as a tree that cannot be annotated at all.
- A let a deleted separator pass as inert, so dropping two words was paid for
with one return. A separator may only be inert below the letter an F2 group
collapses on, which is a different region and now says so on the tape.
The last of those was caught by transitivity, on configurations no bounded
sweep had reached: x = 0 ⊥:⊥a, y = 1 ⊥:⊥a:⊥a, z = 0 ⊥, where that system only
ever cycles. A sweep over small stacks is a weak oracle; asking the built
relation whether it is transitive is a strong one, and it belongs in the tests
for good.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The last piece. Kartzow's regular reachability constrains a run by the labels it reads, and where he builds the label automaton into the reachability automaton, here it goes into a PRODUCT SYSTEM whose ordinary reachability is the answer. What is left is to say that the two configurations are the plain ones underneath -- same stack, control state tagged with the label automaton's initial state at one end and an accepting one at the other: Reach_L(x,y) = exists u,v. Tag_p0(x,u) & Reach(u,v) & (or_f Tag_f(y,v)) Both kinds of configuration share a structure for the length of that formula, which is why the encoding can carry root letters for a second system's states, and the alphabet is narrowed again once the tags are quantified away. An epsilon-contraction needs nothing further: it is the case of any number of silent labels followed by one other. `Reach` is now a relation of the configuration graph like any other, so a first-order formula may ask about runs of any length -- the question `autstr.turing` cannot answer, and the reason these graphs are on the tree engine at all. It is declared from the start and built the first time a query mentions it, since it is exponential in the number of control states; that deferral is the opt-out, and no flag is needed. `reach_along` installs a label-constrained version under a name of the caller's choosing. Checked against a search that tracks the labels it reads, on four constraints: an exact word, a two-letter word, everything (which is shown to give back plain reachability), and the contraction shape. The graph's own reachability is checked to be reflexive, transitive, and to contain the edge relation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Its lead-in ended in an em dash, so docutils read the aligned rules as a definition list whose last two terms lack a definition, and the docs build warned. `::` is what the rest of the module already uses. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Reachability for level 2 collapsible pushdown graphs
Two changes that turn out to be one. `.symbolic()` could be called with no
arguments on nine of the library's structures, because each declares a
`default_signature` naming its operators and the codec that turns Python values
into elements. It could not on Büchi arithmetic or MSO0: those were built by
plain functions returning a bare presentation, with nowhere to hang a
signature. `autstr.arithmetic` existed to fill that gap -- for ONE of the three,
which is what made it look like a second, rival interface.
So the signature moves onto the presentation, where the rest of the library
keeps it, and the module that worked around its absence goes away. All three
gain their codec, verified against the automata rather than assumed:
- N: binary, least significant bit first (checked against A(x,y,z)),
- Z: sign symbol then magnitude (as before),
- MSO0: a set as a bitmask, position i set iff i is a member, in CANONICAL
form -- the universe rejects trailing zeros, so {0} is `1` and the empty
set is the empty word (checked against Subset over all subsets of {0,1,2}).
MSO0 therefore gains an interface it never had: union, intersection and
difference as `+`, `*`, `-`, and solutions that come back as Python sets.
`buildin` was the other half of the same confusion: every structure the library
ships is built in, so the name carved nothing. Its contents move to where their
subject already lives -- `arithmetic` (Buechi N and Z), `powerset` (MSO0),
`tree_arithmetic` (Skolem, matching algebra/tree_algebra), and the generic
automaton constructors to `utils.automata_tools`, which was already importing
`one` from across the package boundary. `CompiledPresentation` holds the part
the presentations share.
The precompiled `.autstr` artifacts go too. They saved 0.03s, 0.23s and 0.44s
against building from scratch, and the built presentations are identical to the
loaded ones relation by relation. Serialization stays fully supported; it just
stops shipping artifacts nobody needed.
BREAKING: `autstr.buildin.*` is gone, as are `autstr.arithmetic.integers` and
`signature`; encode/decode are now classmethods on the presentations.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The abelian-groups cell was labelled "has an element of order 4" and asked for
an element of order 2: `A(x,x,x)` spells x = 0, so `A(x,x,z) and A(z,z,z)` says
2x = 0. Z/2 alone satisfied it. The corrected formula asks for y = 2x, z = 2y = 0
with x and y both nonzero, which separates the two groups of order 4 -- Z/4 has
such an element, Z/2 + Z/2 does not.
That cell is also where the symbolic interface earns its place: with `+` and
`.eq` the query reads as the mathematics, and a class has no constant symbols,
so the identity is named by what defines it (t + t = t).
MSO0 gains its codec's payoff: union, intersection and difference as `+`, `*`,
`-`, membership and subset as methods, and solutions that come back as Python
sets -- the eight ways to split {0,1,2} in two, enumerated from the automaton.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The composition notebook becomes "building new structures from old": the
integers constructed from the naturals as a 2-dimensional quotient
interpretation, which is small enough to read and real enough to be worth
saving. It carries the codec story -- the construction is correct but
illegible until a codec says that the pair (a, b) denotes a - b -- and closes
on the shipped example of the same idea, `autstr.ordinals`.
A new notebook, `infinite_structures`, covers what had none: the integer grid,
the regular tree, Turing configuration graphs and level 2 collapsible pushdown
graphs. The last two are the point. Both present computation as a graph and
both have a decidable first-order theory, but reachability is the halting
problem for one and a relation of the other -- so `Reach` is there to be
queried, and transitivity over all runs of all lengths is decided in under a
second.
Writing those two turned up three real defects, none of which any test saw:
- ENUMERATION WAS BROKEN for every interpreted structure of dimension > 1,
including the shipped `Ordinal(2)`. `iterate_language` built each tape by
string-concatenating letters, which holds only while a letter is one
character; over a product alphabet a letter is a tuple, and str() flattened
('0','1') into text no codec could read. Tapes are tuples of letters now.
Membership worked throughout, which is why this went unseen.
- SERIALIZING SUCH A PRESENTATION could not be reloaded: JSON has no tuples,
so the alphabet came back as a set of lists (unhashable) and the padding
symbol as a list. Both are restored on load.
- The v2 back-compat loader lost its only test when the `.autstr` artifacts
went away -- `test_the_legacy_flat_payload_still_loads` was left building a
presentation and querying it, touching no legacy payload at all. It now
constructs a v2 payload by hand and reads it.
Also: the abelian-groups notebook cell and `is_deterministic`'s docstring, which
still said reachability was not built.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The countable atomless Boolean algebra had no notebook coverage. It sits next to the finite Boolean algebras, where the contrast is the point: finite ones are powersets and full of atoms, and dropping finiteness leaves exactly one countable algebra in which every nonzero element splits forever. Its elements are trees, so it is the tree engine's turn. Bipartiteness in the graphs notebook now appears twice: as the formula string, and built from `symbolic()` with `.implies`, `.all` and `.drop`. A set variable is just a variable, which is what makes the query monadic second-order, and the symbolic form makes that legible instead of nesting six parentheses. Checked to agree with the string form on all three of that cell's graphs. `infinite_structures` joins the documentation's notebook toctree. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The README carried the whole release history, which made it long and made the history shallow -- there was never room to say what a release actually changed. CHANGELOG.md takes it over, with v4.0.0 written out properly: what was added, what moved, what was fixed, and an upgrade path from 3.x. The docs build copies it in, so it has a page on the site too. What stays in the README is what only the README can say: the AI-assisted algorithm engineering narrative, the gource animation, the highlights of the newest version, and a link to the rest. The quick start now opens on the symbolic interface -- which is the honest entry point, and was also the one broken example in the file, since it still imported a class that the arithmetic rewrite deleted a release ago. Version 4.0.0 rather than 3.2: `autstr.buildin` is gone, `autstr.arithmetic` holds something else, and the old term-algebra front end has no replacement of the same shape. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Gource over the full commit history, now reaching the symbolic layer, the interpretations, the infinite graphs and the collapsible pushdown work. The sieve automaton is unchanged, byte for byte -- the example it renders did not move. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The string side had it and the tree side did not, which put the expensive constructions on the wrong side of the line: a tree relation is where the cost lives, and `Reach` for a collapsible pushdown graph is exponential in the system's control states. It turned out to be a short walk. A tree automaton's compiled form is a sorted table of child pairs with one decision-diagram root each, so the payload is the pair keys plus the shared sub-DAG below those roots -- and `STORE.export` / `import_nodes` are generic over roots, so the diagram half needed no new code. A relation over a convolution alphabet too wide to enumerate still writes out in the size of its diagrams, exactly as on the string side. Two deliberate differences from the string presentation serializer: each automaton's payload is stored as raw bytes with a length prefix rather than as a JSON list of integers (which costs about four bytes of file per byte of data), and the JSON-has-no-tuples fix moved to `utils.misc` instead of being copied, since both engines need it now. Measured on the case it exists for: the collapsible `Reach` presentation is 22709 bytes, reloads in 0.01s against 0.5s to rebuild, and the reloaded relation is still reflexive, still contains the edge relation, and is still transitive. Skolem arithmetic round-trips and answers identical queries; a flipped payload byte is caught by the checksum. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The README carried eleven references and the documentation none, which is backwards -- a reader of the docs meets the constructions and has nowhere to follow them. `references.md` now holds the bibliography, grouped and annotated with what each work IS in this library, and the README keeps the four it leans on hardest plus a link. Citing where it was due exposed a gap: the overview had no section on any of the v4 material. It gains two -- interpretations (with the tree quotient's least description, and the ordinals as the payoff) and infinite graphs (the grid, the tree, Turing configuration graphs, and the collapsible pushdown graphs where reachability comes back). Each names its source at the point of use: Kuske & Weidner and Colcombet & Loeding on tree quotients, Delhomme on why `Ordinal` takes an exponent, Kartzow on the encoding and the run decomposition, Courcelle on the linear-time claim, Abu Zaid/Graedel/Reinhardt on advice. Three entries had no bibliographic details anywhere in the repository and could not be verified offline (Delhomme 2004, Oum & Seymour 2006, Colcombet & Loeding 2007); they carry author, title and venue but no DOI, pending a check. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
All four now carry a DOI, and one annotation was wrong.
Delhomme 2004 -> 10.1016/j.crma.2004.03.035 (CR Math. 339(1), 5-10)
Oum & Seymour -> 10.1016/j.jctb.2005.10.006 (JCTB 96(4), 514-528)
Colcombet & -> 10.2168/LMCS-3(2:4)2007 (LMCS 3(2:4), 1-36)
Loeding
Kuske & -> 10.1007/978-3-642-22993-0_39 (LNCS 6907, 424-435)
Weidner
Kartzow -> 10.2168/LMCS-9(1:12)2013 (issue was 9(1:12), not 9(1))
Oum & Seymour is the one that needed care. A publisher's abstract page claims
rank-width is not defined there, which would have made it the wrong citation
for `RankWidthClass`; Oum's own later survey settles it -- "Rank-width was
introduced by Oum and Seymour [71]", where [71] is exactly this paper. The
entry now says so, as the branch-width of the cut-rank function.
Colcombet and Loeding's role is stated more carefully too: the existence of
injective presentations for tree-automatic structures, which is what makes a
quotient interpretation well posed over trees, with Kuske and Weidner making it
effective.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Release preparation for v4.0.0
Contributor
There was a problem hiding this comment.
Pull request overview
Release PR that merges dev into main for v4.0.0, introducing a new symbolic first-order API, first-order interpretations, new infinite-structure presentations (including Turing configuration graphs), and tree-engine serialization, while removing the legacy autstr.buildin module and updating docs/tests/notebooks accordingly.
Changes:
- Add the symbolic layer (
autstr.symbolic) with signatures/codecs, backends, and compilation to existing evaluation engines. - Add new/expanded structures and utilities (e.g.,
autstr.infinite_graphs,autstr.powerset.MSO0,autstr.tree_algebra, tree automaton finiteness/enumeration helpers, and tree presentation serialization). - Perform the v4.0.0 migration (module moves away from
autstr.buildin, version bump, packaging/docs updates, new regression tests).
Reviewed changes
Copilot reviewed 75 out of 80 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/test_turing.py | Adds tests for Turing machine config graphs, codec, step relation, and FO boundary. |
| tests/test_tree_uniform.py | Adds tests ensuring symbolic interface works for uniformly tree-automatic classes. |
| tests/test_tree_presentations.py | Updates imports for module moves; adds regression tests for sentences under connectives (tree engine). |
| tests/test_tree_automata.py | Adds finiteness/enumeration oracle tests and imports iteration helpers. |
| tests/test_tree_algebra.py | Adds tests for the atomless Boolean algebra structure, codec, and operations. |
| tests/test_symbolic_tree.py | Adds tree-engine symbolic layer tests using Skolem arithmetic as oracle. |
| tests/test_skolem.py | Updates imports due to autstr.buildin removal. |
| tests/test_serialization.py | Adds serialization regression tests (including legacy v2 payload) and tree serialization tests. |
| tests/test_regular_tree.py | Adds tests for RegularTree codec, relations, and graph properties. |
| tests/test_presentations.py | Adds invariants/regressions for universe restriction and sentence markers under connectives. |
| tests/test_interpretations.py | Adds interpretation tests (domain restriction, dimension, quotient, validation). |
| tests/test_integer_grid.py | Adds tests for IntegerGrid codec and adjacency semantics. |
| tests/test_infinite_graphs.py | Adds tests for the InfiniteGraph wrapper surface and symmetry behavior. |
| tests/test_infinite_extraspecial.py | Adds tests for the new infinite extraspecial group and operand order in symbolic terms. |
| tests/test_equality.py | Adds tests for deferred equality construction across families and structures. |
| tests/test_automata_tools.py | Adds tests for fold_tapes, shortlex_order, and partial_dfa. |
| tests/test_arithmetic.py | Rewrites arithmetic tests to use symbolic interface and adds MSO0 set tests. |
| scripts/gen_readme_media.py | Updates README media generator to use symbolic arithmetic interface. |
| pyproject.toml | Bumps version to 4.0.0 and removes autstr.buildin package-data artifacts. |
| notebooks/groups.ipynb | Updates examples to symbolic interface and keeps notebooks output-free. |
| notebooks/graphs.ipynb | Adds symbolic example snippet for graph classes. |
| notebooks/composition.ipynb | Expands notebook to include interpretations/serialization narrative and examples. |
| docs/source/references.md | Adds new references page for foundational and project citations. |
| docs/source/overview.md | Updates overview for v4 features: symbolic layer, interpretations, infinite graphs, tree notes, references. |
| docs/source/index.rst | Adds changelog/references to toctree and includes infinite structures notebook. |
| docs/source/conf.py | Copies CHANGELOG into Sphinx tree for a dedicated docs page. |
| docs/media/history.gif | Updates LFS pointer for history animation. |
| CHANGELOG.md | Adds full v4.0.0 changelog and upgrade guide. |
| autstr/utils/misc.py | Adds alphabet_from_json helper for tuple restoration during serialization. |
| autstr/uniform.py | Adds SymbolicClassWrapper, deferred relations support, and symbolic interface for classes. |
| autstr/tree_uniform.py | Documents symbolic backend reuse for tree classes. |
| autstr/tree_presentations.py | Adds TreeAutomaticPresentationSerializer, deferred relations integration, and safer evaluate(..., updates=...). |
| autstr/tree_groups.py | Adopts SymbolicClassWrapper and standardizes equality naming/aliasing. |
| autstr/tree_graphs.py | Adopts SymbolicClassWrapper and installs deferred extensional equality for set-valued graph classes. |
| autstr/tree_arithmetic.py | Renames/moves Skolem arithmetic module and adds default symbolic signature with codec. |
| autstr/tree_algebra.py | Introduces AtomlessBooleanAlgebra structure with deferred definable relations and symbolic signature. |
| autstr/symbolic/signature.py | Adds signature model, codecs, and helper signature constructors (operation/order/graph/relational). |
| autstr/symbolic/compiler.py | Adds compilation from symbolic AST to NLTK expressions, including term flattening and name mangling. |
| autstr/symbolic/backends.py | Adds structure/class/tree backends for evaluation, membership, enumeration, and finiteness semantics. |
| autstr/symbolic/init.py | Exposes symbolic public API. |
| autstr/sparse_tree_automata.py | Adds finiteness analysis and binary serialization for tree automata. |
| autstr/sparse_automata.py | Uses alphabet_from_json when deserializing product alphabets. |
| autstr/powerset.py | Adds MSO0 presentation with encode/decode and symbolic signature for set operations. |
| autstr/mtbdd.py | Adds fold_tapes diagram transformation. |
| autstr/infinite_graphs.py | Adds InfiniteGraph, IntegerGrid, and RegularTree factories with codecs and symbolic surface. |
| autstr/groups.py | Adopts SymbolicClassWrapper; adds InfiniteExtraspecialGroup structure. |
| autstr/graphs.py | Adopts SymbolicClassWrapper for set-valued graph classes and supports deferred equality. |
| autstr/cocycle_groups.py | Adopts SymbolicClassWrapper for cocycle rank-width groups. |
| autstr/buildin/automata.py | Deletes legacy buildin automata module (moved to utils and refactored). |
| autstr/buildin/init.py | Remains as stub/placeholder after buildin removal. |
| autstr/algebra.py | Adopts SymbolicClassWrapper and deferred equality for finite Boolean algebras. |
| autstr/_version.py | Bumps __version__ to 4.0.0. |
| .pre-commit-config.yaml | Adds nbstripout to keep notebooks output-free while preserving cell ids. |
| .gitignore | Ignores generated docs/source/changelog.md. |
| .github/workflows/publish.yaml | Updates smoke test import paths for v4 module moves. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+238
to
+240
| Min="(forall z. not Subset(z, x)) or " # Empty set case | ||
| "(Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(y, z)))", | ||
| Max="Sing(y) and Subset(y, x) and forall z. (-(Sing(z) and Subset(z, x)) or Leq_sing(z, y))", |
`Min` carried a disjunct for "the empty set case" that no set satisfies: `forall z. not Subset(z, x)` is refuted by z = x, since Subset is reflexive. Confirmed twice over -- `exists x.(all z.(not Subset(z,x)))` is False over the structure, and removing the disjunct leaves the same language and the same five states. What it hid is worth writing down. Min(empty, y) is empty, which IS the right semantics -- the empty set has no least member -- but by accident rather than by the guard that claimed to arrange it. The comment now says so, and a test pins it, since the behaviour was neither documented nor asserted anywhere. `Max` never had the disjunct, so the two now agree. The other two: the buildin rename inserted an import above an existing one in two test modules, leaving a duplicate import with an assignment wedged between. One import block, assignment after it. (test_arithmetic.py had the same shape already correct.) Found by Copilot's review of #46. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The suite is CPU-bound and its tests are independent, and we were running it on one core of sixteen. `pytest-xdist` joins the test extra and CI runs `-n auto`. serial 11:06 -n auto (16) 3:54 -n 4 3:56 The two parallel figures being equal is the interesting part: past four workers there is nothing left to divide, because the wall time is one test. `TestClaimAndVerifyChainRing::test_check_implicit_ring` takes 194s of the 234s total -- nested existentials over Z/4 members through the functional-atom path, which is exactly the case that exists to be expensive. Next after it are 101s (`test_tree_multiplication_and_sentence_z4`) and 44s (a regular-reachability search), so the floor is set by a handful of deliberately heavy tests rather than by breadth. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Cascades
devintomainfor the v4.0.0 release: 85 commits, 80 files,everything since the v3.1.0 tag.
The full account is in CHANGELOG.md; the headlines:
A symbolic first-order layer (
autstr.symbolic). Write(x + y).eq(z) & z.lt(100)instead of a formula string, over any structure orclass, on either engine. Every structure declares its own operators and its own
codec, so Python values go in and come out and
symbolic()needs no arguments.First-order interpretations (
autstr.interpretations) that compute theinterpreted presentation, quotients included — over trees too, where no order
is well-founded and the representative of a class is its least description.
Infinite graphs (
autstr.infinite_graphs,autstr.turing): the integergrid, the regular tree, and Turing-machine configuration graphs, where
first-order logic stops exactly at reachability.
Level 2 collapsible pushdown graphs with reachability
(
autstr.collapsible,autstr.collapsible_reach). Tree-automatic by Kartzow'sencoding, and
Reachis a relation of the graph — so a first-order formula mayask about runs of any length, which is precisely what the Turing graph cannot
be asked.
The countable atomless Boolean algebra, the ordinals below ω^ω and
ω^(ω^n), and serialization for the tree engine.
Breaking changes
autstr.buildinis gone — every structure the library ships is built in, soits contents moved to modules named for their subject:
autstr.buildin.presentationsautstr.arithmetic,autstr.powersetautstr.buildin.tree_presentationsautstr.tree_arithmeticautstr.buildin.automataautstr.utils.automata_toolsautstr.arithmeticnow holds the Büchi presentations themselves; the oldterm-algebra front end is replaced by the symbolic layer. The precompiled
.autstrartifacts are gone (they saved 0.03–0.44 s and were a second sourceof truth). The changelog has the upgrade path.
State
-W --keep-going, every notebook executed.After the merge
Publishing is
workflow_dispatchonpublish.yaml(TestPyPI first, thenPyPI), or a GitHub Release for the PyPI path. The plan is: publish to TestPyPI,
install from there into a clean environment and run the suite against the
installed package, then repeat for PyPI.
Generated with Claude Code