Symbolic interfaces - #36
Closed
fariedabuzaid wants to merge 20 commits into
Closed
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>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR introduces a new symbolic-expression frontend (autstr.symbolic) that lets users build first-order terms/formulas with Python operators instead of formula strings, and wires it through both string- and tree-automatic backends (structures and uniformly automatic classes). It also adds deferred/lazy construction for expensive definable relations (notably equality), plus new tree-automata tooling and tests to validate finiteness/enumeration and the symbolic layer across engines.
Changes:
- Add
autstr.symbolic(AST, signature binding, compiler to NLTK formulas, evaluation backends) and comprehensive tests for both word and tree engines. - Add
DeferredRelationsto support lazily-constructed relations (e.g., equality), and adopt it across presentations/classes/families. - Extend tree-automata utilities with canonicalization, finiteness checking, and shortlex enumeration; refactor Büchi arithmetic API to expose a symbolic structure (
integers()).
Reviewed changes
Copilot reviewed 32 out of 32 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/test_tree_uniform.py | Adds tests asserting the symbolic class interface works for uniformly tree-automatic classes. |
| tests/test_tree_tools.py | Adds tests for k_deeper_automaton used by exinf in the tree backend. |
| tests/test_tree_automata.py | Adds oracle-based tests for tree-language finiteness and enumeration. |
| tests/test_symbolic.py | New test suite covering the generic symbolic interface over word presentations. |
| tests/test_symbolic_tree.py | New test suite covering symbolic evaluation over tree presentations. |
| tests/test_equality.py | New tests validating deferred/lazy equality construction across families. |
| tests/test_arithmetic.py | Refactors arithmetic tests to use the new symbolic integers() API. |
| scripts/gen_readme_media.py | Updates README-media generation to use the symbolic arithmetic API. |
| notebooks/arithmetic_and_algebra.ipynb | Updates notebook to the new symbolic arithmetic API and adjusts narrative. |
| docs/source/overview.md | Documents the symbolic interface and shows new usage examples. |
| autstr/utils/tree_automata_tools.py | Adds tree canonicalization, k_deeper_automaton, and shortlex enumeration support. |
| autstr/utils/automata_tools.py | Adds word-level canonicalization for tuple-finiteness/cycle checks. |
| autstr/uniform.py | Adds SymbolicClassWrapper, integrates DeferredRelations, and adds class-level symbolic(). |
| autstr/tree_uniform.py | Documents/clarifies that class-level symbolic support is inherited and backend-agnostic. |
| autstr/tree_presentations.py | Adds deferred-relations support and a tree-structure symbolic backend integration. |
| autstr/tree_groups.py | Adopts SymbolicClassWrapper and standardizes equality naming (Eq with E alias). |
| autstr/tree_graphs.py | Adopts SymbolicClassWrapper and introduces deferred extensional equality for set elements. |
| autstr/symbolic/signature.py | New: declares Signature, operator bindings, function graphs, and element codecs. |
| autstr/symbolic/expr.py | New: immutable AST for terms/formulas with operator overloading and quantification helpers. |
| autstr/symbolic/context.py | New: user-facing symbolic context, symbol lookup, evaluation surface, and relation wrapper. |
| autstr/symbolic/compiler.py | New: compiles symbolic AST to NLTK expressions with safe variable renaming and term flattening. |
| autstr/symbolic/backends.py | New: backends for word/tree structures and uniformly automatic classes (incl. exinf support). |
| autstr/symbolic/init.py | New: package exports for the symbolic layer. |
| autstr/sparse_tree_automata.py | Adds co-reachability and finiteness checking for sparse tree automata. |
| autstr/presentations.py | Introduces DeferredRelations, adds symbolic(), and supports “prepared updates” fast path. |
| autstr/groups.py | Adopts SymbolicClassWrapper and deferred equality for relevant families. |
| autstr/graphs.py | Adopts SymbolicClassWrapper and deferred extensional equality for set-valued graph classes. |
| autstr/cocycle_groups.py | Adopts SymbolicClassWrapper to expose symbolic access at the family wrapper level. |
| autstr/buildin/tree_presentations.py | Standardizes equality symbol (Eq) for Skolem arithmetic and provides default signature. |
| autstr/arithmetic.py | Replaces the old custom term layer with a symbolic integers() structure and codec. |
| autstr/algebra.py | Adopts SymbolicClassWrapper and deferred equality for boolean algebras. |
| .pre-commit-config.yaml | Adds nbstripout hook to keep notebooks output-free and stable. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
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>
Owner
Author
|
switching to two staged setup |
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.
No description provided.