feat(math): add universal algebra domain with term evaluation, equation profiles, subalgebras, congruences, and quotients (#1912) - #2034
Conversation
…on profiles, subalgebras, congruences, and quotients Add the universal_algebra domain implementing exact, bounded, deterministic universal-algebra operations over immutable finite algebra values: - universal_algebra.term.evaluate.compute: exact bottom-up term evaluation over a finite algebra with complete operation tables - universal_algebra.equation.profile.compute: evaluate s = t over all assignments, returning HOLDS with satisfying count or FAILS with first counterassignment and exact left/right values - universal_algebra.subalgebra.generated.compute: least subalgebra containing a generating set by finite closure under all basic operations and nullary constants - universal_algebra.congruence.check.compute: exact compatibility check of a carrier partition against all basic operations - universal_algebra.quotient.compute: quotient algebra induced by a congruence with block-wise operations The FiniteAlgebra value parses only well-formed single-sorted finite algebras with complete operation tables. Operation and argument axes are exact and ordered. The domain does not propose a theorem prover, model finder, variety classifier, or equational presentation/free-algebra constructor. Closes #1912
- Import TOOLS and ADMISSIONS in catalog/builtins.py. - Update frozen admission baselines (KEEP 239->244, candidates 399->404) and add the universal_algebra schema-snapshot fragment (5 operations). - Add 14 focused tests (term evaluation, equation profile, generated subalgebra, congruence check, quotient, validation).
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![devin-ai-integration[bot]](https://avatars.githubusercontent.com/in/811515?s=60&v=4){kind=small}
| for args in iproduct(range(block_count), repeat=symbol.arity): | ||
| cell_index = 0 | ||
| for arg in args: | ||
| cell_index = cell_index * n + arg | ||
| output = algebra.tables[op_idx][cell_index] | ||
| table.append(block_of[output]) |
There was a problem hiding this comment.
🔴 Quotient algebra returns wrong operation tables
Quotient operation tables are built by feeding block numbers straight into the original element table (algebra.tables[op_idx][cell_index] at src/jacobian/math/universal_algebra/operations.py:188-193) instead of a representative element of each block, so the returned quotient is mathematically wrong whenever blocks and elements do not coincide.
Impact: Users get incorrect quotient algebra tables for most non-trivial partitions, silently and with no error.
Block indices used as carrier indices when addressing the original table
For an operation of arity r, the code enumerates args over range(block_count) but computes cell_index in base n = len(carrier) and then reads the original table at that index. The original table is indexed by carrier elements, not blocks, so this only produces correct results in the accidental cases block_count == n (the identity partition, where block i happens to be {i} in order) or block_count == 1 with the first block containing element 0 — which are exactly the two cases covered by the tests at tests/math/universal_algebra/test_universal_algebra.py:183-188.
Example: carrier size 3, partition ((0,1),(2,)), binary op. The quotient table for (B0,B1) should be block_of(f(rep(B0), rep(B1))) = block_of(f(0,2)), i.e. original cell 0*3+2 = 2; the code instead reads cell 0*3+1 = 1, i.e. f(0,1).
The correct construction picks a representative per block (e.g. min(block)), computes cell_index from the representatives in base n, and maps the output through block_of.
| for args in iproduct(range(block_count), repeat=symbol.arity): | |
| cell_index = 0 | |
| for arg in args: | |
| cell_index = cell_index * n + arg | |
| output = algebra.tables[op_idx][cell_index] | |
| table.append(block_of[output]) | |
| representatives = [min(block) for block in partition] | |
| for args in iproduct(range(block_count), repeat=symbol.arity): | |
| cell_index = 0 | |
| for arg in args: | |
| cell_index = cell_index * n + representatives[arg] | |
| output = algebra.tables[op_idx][cell_index] | |
| table.append(block_of[output]) |
Was this helpful? React with 👍 or 👎 to provide feedback.
| class SubalgebraRequest(StrictModel): | ||
| """Compute the least subalgebra containing the generating set.""" | ||
|
|
||
| algebra: FiniteAlgebra | ||
| generators: tuple[int, ...] = Field(default=()) |
There was a problem hiding this comment.
🔴 Subalgebra generators outside the carrier crash the operation
Generating elements are never checked against the algebra size before being used to look up operation results (algebra.tables[op_idx][cell_index] at src/jacobian/math/universal_algebra/operations.py:109-113), so a request naming a non-existent element aborts with an internal error instead of a typed result.
Impact: A validly-shaped subalgebra request with an out-of-range generator raises a host exception rather than returning a mathematical answer or a validation error.
Missing request validation on `SubalgebraRequest.generators`
SubalgebraRequest (src/jacobian/math/universal_algebra/_models.py:57-61) accepts any tuple of ints; EvaluateRequest does validate its assignment against the carrier range (src/jacobian/math/universal_algebra/_models.py:20-25) and CongruenceRequest validates partition elements (src/jacobian/math/universal_algebra/_models.py:78-89), so this omission is inconsistent.
With carrier=("0","1") and generators=(5,), the closure loop computes cell_index = 5*2+5 = 15 for a binary operation whose table has 4 cells, raising IndexError. AGENTS.md requires that an accepted request return a typed domain result, with mathematical inapplicability handled in the request validator.
| class SubalgebraRequest(StrictModel): | |
| """Compute the least subalgebra containing the generating set.""" | |
| algebra: FiniteAlgebra | |
| generators: tuple[int, ...] = Field(default=()) | |
| class SubalgebraRequest(StrictModel): | |
| """Compute the least subalgebra containing the generating set.""" | |
| algebra: FiniteAlgebra | |
| generators: tuple[int, ...] = Field(default=()) | |
| @model_validator(mode="after") | |
| def require_valid_generators(self) -> Self: | |
| n = len(self.algebra.carrier) | |
| if any(not 0 <= g < n for g in self.generators): | |
| raise ValueError("generator out of carrier range") | |
| return self |
Was this helpful? React with 👍 or 👎 to provide feedback.
| class QuotientRequest(StrictModel): | ||
| """Compute the quotient algebra A/theta.""" | ||
|
|
||
| algebra: FiniteAlgebra | ||
| partition: tuple[tuple[int, ...], ...] |
There was a problem hiding this comment.
🔴 Quotient requests with malformed partitions crash instead of returning a result
The partition supplied for a quotient is accepted without any range or disjointness check (partition: tuple[tuple[int, ...], ...] at src/jacobian/math/universal_algebra/_models.py:99-103), so a partition mentioning a non-existent element can abort the call with an internal lookup error.
Impact: A well-formed-looking quotient request can fail with a host exception instead of a mathematical result or a clear validation message.
Cover check in `congruence_check` can be satisfied by out-of-range elements
CongruenceRequest validates element range and block disjointness (src/jacobian/math/universal_algebra/_models.py:78-89), but QuotientRequest does not. quotient delegates to congruence_check, whose only structural guard is len(block_of) != n (src/jacobian/math/universal_algebra/operations.py:139-140). With carrier=("0","1") and partition=((0, 5),), block_of = {0: 0, 5: 0} has size 2 == n, so the guard passes, and the compatibility loop then evaluates block_of[1], raising KeyError. Adding the same validator used by CongruenceRequest (and/or making congruence_check verify the keys are exactly range(n)) fixes it.
| class QuotientRequest(StrictModel): | |
| """Compute the quotient algebra A/theta.""" | |
| algebra: FiniteAlgebra | |
| partition: tuple[tuple[int, ...], ...] | |
| class QuotientRequest(StrictModel): | |
| """Compute the quotient algebra A/theta.""" | |
| algebra: FiniteAlgebra | |
| partition: tuple[tuple[int, ...], ...] | |
| @model_validator(mode="after") | |
| def require_partition_covers_carrier(self) -> Self: | |
| n = len(self.algebra.carrier) | |
| seen: set[int] = set() | |
| for block in self.partition: | |
| for elem in block: | |
| if not 0 <= elem < n: | |
| raise ValueError("partition element out of carrier range") | |
| if elem in seen: | |
| raise ValueError("partition blocks must be disjoint") | |
| seen.add(elem) | |
| return self |
Was this helpful? React with 👍 or 👎 to provide feedback.
| @model_validator(mode="after") | ||
| def require_valid_root(self) -> Self: | ||
| if self.root >= len(self.nodes): | ||
| raise ValueError("root index out of range") | ||
| return self |
There was a problem hiding this comment.
🔴 Malformed terms make evaluation crash with an internal error
Term node references and node kinds are never checked when a term is parsed (only the root index is checked, at src/jacobian/math/universal_algebra/values.py:87-91), so a request with a child index out of range, a self-referencing node, an unknown kind, or a variable not covered by the assignment aborts with an internal error.
Impact: Accepted-looking term evaluation and equation requests can fail as host errors rather than returning a mathematical value or a validation message.
Unvalidated flat-term structure and assignment completeness
FlatTerm validates only root < len(nodes). Consequences in evaluate_term (src/jacobian/math/universal_algebra/operations.py:29-52):
- A child index >=
len(nodes)raisesIndexErroratterm.nodes[index]. - A node whose children include its own index (or any cycle) recurses forever, raising
RecursionError. Term.kindis a free-formstr(src/jacobian/math/universal_algebra/values.py:74), sokind="foo"reaches theunknown node kindValueError.EvaluateRequestvalidates assignment ranges but not completeness, so a term usingvariable_id=3withassignment=(0,)raisesincomplete assignment; likewiseequation_profilebuilds assignments only forrange(variable_count)(src/jacobian/math/universal_algebra/operations.py:68-70), so a term referencing a higher variable index raises.
AGENTS.md requires the request model to encode the advertised mathematical domain (completeness, well-formedness) so that an accepted request always returns a typed result. Fixes: constrain kind to a literal, validate every child index against len(nodes) and acyclicity/topological ordering plus arity in FlatTerm, and validate assignment/variable coverage in EvaluateRequest and EquationProfileRequest.
Prompt for agents
FlatTerm/Term in src/jacobian/math/universal_algebra/values.py accept structurally invalid terms: `kind` is an unconstrained str, child indices are not checked against the node list, cycles are permitted, and children counts are not checked against operation arity. evaluate_term in operations.py then raises IndexError, RecursionError or ValueError for such inputs. Additionally EvaluateRequest (_models.py) validates assignment ranges but not that every variable referenced by the term has an assigned value, and EquationProfileRequest does not check that all term variable ids are < variable_count, so evaluate_term raises 'incomplete assignment'. Per AGENTS.md every accepted request must return a typed domain result, so these conditions must be rejected by the request/value validators (constrain kind to a Literal, validate child indices in range and acyclic/topologically ordered, and validate variable coverage).
Was this helpful? React with 👍 or 👎 to provide feedback.
| for op_idx, symbol in enumerate(algebra.operations): | ||
| if symbol.arity == 0: | ||
| continue | ||
| for x in iproduct(range(n), repeat=symbol.arity): | ||
| for y in iproduct(range(n), repeat=symbol.arity): | ||
| if all(block_of[x[j]] == block_of[y[j]] for j in range(symbol.arity)): |
There was a problem hiding this comment.
🔴 Congruence and quotient checks can run for effectively unbounded time
The congruence compatibility test loops over every pair of argument tuples (iproduct(range(n), repeat=symbol.arity) nested twice at src/jacobian/math/universal_algebra/operations.py:146-147), which for the largest accepted algebra is on the order of a trillion iterations, so the call never finishes.
Impact: A request within the documented limits can hang the server indefinitely.
n^(2r) enumeration with n up to 32 and r up to 4
MAX_CARRIER_SIZE = 32 and MAX_ARITY = 4 (src/jacobian/math/universal_algebra/values.py:18-20) permit n^(2*arity) = 32^8 ≈ 1.1e12 iterations per operation, times up to 16 operations. quotient runs the same check first (src/jacobian/math/universal_algebra/operations.py:171).
The compatibility check can be done in n^arity * arity work by, for each argument tuple, comparing against tuples where one coordinate is replaced by another element of the same block (or simply by iterating over block-index tuples and their representatives). Additionally, AGENTS.md requires an explicit, tested work budget: either derive a bound and reject requests above it, or reduce the enumeration.
The same class of problem affects EquationProfileRequest.variable_count, which is only Field(ge=1) (src/jacobian/math/universal_algebra/_models.py:40); equation_profile enumerates n ** variable_count assignments, so variable_count=20 with n=32 is unbounded work.
Prompt for agents
congruence_check in src/jacobian/math/universal_algebra/operations.py enumerates all pairs (x, y) of argument tuples, i.e. n^(2*arity) iterations, with n up to MAX_CARRIER_SIZE=32 and arity up to MAX_ARITY=4 (values.py). That is ~1e12 iterations per operation, so an accepted request can hang. quotient() invokes the same check. Rework the compatibility test to a bounded form (for each argument tuple, vary one coordinate over its block, or iterate over block-index tuples with representatives), and/or add an explicit named work budget validated on the request. Separately, EquationProfileRequest.variable_count in _models.py has no upper bound while equation_profile enumerates n**variable_count assignments; add a bounded budget there too.
Was this helpful? React with 👍 or 👎 to provide feedback.
| for symbol in algebra.operations: | ||
| if symbol.arity == 0: | ||
| for output in algebra.tables[algebra.operations.index(symbol)]: | ||
| carrier_set.add(output) |
There was a problem hiding this comment.
🟡 Nullary constants are looked up by symbol equality, which can pick the wrong table
When seeding the subalgebra with constants, the operation's table is located by searching for an equal operation symbol (algebra.operations.index(symbol) at src/jacobian/math/universal_algebra/operations.py:97), so two symbols with the same name and arity make the wrong constant be used.
Impact: For algebras with repeated operation symbols, the generated subalgebra can contain wrong elements.
`list.index` matches by value, not position
OperationSymbol is a pydantic model compared by field values, and FiniteAlgebra does not require unique operation_ids (src/jacobian/math/universal_algebra/values.py:44-61), so two distinct nullary symbols with the same id/arity but different tables collapse to the first index. The enclosing loop should use enumerate(algebra.operations) like the closure loop at src/jacobian/math/universal_algebra/operations.py:104.
| for symbol in algebra.operations: | |
| if symbol.arity == 0: | |
| for output in algebra.tables[algebra.operations.index(symbol)]: | |
| carrier_set.add(output) | |
| for op_idx, symbol in enumerate(algebra.operations): | |
| if symbol.arity == 0: | |
| for output in algebra.tables[op_idx]: | |
| carrier_set.add(output) |
Was this helpful? React with 👍 or 👎 to provide feedback.
| def compute_congruence(request: CongruenceRequest) -> CongruenceResult: | ||
| result = congruence_check(request.algebra, request.partition) | ||
| return CongruenceResult( | ||
| is_congruence=result["is_congruence"], # type: ignore[arg-type] | ||
| obstruction=result.get("obstruction"), # type: ignore[arg-type] | ||
| ) |
There was a problem hiding this comment.
🔍 Congruence obstruction details are computed but dropped at the wire boundary
congruence_check returns rich obstruction data (operation, x, y) on failure, but CongruenceResult only carries is_congruence and an obstruction string, so compute_congruence discards the witness. The declared tool description advertises a compatibility check; if the witness is meant to be user-visible (as the equation profile exposes its counterassignment), the result model should include it. Also note quotient turns a non-congruence partition into a raised ValueError rather than a typed result, which is a different pattern from congruence_check returning an obstruction.
Was this helpful? React with 👍 or 👎 to provide feedback.
| class QuotientResult(StrictModel): | ||
| """The quotient algebra carrier, operations, and tables.""" | ||
|
|
||
| carrier: tuple[str, ...] | ||
| operations: tuple[tuple[str, int], ...] | ||
| tables: tuple[tuple[int, ...], ...] |
There was a problem hiding this comment.
🔍 Quotient result does not carry the block membership map or validate table sizes
QuotientResult reports carrier labels B0..Bk, the original (operation_id, arity) pairs and flattened tables, but nothing tells the caller which original elements belong to which block, so the quotient homomorphism is not recoverable from the result. Additionally the tables are indexed in base block_count while FiniteAlgebra would validate them in base len(carrier); the result is a loose tuple-of-tuples with no cell-count validation, so a caller cannot round-trip it into a FiniteAlgebra without re-deriving the indexing convention.
Was this helpful? React with 👍 or 👎 to provide feedback.
| @model_validator(mode="after") | ||
| def require_well_formed(self) -> Self: | ||
| if len(self.carrier) > MAX_CARRIER_SIZE: | ||
| raise ValueError("carrier size exceeds the bounded budget") | ||
| if len(set(self.carrier)) != len(self.carrier): | ||
| raise ValueError("carrier labels must be unique") | ||
| if len(self.tables) != len(self.operations): | ||
| raise ValueError("tables must have one entry per operation symbol") | ||
| for symbol, table in zip(self.operations, self.tables, strict=True): | ||
| expected_cells = len(self.carrier) ** symbol.arity | ||
| if len(table) != expected_cells: | ||
| raise ValueError( | ||
| f"operation {symbol.operation_id} table has wrong cell count" | ||
| ) | ||
| for output in table: | ||
| if not 0 <= output < len(self.carrier): | ||
| raise ValueError("table output out of carrier range") | ||
| return self |
There was a problem hiding this comment.
🔍 Signature does not enforce unique operation ids despite the stated contract
The PR description says FiniteSignature carries "unique IDs", but the implemented FiniteAlgebra validator only checks carrier uniqueness, table counts and output ranges — duplicate operation_id values are accepted. This is what makes the operations.index(symbol) lookup ambiguous and also means the quotient result can report two identically named operations.
Was this helpful? React with 👍 or 👎 to provide feedback.
| class TestQuotient: | ||
| def test_trivial_quotient(self) -> None: | ||
| result = compute_quotient( | ||
| QuotientRequest(algebra=_boolean_algebra(), partition=((0, 1),)) | ||
| ) | ||
| assert result.carrier == ("B0",) | ||
| assert len(result.operations) == 2 |
There was a problem hiding this comment.
🔍 Tests cover only degenerate quotient/congruence cases
All quotient and congruence tests use a 2-element algebra with either the universal partition (1 block) or the identity partition (2 blocks, in order). Both are exactly the cases where the block-index-as-element table indexing coincidentally produces correct output, which is why the incorrect quotient table construction is not detected. A 3-element algebra with a 2-block partition (e.g. Z/3 with blocks {0,1},{2} or a genuine congruence on a 4-element algebra) would be the defining-invariant test: quotient tables must agree with block_of(f(reps)) for every block tuple.
Was this helpful? React with 👍 or 👎 to provide feedback.
morluto
left a comment
morluto
left a comment
There was a problem hiding this comment.
Review verdict: blocked — quotient operations are indexed by block IDs as though they were carrier elements
1. quotient() computes the wrong operation table
For quotient arguments (B_i1, ..., B_ir), the original operation must be evaluated on one representative from each block. The code instead feeds the block indices themselves into the original dense table:
cell_index = cell_index * n + argA minimal counterexample is a four-element algebra with unary identity f(x)=x and the congruence ((0,1),(2,3)). The quotient operation must be identity on two blocks, table (0,1). This code evaluates original elements 0 and 1, both in block 0, and returns (0,0).
Choose a deterministic representative partition[arg][0] for every quotient argument, evaluate the original table at those carrier indices, then map the result through block_of. Add a quotient well-definedness/reconstruction test independent of block ordering.
2. The “partition” boundary admits empty blocks and QuotientRequest has no partition validation
CongruenceRequest checks disjointness/range but not coverage despite its validator name, and it never rejects empty blocks. ((0,1), ()) covers a two-element carrier, so congruence_check() returns true and quotient() creates a spurious empty quotient class. A partition must have nonempty, pairwise-disjoint blocks whose union is the carrier. Reuse one exact partition value/validator for both check and quotient.
3. FlatTerm is not a safe term representation
It validates only the root. Child indices may be negative/out of range; nodes may self-reference or form cycles; arbitrary kind/field combinations are accepted. A one-node application whose child is itself recurses until RecursionError. Validate the complete reachable graph as an acyclic, well-founded term DAG (or require children to precede parents), validate node variants structurally, and bound node count/depth.
EvaluateRequest also does not enforce its claimed complete assignment: extras are ignored and missing variables fail only during execution. EquationProfileRequest does not require term variable IDs below variable_count.
4. The advertised bounded completeness is not bounded
variable_count has no upper/work bound, so equation profiling accepts |A|^k enumeration for arbitrary k. Congruence checking accepts up to 32^(2*4) argument pairs (over one trillion per operation). Bounds must constrain the actual derived work, not only carrier/arity independently.
5. Generated-subalgebra metadata is wrong
generators are not range/uniqueness validated, and is_closed compares final set size with the raw tuple length. Duplicate generators can make a closed set report false; an empty generator tuple with nullary constants always reports true even though constants were added. Define whether this field means “the input set was already closed” or “the returned set is closed”, then compute and validate that exact predicate.
The basic table encoding and term-evaluation indexing are sound once inputs are well-founded. The quotient bug is independently merge-blocking.
Deep review summaryVerdict: REQUEST CHANGES — quotient tables are mathematically wrong, and several accepted inputs can crash or exceed any defensible work bound. 1.
|
1 participant
Closes #1912.
Summary
Add the
universal_algebradomain implementing exact, bounded, deterministic universal-algebra operations over immutable single-sorted finite algebra values. This is the general finite-algebra layer above #1686's one-binary-operation magma tools and below many domain-specific algebra families.Design and library choices
The domain uses an exact enumeration kernel over immutable finite-algebra values. No theorem prover, model finder, variety classifier, or equational presentation/free-algebra constructor is introduced. Per the issue, this does not propose a general first-order logic language, many-sorted framework, or arbitrary callback system.
Representation (
values.py).FiniteAlgebrabinds a finite unique carrier, aFiniteSignature(tuple ofOperationSymbols with unique IDs and bounded arities), and complete operation tables (one per operation, indexed by the dense Cartesian product of input positions in row-major order). The value parses only well-formed algebras: unique carrier labels, correct table cell counts, and in-range table outputs. AFlatTermis a closed source-bound AST (flat node list with parent/child indices) for finite-algebra terms.Operations (
operations.py). All functions are deterministic and complete for accepted values.term.evaluate.compute— exact bottom-up term evaluation under a complete variable assignment.equation.profile.compute— evaluates = tover all assignments. ReturnHOLDSwith satisfying count, orFAILSwith first counterassignment and exact left/right values. Generalizes magma identity calculation to an arbitrary finite signature.subalgebra.generated.compute— least subalgebra containing a generating set by finite closure under all basic operations and nullary constants.congruence.check.compute— exact compatibility check of a carrier partition against all basic operations.quotient.compute— quotient algebraA/thetainduced by a congruence with block-wise operations.Invariances verified by tests
AND(0, 1) = 0andAND(1, 1) = 1in the 2-element Boolean algebra.AND(x, x) = xholds (idempotence) with 2 satisfying assignments;AND(x, y) = xfails.{0}is{0}(closed); of{0, 1}is{0, 1}.{{0, 1}}and equality partition{{0}, {1}}are both congruences.Validation
make checklint + typecheck clean; 14 focused domain tests; all 1136tests/math,tests/catalog,tests/dispatchtests pass.universal_algebraschema-snapshot fragment added (5 operations).Continue this on Linzumi