A canonical form for rational functions over Q (#934)

[Rafael-SOWNet]

Closes #934.

The part of the language where a canonical form is possible. There is none for the whole of it — zero-equivalence is undecidable once pi, the exponential, the trigonometric functions and abs are in play (Richardson 1968) — so the boundary is in the signature: anything that is not a rational function over ℚ gets no answer at all, never a normalisation that resembles one.

1/x + 1/y             ->  (x + y) / (x * y)
(x + y)/(x * y)       ->  (x + y) / (x * y)      the same tree, which nothing could do before
2 * x / (4 * y)       ->  1/2 * x / y
x / (2 * y)           ->  1/2 * x / y
(x^2 - 1) / (x - 1)   ->  x + 1 provided not x - 1 = 0
sin(x) / x            ->  refused

Two rational functions are equal exactly when this form is identical, so equality on that sublanguage is decided by comparing nodes rather than by searching — which is what a canonical form is for, and what (a - b).Simplify() against zero can never be.

What was actually missing

Four steps, and only the first is new. Nothing in the library put an expression over a common denominator — measured through Simplify, InnerSimplified and Factorize alike, and Simplify actively prefers the split form — so 1/x + 1/y and (x+y)/(x*y) could not be brought together by any existing route.

Gathering is a structural recursion over sums, differences, products, quotients and whole powers, taking the product of denominators rather than their least common multiple: both are correct, the product is cheaper to build, and the GCD removes the difference immediately afterwards.

The other three steps are existing parts. PolynomialGcd.Gcd reduces the quotient and verifies its own division by multiplying back. MultivariatePolynomial.LeadingCoefficient, from the Gröbner half of the class, gives the lexicographic leading coefficient to scale by, so the denominator comes out monic — without that, 2x/(4y) and x/(2y) stay different trees for one function, since a greatest common divisor is fixed only up to a unit.

The assertion the whole form rests on

Cancelling carries its condition. (x^2 - 1)/(x + 1) is undefined at x = -1 and x - 1 is not, so they are not the same function and the form must not equate them, however universally that cancellation is written. There is a test saying exactly that, beside one saying x/x is not 1.

(I wrote the opposite first — (x^2-1)/(x+1) equals x-1 as a same-function case — and it failed. The form was right and the test was wrong.)

Gathering over a common denominator widens nothing by itself, since a sum is defined exactly where its terms are, so no condition is invented where nothing was cancelled. That has a test too.

Scope

Offered and not applied: nothing in the library runs it, and a test pins that. No BREAKING-CHANGES.md entry — no input gives a different answer. The new public property is in PublicApi.txt.

Suite 6998 passed / 0 failed, of which 38 are new; F# 130/130; casbench 116/119 with 0 wrong, 0 error, 0 timeout; propcheck 1340/0; rootcheck 596/596; simpsweep 10463/10463.

🤖 Generated with Claude Code