Offer a canonical form for the commutative structure (#746) - #933
Merged
Conversation
#746 tier 1 asks for "a specified canonicaliser". This is one, and it is a composition of parts that all already existed -- `Transformation.Canonicalisation` is InnerSimplification, then the CanonicalOrderExact rule set, then InnerSimplification again. No rule is changed and nothing new is computed. The leading normalisation is the part that matters and it is not obvious. The sort's key depends on a node's class and the normalisation changes classes: in 1/2 - x the constant reaches an unprepared sort as `1 * 2 ^ (-1)`, a product, and is ordered against -x as one, then folds to the number 1/2 immediately afterwards -- so the next pass orders it the other way and the two alternate for ever. Sorting a tree that has already settled sorts what the tree is actually going to be. Measured over 834 generated expressions and 2738 ordered pairs by the analysis workspace's `canoncheck`: idempotence order independence InnerSimplified 0 of 834 2024 of 2738 order, then normalise 21 of 834 0 of 2738 this 0 of 834 0 of 2738 Nesting goes with order, which was not expected and is now a test: the sort works over commutative *chains* rather than over one node, so it flattens as it sorts. `(x + y) + a` and `x + (y + a)` both reach `a + x + y` and reach it as the same tree -- where InnerSimplified alone leaves them as two different trees that print identically, associativity being normalised on the way out rather than in the expression. A test states both halves of that side by side, because a comparison of printed forms cannot tell the two situations apart and every test here compares entities for that reason. What it does not claim: it is not a canonical form for the language, since zero-equivalence is undecidable here, and it is not a simplification -- it makes an expression comparable, not shorter. Equal trees mean the expressions are equal; different trees mean nothing at all. `Docs/Contributing/CanonicalForm.md` states the boundary. Nothing in the library runs it: it is offered, not applied, and a test pins that. Putting it inside InnerSimplified would move every commutative operand order in every printed answer at once, which is a decision for a release rather than for a transformation. No BREAKING-CHANGES entry: no input gives a different answer. The new public property is recorded in PublicApi.txt, which is what caught it. Measured: suite 6988 passed / 0 failed, of which 28 are new. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 14, 2026
Two corrections, both from a test that failed the way round I did not expect. Nesting goes with order. The sort works over commutative *chains* rather than over one node, so it flattens as it sorts: (x + y) + a and x + (y + a) both reach a + x + y and reach it as the same tree. I had written a test asserting they stay different and it failed, which is how this was found. So flattening is no longer owed -- what is owed is that InnerSimplified on its own does neither, and InnerSimplified is what every rule and every cache in the library actually sees. And the composition now exists under a name, Transformation.Canonicalisation (PR #933), so §8's first item is no longer to build it but to decide where it runs. Offering it changes nothing; putting it inside InnerSimplified moves every commutative operand order in every printed answer at once. The warning in §3 stands unsoftened for the same reason: the canonicaliser makes those two trees one, and almost nothing calls the canonicaliser. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 14, 2026
…rary is (#746) (#928) * State what canonical form means here, and measure how far off the library is (#746) #746's tier 1 asks for "canonical forms with a written specification of what canonical means for each node class, and a stated distinction between canonical and simplest", and its item 65 asks whoever does it to take a position, write it down, and let the engine be checked against it. This is the document; the checking is a new harness in the analysis workspace, and every number here came out of it rather than out of an argument. **The position.** Canonical is about identity and simplest is about presentation. A canonical form exists to make equality a structural comparison; a simplest form is the best-rated member of a class under a cost metric that the caller chooses, so it is only defined relative to one. **A complete canonical form does not exist, and that is a theorem rather than a gap.** Zero- equivalence is undecidable for the class the library accepts -- rationals, pi, exp, the trigonometric functions, abs and composition (Richardson 1968) -- and a canonical form would decide it. So the specification is a canonical form on a decidable sublanguage with the boundary written down, a normalisation everywhere else that must not be mistaken for one, and a search that is not required to be canonical at all. That is Moses' three-way split from 1971 and it costs nothing but saying so. **Three properties, none needing an oracle, measured against both candidates:** InnerSimplified Simplify idempotence 1 failed of 834 0 failed of 120 order independence 2024 failed of 2738 8 failed of 72 listed agreements 20 failed of 30 6 failed of 30 Neither is canonical, and Simplify is much the closer of the two -- which is the opposite of what the names suggest. InnerSimplified does not order the operands of a sum or a product at all, so it fails three quarters of the order checks by construction. Simplify reorders as a side effect of rating candidates, and its eight failures are all ties settled by generation order. **The finding that matters most to anyone writing a rule or a test:** `(x + y) + a` and `x + (y + a)` both print as `x + y + a` and are different trees. Associativity is normalised in the printer, not in the expression, so a comparison of printed forms calls them equal and a comparison of entities does not. The harness compares entities, which is why it saw this. **Two defects rather than decisions**, each measured and each reproducible on its own: cos(0 ^ y).InnerSimplified -(-1) provided ... then 1 provided ... not idempotent cos(-x).Simplify() cos(-x) while cos(-2 * x) -> cos(2 * x) The first is a rewrite building `-(-1)` above already-normalised children and returning without re-normalising; `-(-1)` on its own folds immediately. The second is the parity identities keyed on a shape a bare negation does not have -- sin, tan and abs behave the same way. Per node class the file states the target rather than describing today, marking each line met or not. One line is flagged as needing a maintainer's yes before anyone implements it: making subtraction and division sugar for a sum and a product, which is what makes the commutative laws reachable and is also a breaking change to everything that matches on Divf. And it names where a canonical form is actually available now: rational functions over Q, where zero-equivalence is decidable and the parts -- multivariate GCD, expansion, a monomial order -- landed with the polynomial layer in #918 and #923. That is the piece to build first because it is the piece that is possible. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Correct the specification: the total order exists, and the obstacle is confluence (#746) The first version of this file said a total order on operands was owed. It is not: the library has one, at three granularities, and measuring it changes what the document should ask for. `RewriteRules.CanonicalOrderExact` sorts and groups the operands of sums, products, conjunctions, disjunctions and set operations by the whole subtree. Applied before the normalisation it makes order independence **perfect** -- 0 failures of 2738, against 2024 without it. So the piece a specification would normally have to invent is built; what is missing is that the normalisation does not run it, which is also most of why `Simplify` agrees so much more often than `InnerSimplified`. And the reason it cannot simply be moved there is now measured rather than guessed at. Sorting and then normalising is **not idempotent** -- 21 of 834 -- and every failure is the same phenomenon, the sort and `Patterns.NumericNeatRules` disagreeing about where a numeric operand belongs and each undoing the other: 1 / 2 - x -> -x + 1/2 -> 1/2 + -x -> ... Neither is wrong on its own. Until they are made to agree, applying the order inside the normalisation trades 2024 order failures for a form that never settles. So §8's first item is no longer "specify and implement a total order" but "make the order and the normalisation confluent", which is a much smaller and much better defined question, and it is the one actually in the way of everything else in tier 1's canonicaliser. The measurement table gains the third column, §4's commutative rows say ordered-but-not-run rather than not-ordered, and §7 records that the harness now runs all three properties over all three candidate forms -- the differences between the columns being the point rather than any one number. Also: the two defects §3 lists are fixed, in #929 and #930, so the table is labelled with the build it was taken on and with what it reads without them. A harness report records a build. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Compose the canonicaliser out of what exists: normalise, order, normalise (#746) The previous revision said the order and the normalisation had to be made to agree, and left that as the open question. It is not a disagreement between rules and nothing has to be decided between them. The sort's key depends on a node's class and the normalisation changes classes. In 1/2 - x the constant reaches the sort as 1 * 2 ^ (-1), a product, and is ordered against -x as one; the normalisation folds it to the number 1/2, and the next sort orders it the other way. So the sort was ordering a shape about to stop existing. Normalising first gives both properties at once: InnerSimplified order then normalise normalise, order, normalise idempotence 0 of 834 21 of 834 0 of 834 order independence 2024 of 2738 0 of 2738 0 of 2738 x + (-1/2), whose constant is already a number when the sort reads it, was stable throughout, which is the control that makes this the explanation rather than a guess. So §8's first item is now to expose that composition as the canonicaliser rather than to reconcile anything. It needs no rule changed. What it needs is a decision about where it runs: opt-in changes nothing, and inside InnerSimplified every commutative operand order in every printed answer moves at once. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * The canonicaliser reaches associativity too, and it now exists (#746) Two corrections, both from a test that failed the way round I did not expect. Nesting goes with order. The sort works over commutative *chains* rather than over one node, so it flattens as it sorts: (x + y) + a and x + (y + a) both reach a + x + y and reach it as the same tree. I had written a test asserting they stay different and it failed, which is how this was found. So flattening is no longer owed -- what is owed is that InnerSimplified on its own does neither, and InnerSimplified is what every rule and every cache in the library actually sees. And the composition now exists under a name, Transformation.Canonicalisation (PR #933), so §8's first item is no longer to build it but to decide where it runs. Offering it changes nothing; putting it inside InnerSimplified moves every commutative operand order in every printed answer at once. The warning in §3 stands unsoftened for the same reason: the canonicaliser makes those two trees one, and almost nothing calls the canonicaliser. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Name what is actually missing for the rational-function form (#934) §8's remaining build item is smaller and more specific than 'a rational-function canonical form'. The greatest common divisor is already there and already verifies itself; what is missing is that nothing in the library puts an expression over a common denominator, so 1/x + 1/y and (x+y)/(x*y) cannot be brought to a common form by any existing route -- measured through Simplify, InnerSimplified and Factorize alike, and Simplify actively prefers the split form. Filed as #934 with the design and that measurement, so the next person starts from what is missing rather than from what it is called. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> --------- 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
1 participant
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.
#746 tier 1 asks for "a specified canonicaliser". This is one, and it is a composition of parts that all already existed —
Transformation.CanonicalisationisInnerSimplification, then theCanonicalOrderExactrule set, thenInnerSimplificationagain. No rule is changed and nothing new is computed.The leading normalisation is the part that matters
The sort's key depends on a node's class, and the normalisation changes classes. In
1/2 - xthe constant reaches an unprepared sort as1 * 2 ^ (-1)— a product — and is ordered against-xas one, then folds to the number1/2immediately afterwards, so the next pass orders it the other way and the two alternate for ever:Sorting a tree that has already settled sorts what the tree is actually going to be.
x + (-1/2), whose constant is already a number, was stable throughout — the control that makes this the explanation rather than a guess.Measured
Over 834 generated expressions and 2738 ordered pairs, by the analysis workspace's
canoncheck:InnerSimplifiedNesting goes with order, which I did not expect
The sort works over commutative chains rather than over one node, so it flattens as it sorts.
(x + y) + aandx + (y + a)both reacha + x + yand reach it as the same tree — whereInnerSimplifiedalone leaves them as two different trees that print identically, associativity being normalised on the way out rather than in the expression.A test states both halves side by side, because a comparison of printed forms cannot tell those two situations apart. Every test here compares entities, for that reason. (I had written the opposite as a test asserting non-equality; it failed, which is how this was found.)
What it does not claim
Not a canonical form for the language — zero-equivalence is undecidable here — and not a simplification: it makes an expression comparable, not shorter. Equal trees mean the expressions are equal; different trees mean nothing at all.
Docs/Contributing/CanonicalForm.md(#928) states the boundary.Nothing runs it: it is offered, not applied, and a test pins that. Putting it inside
InnerSimplifiedwould move every commutative operand order in every printed answer at once — a decision for a release rather than for a transformation.Scope
No
BREAKING-CHANGES.mdentry: no input gives a different answer. The new public property is recorded inPublicApi.txt, which is what caught the omission.Suite 6988 passed / 0 failed, of which 28 are new.
🤖 Generated with Claude Code