From 05326bb9bb243d25bde03cd8187416e32d1cb991 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 14 Aug 2026 02:22:00 +0000 Subject: [PATCH 1/5] 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. https://github.com/asc-community/AngouriMath/issues/746 Co-authored-by: Claude Opus 5 --- AGENTS.md | 1 + .../Docs/Contributing/CanonicalForm.md | 238 ++++++++++++++++++ .../AngouriMath/Docs/Contributing/README.md | 5 +- 3 files changed, 243 insertions(+), 1 deletion(-) create mode 100644 Sources/AngouriMath/Docs/Contributing/CanonicalForm.md diff --git a/AGENTS.md b/AGENTS.md index 60e702ccf..cb16332a5 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -369,6 +369,7 @@ are short, and a stale one is worse than none — if you change what a file desc | [`Contributing/ImproveParser.md`](Sources/AngouriMath/Docs/Contributing/ImproveParser.md) | how to change the grammar and regenerate | | [`Contributing/Transformations.md`](Sources/AngouriMath/Docs/Contributing/Transformations.md) | the transformation layer the 1.x entry points sit on, and how to add the next rule set | | [`Contributing/SimplificationContract.md`](Sources/AngouriMath/Docs/Contributing/SimplificationContract.md) | what a rewrite may assume, and the ten obligations one has to meet. Read it *before* adding or changing a rule | +| [`Contributing/CanonicalForm.md`](Sources/AngouriMath/Docs/Contributing/CanonicalForm.md) | canonical versus simplest, why no canonical form exists for the whole language, and what one means per node class. Read it before comparing two expressions for equality | | [`Contributing/coding_rules.md`](Sources/AngouriMath/Docs/Contributing/coding_rules.md) | sealed-or-abstract, and immutability of `Entity` | | [`WhatsNew/version_performance_control.md`](Sources/AngouriMath/Docs/WhatsNew/version_performance_control.md) | the inter-version performance table, and how to add a column | | `Sources/Analyzers/` | the custom analyzers, including the static-field one behind `[ConstantField]` | diff --git a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md new file mode 100644 index 000000000..52dc3b766 --- /dev/null +++ b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md @@ -0,0 +1,238 @@ +# What canonical form means here, and how it differs from simplest + +[#746](https://github.com/asc-community/AngouriMath/issues/746) tier 1 asks for two things this +file is: a written specification of what canonical means for each node class, and **a stated +distinction between canonical and "simplest"**. Its item 65 says to take a position, write it down, +and let the engine be checked against it. The checking is `work/canoncheck`, and every number below +came out of it rather than out of an argument. + +Read [SimplificationContract.md](SimplificationContract.md) first if you are changing a rewrite. +That file is about whether a rewrite is *sound*. This one is about what shape the expression it is +handed is in, and what a caller may conclude from two expressions having the same shape. + +--- + +## 1. The position, in one paragraph + +**Canonical is about identity. Simplest is about presentation. They are different jobs, they want +different machinery, and conflating them is how a library ends up with neither.** + +A *canonical form* is a function `c` on expressions such that `c(a)` and `c(b)` are the **identical +tree** whenever `a` and `b` denote the same mathematical object. Its whole purpose is that equality +becomes a structural comparison: you get to decide `a = b` by canonicalising both and comparing +nodes. It says nothing about whether the result is nice to look at. + +A *simplest form* is the best-rated member of an equivalence class under a cost metric. The metric +is a caller's choice — smallest tree, fewest radicals, numerically stablest, most readable to a +student — so "simplest" is only defined relative to one, and two different metrics give two +different answers that are both right. + +The library has one of each, and they are `InnerSimplified` and `Simplify`. Neither is currently +canonical; §3 measures how far off each is, and the answer is not the one the names suggest. + +## 2. A complete canonical form does not exist, and that is a theorem rather than a gap + +For the class of expressions AngouriMath accepts — rationals, `pi`, the exponential, the +trigonometric functions, `abs`, and composition — **deciding whether an expression is zero is +undecidable.** That is Richardson's theorem (Daniel Richardson, *Some undecidable problems involving +elementary functions of a real variable*, J. Symbolic Logic 33 (1968), 514–520), and since a +canonical form would decide zero-equivalence by canonicalising and comparing against `0`, no +canonical form exists for the whole language. + +So the specification cannot be "canonicalise everything", and any roadmap item that reads that way +is asking for something that is not there. What it can be, and what the rest of this file is: + +1. **A canonical form on a decidable sublanguage**, stated exactly, with the boundary written down. +2. **A normalisation everywhere else** — idempotent, order-independent, and cheap — which is not + canonical and must not be relied on as though it were. +3. **A search** for a presentable form, which is `Simplify`, and which is explicitly not required to + be canonical. + +This is the classical three-way split — Joel Moses, *Algebraic simplification: a guide for the +perplexed*, CACM 14 (1971), 527–537 — and taking the position costs nothing except writing it down, +which is what tier 1 asked for. + +## 3. Where the library actually stands, measured + +Three properties, each of which a canonical form must have and none of which needs an oracle: + +- **idempotence** — applying the form twice is applying it once; +- **order independence** — the operands of a commutative operator may be written either way round; +- **agreement** — two writings of one expression reach the same form. + +`work/canoncheck` measures all three against both candidates, comparing **entities and not printed +strings**. Measured on `master`: + +| | `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.** That is worth stating +plainly because the names imply the opposite: `InnerSimplified` sounds like the normal form and +`Simplify` like the pretty-printer, and it is the other way round. `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 searching and rating candidates, and agrees +far more often — but not always, because when two candidates rate equal the tie goes to whichever +was generated first, which depends on the input order. What ranks them is +`MathS.Settings.ComplexityCriteria` — `SimplifiedRate`, a weighted count — and not the node count +that `Complexity` returns; ties between differently-shaped forms are common. + +### The finding that matters most for anyone writing a rule + +`(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. A rule, a test or a cache that compares printed +forms will call them equal; one that compares entities will not. Compare entities. + +### Two defects it turned up, rather than decisions + +- `cos(0 ^ y)` is not idempotent under `InnerSimplified`: the first pass leaves `-(-1)` at the head + of the answer and the second folds it to `1`. `-(-1)` on its own folds immediately, so a rewrite + is building it above already-normalised children and returning without re-normalising. +- `cos(-x)`, `sin(-x)`, `tan(-x)` and `abs(-x)` are left alone by `Simplify`, while `cos(-2 * x)` + folds to `cos(2 * x)`. The parity identities are keyed on a shape that a bare negation does not + have. + +## 4. What canonical means per node class + +This is the **target**, not a description of today. Where the library already meets a line it is +marked; where it does not, the line is what `canoncheck` should eventually assert. + +### Leaves + +| class | canonical form | +|---|---| +| `Integer`, `Rational` | lowest terms, denominator positive; a rational with denominator one is an `Integer` — **met** | +| `Real`, `Complex` | a complex with zero imaginary part is a `Real`; likewise down the tower — **met** | +| `Variable` | itself; the name is the identity | +| `Boolean` | `True` or `False` | + +### Commutative operators + +| class | canonical form | +|---|---| +| `Sumf` | flat over nesting, operands in a total order, numeric operands folded into one leading term, a zero term dropped — **not met**: neither flattened nor ordered in the tree | +| `Mulf` | flat, ordered, numeric factors folded into one leading factor, a one factor dropped, a zero factor collapsing the product — **not met**, as above | +| `Andf`, `Orf`, `Xorf` | flat, ordered, constants folded, duplicates dropped — **not met** | +| `Unionf`, `Intersectionf` | flat, ordered by the element order — **not met** | + +A **total order on operands** is what makes ordering decidable, and it has to be specified rather +than left to whatever a sort happens to do: by node class first in a fixed class order, then by the +class's own key — a number by value, a variable by name, a function by its name and then +lexicographically by its already-ordered children. It has to be total and stable, and it has to be +independent of how the expression was written, which is exactly what the order checks test. + +### Operators that are sugar for a commutative one + +| class | canonical form | +|---|---| +| `Minusf` | absent — `a - b` is `a + (-1) * b` | +| `Divf` | absent — `a / b` is `a * b ^ (-1)` | + +**This is a position and it is not free.** It is the one that makes the commutative laws reachable: +while a difference is its own node, `x - y` and `x + (-y)` are different trees denoting one thing — +measured, both listed pairs disagree — and no amount of ordering sums fixes it, because one of them +is not a sum. The cost is that the printer must put subtraction and division back, or every output +regresses into `a + (-1) * b`. The printer already does exactly this for a negative coefficient, +which is why `(-1) * x` prints `-x`; the change is to stop the *tree* from having two shapes, not to +change what is shown. + +**This is the one line here that needs a maintainer's yes before anybody implements it.** Removing +two node classes touches pattern matching, every `switch` over the hierarchy, the parser's output, +the exporters and `AddingNode.cs`, and it is a breaking change to anything matching on `Divf`. It is +written down as the position because a specification that ducks the question is not one; it is not +written down as a decision already taken. + +### Powers + +| class | canonical form | +|---|---| +| `Powf` | a numeric exponent in lowest terms; `x ^ 1` is `x`; `x ^ 0` is `1` **only where the base is known non-zero**, and otherwise carries the condition; a power of a power multiplies its exponents only where that is sound over the complex plane | + +`x ^ 0` is the standing example of a canonicalisation that a naive specification gets wrong: +measured, the library answers `1 provided not x = 0`, and that is right. `0 ^ 0` is not `1`. A +canonical form that maps `x ^ 0` to `1` unconditionally has made the library answer wrongly to buy +itself a tidier rule, which +[AGENTS.md](../../../../AGENTS.md) forbids in the first line. + +Likewise `sqrt(x)` and `x ^ (1/2)` **must** reach the same form — they denote the same principal +branch — and `(x ^ 2) ^ 3` and `x ^ 6` must not be assumed to, since `(x ^ a) ^ b` is `x ^ (a * b)` +only under conditions the contract file states. + +### Functions + +| class | canonical form | +|---|---| +| `Absf`, `Cosf`, and the even functions | the argument's own canonical form, with a leading negation removed — **not met**, see §3 | +| `Sinf`, `Tanf`, and the odd functions | a leading negation lifted out of the argument to the front of the node — **not met** | +| `Logf` | the base and the argument each canonical; no rewriting between bases, since that is a rule's decision and not a form's | +| everything else | children canonical, node unchanged | + +### Nodes that are not values + +| class | canonical form | +|---|---| +| `Providedf` | the condition itself canonical, and a `Providedf` never nested inside another — `(a provided p) provided q` is `a provided p and q` | +| `Derivativef`, `Integralf`, `Limitf` | children canonical; the node is a request, and a form must not evaluate it | +| `Setf` and the set classes | a finite set ordered and deduplicated — **met**, measured | + +## 5. Where a canonical form is actually available: the polynomial sublanguage + +§2 rules out canonicalising everything. It does not rule out canonicalising the part of the language +where zero-equivalence *is* decidable, and that part is large and useful: **rational functions over +`Q` in finitely many variables.** For those, a canonical form exists, is classical, and — since +[#918](https://github.com/asc-community/AngouriMath/pull/918) and +[#923](https://github.com/asc-community/AngouriMath/pull/923) — is now buildable out of parts the +library has: + +- a quotient of two polynomials, each expanded and with a specified monomial order; +- divided through by their multivariate GCD, which `PolynomialGcd` computes; +- with the denominator made monic in the order, the sign carried in the numerator; +- and the coefficients rationals in lowest terms. + +Two rational functions are equal exactly when this form is identical, so the equality question is +decided rather than searched. This is the concrete deliverable behind tier 1's "a specified +canonicaliser", and it is the piece to build first, because it is the piece that is *possible*. + +The boundary has to be stated at the API rather than hidden: a caller asking to canonicalise +`sin(x) + 1` must be told that no canonical form is claimed, not handed a normalisation that looks +like one. **A form that is canonical on part of the language and silently approximate on the rest is +worse than no form at all**, because its whole value was that structural equality meant something. + +## 6. What `Simplify` is, and what it is not required to be + +`Simplify` searches: it generates candidates by applying rewrites and returns the best by +`MathS.Settings.ComplexityCriteria`. It is therefore + +- **metric-relative** — a different criterion is a different answer, and that is intended; +- **not required to be canonical** — measured, it fails 8 of 72 order checks, all of them ties + broken by generation order; +- **not required to be idempotent**, though measured it is, at 120 of 120; +- **not a decision procedure for equality**. `a.Simplify() == b.Simplify()` failing proves nothing + at all. Use the residual — `(a - b).Simplify()` against zero — and even that is a semi-decision, + by §2. + +The one thing it *is* required to be is sound, which is [SimplificationContract.md](SimplificationContract.md). + +## 7. How this is checked + +`work/canoncheck`. It builds expressions by growing a small grammar, then checks idempotence and +order independence generatively and a listed set of agreements by hand. Its three counts are the +thing to watch; the listed pairs are each a claim this file makes or disclaims, so a disagreement +there is a decision to take rather than necessarily a defect. + +It compares entities. Nothing in it reads a printed form, which is deliberate: the associativity +finding in §3 is invisible to a string comparison and is the single most likely thing to be got +wrong by a test written in a hurry. + +## 8. What is owed + +1. A total order on operands, specified here and implemented once, rather than per node class. +2. Flattening of sums and products in the tree rather than in the printer. +3. The two defects in §3 — the non-idempotent `-(-1)`, and the parity identities that miss a bare + negation. +4. The rational-function canonical form of §5, as an explicit operation with the boundary in its + signature. +5. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is + a measurement, and its numbers belong in a commit message rather than in a gate. diff --git a/Sources/AngouriMath/Docs/Contributing/README.md b/Sources/AngouriMath/Docs/Contributing/README.md index 93620072d..74587e3c9 100644 --- a/Sources/AngouriMath/Docs/Contributing/README.md +++ b/Sources/AngouriMath/Docs/Contributing/README.md @@ -15,7 +15,10 @@ If you aren't sure about what to add, you may want to check the current projects 5. What a simplification rule may assume — read before adding or changing a rewrite. What has to be true for it to be sound, the four things that are not the same, and the branch-cut conventions this library commits to -6. Coding rules — sealed-or-abstract, immutability, and what may be +6. What canonical form means here — and how it differs from + "simplest". Why no canonical form exists for the whole language, what one means per node class, + and where the library measurably stands against it +7. Coding rules — sealed-or-abstract, immutability, and what may be made `public` See also BREAKING-CHANGES.md, where a change that makes From 1c091cc32e2c04126c8ac82fd8287eb54dd0412e Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 14 Aug 2026 03:01:37 +0000 Subject: [PATCH 2/5] Correct the specification: the total order exists, and the obstacle is confluence (#746) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. https://github.com/asc-community/AngouriMath/issues/746 Co-authored-by: Claude Opus 5 --- .../Docs/Contributing/CanonicalForm.md | 128 ++++++++++++------ 1 file changed, 85 insertions(+), 43 deletions(-) diff --git a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md index 52dc3b766..bcfdaef2a 100644 --- a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md +++ b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md @@ -60,24 +60,50 @@ Three properties, each of which a canonical form must have and none of which nee - **order independence** — the operands of a commutative operator may be written either way round; - **agreement** — two writings of one expression reach the same form. -`work/canoncheck` measures all three against both candidates, comparing **entities and not printed -strings**. Measured on `master`: - -| | `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.** That is worth stating -plainly because the names imply the opposite: `InnerSimplified` sounds like the normal form and -`Simplify` like the pretty-printer, and it is the other way round. `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 searching and rating candidates, and agrees -far more often — but not always, because when two candidates rate equal the tie goes to whichever -was generated first, which depends on the input order. What ranks them is -`MathS.Settings.ComplexityCriteria` — `SimplifiedRate`, a weighted count — and not the node count -that `Complexity` returns; ties between differently-shaped forms are common. +`work/canoncheck` measures all three against each candidate, comparing **entities and not printed +strings**. The figures below are on `master` with the two defects of the following subsection fixed +— [#929](https://github.com/asc-community/AngouriMath/issues/929) and +[#930](https://github.com/asc-community/AngouriMath/issues/930), each landing separately. Without +them the first column's idempotence reads 1 rather than 0 and the last column's agreements read 6 +rather than 4; nothing else moves. A harness report records a build, so regenerate it before quoting +it against a later one. + +| | `InnerSimplified` | `CanonicalOrderExact` then `InnerSimplified` | `Simplify` | +|---|---|---|---| +| idempotence | 0 failed of 834 | **21 failed of 834** | 0 failed of 120 | +| order independence | 2024 failed of 2738 | **0 failed of 2738** | 8 failed of 72 | +| listed agreements | 20 failed of 30 | 10 failed of 30 | 4 failed of 30 | + +**None of the three is canonical, and no one of them is closest on every property.** The middle +column is the surprise and it is the useful one. + +**The total order already exists and it works.** `RewriteRules.CanonicalOrderExact` sorts and groups +the operands of sums, products, conjunctions, disjunctions and set operations by the whole subtree, +and applying it makes order independence *perfect* — 0 failures of 2738, against 2024 without it. +There are three granularities: `CanonicalOrder` ignores constants so that `x` and `2 * x` group +together for collecting like terms, `CanonicalOrderCountingConstants` distinguishes them, and +`CanonicalOrderExact` compares whole subtrees, which is the one a canonical form wants. So the thing +a specification would normally have to invent is built; **what is missing is that the normalisation +does not run it.** `Simplify` does, which is most of why it agrees so much more often than +`InnerSimplified` — the names imply the opposite of the truth here. + +**And the pair is not confluent, which is the real obstacle.** Sorting and then normalising is not +idempotent: 21 of 834. Every failure is the sort and `InnerSimplified` disagreeing about where a +numeric operand belongs, and each undoing the other: + +``` +1 / 2 - x -> -x + 1/2 -> 1/2 + -x -> ... +0 ^ x -> 0 provided x / 2 * (...) > 0 -> 0 provided 1/2 * (...) * x > 0 -> ... +``` + +The sort puts the constant one way and `Patterns.NumericNeatRules` puts it back. Neither is wrong on +its own; they simply have not been made to agree, and until they do, applying the order inside the +normalisation would trade 2024 order failures for a form that never settles. + +`Simplify`'s remaining 8 order failures are a different thing again: ties. When two candidates rate +equal the tie goes to whichever was generated first, which depends on the input order. What ranks +them is `MathS.Settings.ComplexityCriteria` — `SimplifiedRate`, a weighted count — and not the node +count that `Complexity` returns; ties between differently-shaped forms are common. ### The finding that matters most for anyone writing a rule @@ -85,14 +111,19 @@ that `Complexity` returns; ties between differently-shaped forms are common. is normalised in the printer, not in the expression. A rule, a test or a cache that compares printed forms will call them equal; one that compares entities will not. Compare entities. -### Two defects it turned up, rather than decisions +### Two defects it turned up, rather than decisions — both since fixed -- `cos(0 ^ y)` is not idempotent under `InnerSimplified`: the first pass leaves `-(-1)` at the head - of the answer and the second folds it to `1`. `-(-1)` on its own folds immediately, so a rewrite - is building it above already-normalised children and returning without re-normalising. -- `cos(-x)`, `sin(-x)`, `tan(-x)` and `abs(-x)` are left alone by `Simplify`, while `cos(-2 * x)` - folds to `cos(2 * x)`. The parity identities are keyed on a shape that a bare negation does not - have. +- `cos(0 ^ y)` was not idempotent under `InnerSimplified`: the first pass left `-(-1)` at the head of + the answer and the second folded it to `1`. `-(-1)` on its own folds immediately, so a rewrite was + building it above already-normalised children and returning without re-normalising. + [#930](https://github.com/asc-community/AngouriMath/issues/930). +- `cos(-x)`, `sin(-x)`, `tan(-x)` and `abs(-x)` were left alone by `Simplify` while `cos(-2 * x)` + folded to `cos(2 * x)` — by accident, through the multiple-angle expansion rather than through + parity, since that skips a coefficient of `-1`. So `sin(-x) + sin(x)` did not reach `0`. + [#929](https://github.com/asc-community/AngouriMath/issues/929); with it the listed agreements + above are 4 rather than 6. + +Both were found on the first run, which is the argument for the harness rather than for the document. ## 4. What canonical means per node class @@ -112,16 +143,22 @@ marked; where it does not, the line is what `canoncheck` should eventually asser | class | canonical form | |---|---| -| `Sumf` | flat over nesting, operands in a total order, numeric operands folded into one leading term, a zero term dropped — **not met**: neither flattened nor ordered in the tree | -| `Mulf` | flat, ordered, numeric factors folded into one leading factor, a one factor dropped, a zero factor collapsing the product — **not met**, as above | -| `Andf`, `Orf`, `Xorf` | flat, ordered, constants folded, duplicates dropped — **not met** | -| `Unionf`, `Intersectionf` | flat, ordered by the element order — **not met** | - -A **total order on operands** is what makes ordering decidable, and it has to be specified rather -than left to whatever a sort happens to do: by node class first in a fixed class order, then by the -class's own key — a number by value, a variable by name, a function by its name and then -lexicographically by its already-ordered children. It has to be total and stable, and it has to be -independent of how the expression was written, which is exactly what the order checks test. +| `Sumf` | flat over nesting, operands in a total order, numeric operands folded into one leading term, a zero term dropped — **ordered by `CanonicalOrderExact`, which the normalisation does not run**; not flattened in the tree | +| `Mulf` | flat, ordered, numeric factors folded into one leading factor, a one factor dropped, a zero factor collapsing the product — as above | +| `Andf`, `Orf`, `Xorf` | flat, ordered, constants folded, duplicates dropped — ordered by the same rewrite | +| `Unionf`, `Intersectionf` | flat, ordered by the element order — ordered by the same rewrite | + +A **total order on operands** is what makes ordering decidable, and the library has one: +`Patterns.SortRules` at three granularities, reached through `RewriteRules.CanonicalOrder`, +`CanonicalOrderCountingConstants` and `CanonicalOrderExact`. Measured, the exact one is total enough +to give order independence on every pair tried. + +Two things are still owed and neither is the order itself. **Flattening** is done by the printer +rather than in the tree, which is why `(x + y) + a` and `x + (y + a)` print alike and differ. And the +order and the normalisation have to be made to **agree**: today, sorting and then normalising +oscillates on any sum with a numeric term, because `Patterns.NumericNeatRules` puts the constant back +where the sort took it from. Deciding which of the two wins is a smaller question than inventing an +order, and it is the one actually in the way. ### Operators that are sugar for a commutative one @@ -218,9 +255,11 @@ The one thing it *is* required to be is sound, which is [SimplificationContract. ## 7. How this is checked `work/canoncheck`. It builds expressions by growing a small grammar, then checks idempotence and -order independence generatively and a listed set of agreements by hand. Its three counts are the -thing to watch; the listed pairs are each a claim this file makes or disclaims, so a disagreement -there is a decision to take rather than necessarily a defect. +order independence generatively and a listed set of agreements by hand. It runs all three over each +of the three candidate forms — `InnerSimplified`, `CanonicalOrderExact` followed by +`InnerSimplified`, and `Simplify` — because the interesting facts are the differences between the +columns rather than any one number. The listed pairs are each a claim this file makes or disclaims, +so a disagreement there is a decision to take rather than necessarily a defect. It compares entities. Nothing in it reads a printed form, which is deliberate: the associativity finding in §3 is invisible to a string comparison and is the single most likely thing to be got @@ -228,11 +267,14 @@ wrong by a test written in a hurry. ## 8. What is owed -1. A total order on operands, specified here and implemented once, rather than per node class. +1. **Make the order and the normalisation agree**, so that `CanonicalOrderExact` followed by + `InnerSimplified` settles instead of oscillating on a sum with a numeric term. This is the piece + in the way of everything else: the order is already total and already gives perfect order + independence, and it cannot be moved into the normalisation until the pair is confluent. 2. Flattening of sums and products in the tree rather than in the printer. -3. The two defects in §3 — the non-idempotent `-(-1)`, and the parity identities that miss a bare - negation. -4. The rational-function canonical form of §5, as an explicit operation with the boundary in its +3. The rational-function canonical form of §5, as an explicit operation with the boundary in its signature. -5. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is +4. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is a measurement, and its numbers belong in a commit message rather than in a gate. + +The two defects §3 lists are fixed and are not on this list. From cf4911a487f9169b2081bfda0679b81f6734878b Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 14 Aug 2026 03:20:07 +0000 Subject: [PATCH 3/5] Compose the canonicaliser out of what exists: normalise, order, normalise (#746) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../Docs/Contributing/CanonicalForm.md | 53 +++++++++++-------- 1 file changed, 30 insertions(+), 23 deletions(-) diff --git a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md index bcfdaef2a..1f846c1fc 100644 --- a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md +++ b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md @@ -68,11 +68,11 @@ them the first column's idempotence reads 1 rather than 0 and the last column's rather than 4; nothing else moves. A harness report records a build, so regenerate it before quoting it against a later one. -| | `InnerSimplified` | `CanonicalOrderExact` then `InnerSimplified` | `Simplify` | -|---|---|---|---| -| idempotence | 0 failed of 834 | **21 failed of 834** | 0 failed of 120 | -| order independence | 2024 failed of 2738 | **0 failed of 2738** | 8 failed of 72 | -| listed agreements | 20 failed of 30 | 10 failed of 30 | 4 failed of 30 | +| | `InnerSimplified` | order, then normalise | **normalise, order, normalise** | `Simplify` | +|---|---|---|---|---| +| idempotence | 0 failed of 834 | 21 failed of 834 | **0 failed of 834** | 0 failed of 120 | +| order independence | 2024 failed of 2738 | 0 failed of 2738 | **0 failed of 2738** | 8 failed of 72 | +| listed agreements | 20 failed of 30 | 10 failed of 30 | 10 failed of 30 | 4 failed of 30 | **None of the three is canonical, and no one of them is closest on every property.** The middle column is the surprise and it is the useful one. @@ -87,18 +87,25 @@ a specification would normally have to invent is built; **what is missing is tha does not run it.** `Simplify` does, which is most of why it agrees so much more often than `InnerSimplified` — the names imply the opposite of the truth here. -**And the pair is not confluent, which is the real obstacle.** Sorting and then normalising is not -idempotent: 21 of 834. Every failure is the sort and `InnerSimplified` disagreeing about where a -numeric operand belongs, and each undoing the other: +**And the composition that has both properties is the third column, which is the canonicaliser this +tier was asking for.** Sorting and *then* normalising is not idempotent — 21 of 834 — but +normalising, sorting, and normalising again is idempotent and order-independent on everything tried: +**0 of 834 and 0 of 2738**. + +The reason is worth knowing, because it is not a conflict 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 then folds it to the number `1/2`, and the next sort — now +seeing a number — orders it the other way: ``` -1 / 2 - x -> -x + 1/2 -> 1/2 + -x -> ... -0 ^ x -> 0 provided x / 2 * (...) > 0 -> 0 provided 1/2 * (...) * x > 0 -> ... +1 / 2 - x sorted -> -x + 1 * 2 ^ (-1) normalised -> -x + 1/2 +-x + 1/2 sorted -> 1/2 + -x ...and back again ``` -The sort puts the constant one way and `Patterns.NumericNeatRules` puts it back. Neither is wrong on -its own; they simply have not been made to agree, and until they do, applying the order inside the -normalisation would trade 2024 order failures for a form that never settles. +So the sort was ordering a shape that was about to stop existing. Normalise first and it sorts what +the tree is actually going to be. `x + (-1/2)`, whose constant is already a number, was stable all +along — which is the control that makes this the explanation rather than a guess. `Simplify`'s remaining 8 order failures are a different thing again: ties. When two candidates rate equal the tie goes to whichever was generated first, which depends on the input order. What ranks @@ -153,12 +160,10 @@ A **total order on operands** is what makes ordering decidable, and the library `CanonicalOrderCountingConstants` and `CanonicalOrderExact`. Measured, the exact one is total enough to give order independence on every pair tried. -Two things are still owed and neither is the order itself. **Flattening** is done by the printer -rather than in the tree, which is why `(x + y) + a` and `x + (y + a)` print alike and differ. And the -order and the normalisation have to be made to **agree**: today, sorting and then normalising -oscillates on any sum with a numeric term, because `Patterns.NumericNeatRules` puts the constant back -where the sort took it from. Deciding which of the two wins is a smaller question than inventing an -order, and it is the one actually in the way. +One thing is still owed and it is not the order. **Flattening** is done by the printer rather than in +the tree, which is why `(x + y) + a` and `x + (y + a)` print alike and differ. The ordering itself is +solved by composing what already exists in the right sequence — normalise, order, normalise — which +§3 measures at 0 failures on both properties. ### Operators that are sugar for a commutative one @@ -267,10 +272,12 @@ wrong by a test written in a hurry. ## 8. What is owed -1. **Make the order and the normalisation agree**, so that `CanonicalOrderExact` followed by - `InnerSimplified` settles instead of oscillating on a sum with a numeric term. This is the piece - in the way of everything else: the order is already total and already gives perfect order - independence, and it cannot be moved into the normalisation until the pair is confluent. +1. **Expose `InnerSimplified` → `CanonicalOrderExact` → `InnerSimplified` as the canonicaliser**, + under a name, with §5's boundary stated in its documentation. It is measured idempotent and + order-independent, it is built entirely out of parts that already exist, and it needs no rule + changed. What it needs is a decision about *where* it runs: as an opt-in operation nothing + changes, and inside `InnerSimplified` every commutative operand order in every printed answer + moves at once, which is a release of its own. 2. Flattening of sums and products in the tree rather than in the printer. 3. The rational-function canonical form of §5, as an explicit operation with the boundary in its signature. From d4f3cd7ec8d54762205f8d5c9ca286e5b741a8e8 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 14 Aug 2026 03:42:36 +0000 Subject: [PATCH 4/5] The canonicaliser reaches associativity too, and it now exists (#746) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. https://github.com/asc-community/AngouriMath/issues/746 Co-authored-by: Claude Opus 5 --- .../Docs/Contributing/CanonicalForm.md | 42 +++++++++++-------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md index 1f846c1fc..c8d3a2930 100644 --- a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md +++ b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md @@ -114,9 +114,15 @@ count that `Complexity` returns; ties between differently-shaped forms are commo ### The finding that matters most for anyone writing a rule -`(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. A rule, a test or a cache that compares printed -forms will call them equal; one that compares entities will not. Compare entities. +`(x + y) + a` and `x + (y + a)` **both print as `x + y + a` and are different trees** after +`InnerSimplified`. Associativity is normalised in the printer, not in the expression. A rule, a test +or a cache that compares printed forms will call them equal; one that compares entities will not. +Compare entities. + +The canonicaliser of the third column *does* make them one tree — `a + x + y` — because the sort +works over commutative chains and so flattens as it sorts. That is worth knowing and does not soften +the warning: what almost everything in the library actually sees is `InnerSimplified`, where the two +trees are still two. ### Two defects it turned up, rather than decisions — both since fixed @@ -160,10 +166,14 @@ A **total order on operands** is what makes ordering decidable, and the library `CanonicalOrderCountingConstants` and `CanonicalOrderExact`. Measured, the exact one is total enough to give order independence on every pair tried. -One thing is still owed and it is not the order. **Flattening** is done by the printer rather than in -the tree, which is why `(x + y) + a` and `x + (y + a)` print alike and differ. The ordering itself is -solved by composing what already exists in the right sequence — normalise, order, normalise — which -§3 measures at 0 failures on both properties. +Both are met by composing what already exists in the right sequence — normalise, order, normalise — +which §3 measures at 0 failures on both properties and which is +`Transformation.Canonicalisation`. **Nesting comes with the ordering**, because 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`, as the same tree. + +What is *not* met is that `InnerSimplified` on its own does neither, and it is `InnerSimplified` that +every rule and every cache in the library sees. ### Operators that are sugar for a commutative one @@ -272,16 +282,14 @@ wrong by a test written in a hurry. ## 8. What is owed -1. **Expose `InnerSimplified` → `CanonicalOrderExact` → `InnerSimplified` as the canonicaliser**, - under a name, with §5's boundary stated in its documentation. It is measured idempotent and - order-independent, it is built entirely out of parts that already exist, and it needs no rule - changed. What it needs is a decision about *where* it runs: as an opt-in operation nothing - changes, and inside `InnerSimplified` every commutative operand order in every printed answer - moves at once, which is a release of its own. -2. Flattening of sums and products in the tree rather than in the printer. -3. The rational-function canonical form of §5, as an explicit operation with the boundary in its - signature. -4. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is +1. **Where the canonicaliser runs.** It exists — `Transformation.Canonicalisation`, built out of + parts that already existed, measured idempotent and order-independent, with no rule changed — and + nothing calls it. Offering it changes nothing for anyone. Putting it inside `InnerSimplified` + moves every commutative operand order in every printed answer at once, which is a release of its + own and a decision rather than an implementation. +2. The rational-function canonical form of §5, as an explicit operation with the boundary in its + signature. This is the one that needs building rather than composing. +3. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is a measurement, and its numbers belong in a commit message rather than in a gate. The two defects §3 lists are fixed and are not on this list. From 98da5fa2ee3d22d977b9dfafe4bfedd742c98875 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 14 Aug 2026 03:59:52 +0000 Subject: [PATCH 5/5] Name what is actually missing for the rational-function form (#934) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §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 --- Sources/AngouriMath/Docs/Contributing/CanonicalForm.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md index c8d3a2930..a7a34ed8b 100644 --- a/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md +++ b/Sources/AngouriMath/Docs/Contributing/CanonicalForm.md @@ -288,7 +288,12 @@ wrong by a test written in a hurry. moves every commutative operand order in every printed answer at once, which is a release of its own and a decision rather than an implementation. 2. The rational-function canonical form of §5, as an explicit operation with the boundary in its - signature. This is the one that needs building rather than composing. + signature — [#934](https://github.com/asc-community/AngouriMath/issues/934). This is the one that + needs building rather than composing, and the part that is missing is smaller and more specific + than it sounds: the greatest common divisor is already there and already verifies itself, but + **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. `Simplify` prefers the + split one and will pull the combined one apart again. 3. `canoncheck` in CI once the counts are meant to be zero, which they are not yet. Until then it is a measurement, and its numbers belong in a commit message rather than in a gate.