State what canonical form means here, and measure how far off the library is (#746)

[Rafael-SOWNet]

Part of #746 tier 1, which asks for "canonical forms with a written specification of what canonical means for each node class, and a stated distinction between canonical and simplest". 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 (canoncheck) in the analysis workspace, and every number below came out of it rather than out of an argument.

The position

Canonical is about identity. Simplest is about presentation. A canonical form exists so that equality becomes a structural comparison; a simplest form is the best-rated member of an equivalence class under a cost metric the caller chooses, so it is only defined relative to one. Conflating them is how a library ends up with neither.

A complete canonical form does not exist, and that is a theorem rather than a gap

Zero-equivalence is undecidable for the class AngouriMath accepts — rationals, pi, exp, the trigonometric functions, abs, and composition (Richardson 1968) — and a canonical form would decide it by canonicalising and comparing against 0.

So the specification is deliberately three things rather than one: a canonical form on a decidable sublanguage with the boundary written down, a normalisation everywhere else that must not be relied on as though it were canonical, and a search that is not required to be canonical at all. That is Moses' 1971 three-way split, and taking the position costs nothing except writing it down.

Where the library measurably stands

Three properties, each of which a canonical form must have and none of which needs an oracle — idempotence, order independence over commutative operators, and agreement between writings of one expression:

	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 — 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; its eight failures are all ties settled by generation order.

The finding that matters most for 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. A comparison of printed forms calls them equal; a comparison of entities does not. The harness compares entities, which is the only reason it saw this.

Two defects rather than decisions

Both measured, both reproducible on their own:

"cos(0 ^ y)".InnerSimplified   ->  -(-1) provided ...   and again  ->  1 provided ...
"cos(-x)".Simplify()           ->  cos(-x)      while  "cos(-2 * x)".Simplify()  ->  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. Filed separately.

What the document specifies

Per node class it states the target, marking each line met or not met against the measurement. Leaves, the commutative operators (flat, ordered by a specified total order, constants folded), powers, functions, and the nodes that are not values.

One line is flagged as needing a maintainer's yes before anybody implements it: making subtraction and division sugar for a sum and a product. That is what makes the commutative laws reachable — while a difference is its own node, x - y and x + (-y) are different trees denoting one thing, and no amount of ordering sums fixes it — but it removes two node classes and 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.

x ^ 0 is the standing example of a canonicalisation a naive specification gets wrong: the library answers 1 provided not x = 0, and that is right.

And where a canonical form is actually available now

Rational functions over ℚ, where zero-equivalence is decidable and where 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.

Scope

Documentation only — three files, no code. canoncheck lives in the analysis workspace with the other harnesses rather than in this repository.

🤖 Generated with Claude Code

[Rafael-SOWNet]

Pushed a correction after measuring further, since the first version of the document got a claim wrong.

The total order already exists. RewriteRules.CanonicalOrderExact sorts and groups commutative operands by the whole subtree, and applying it before the normalisation 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 InnerSimplified does not run it, which is also most of why Simplify agrees so much more often.

And the real obstacle is confluence, not the order. Sorting then normalising is not idempotent — 21 of 834 — and every failure is the sort and Patterns.NumericNeatRules disagreeing about where a numeric operand belongs, each undoing the other:

1 / 2 - x   ->   -x + 1/2   ->   1/2 + -x   ->   ...

Neither is wrong alone. Until they agree, moving the order into the normalisation trades 2024 order failures for a form that never settles. §8's first item is now that question rather than "implement a total order".

The measurement table gains a third column for it, and is labelled with the build it was taken on — #929 and #930 are both fixed and land separately.