Skip to content

A canonical form for rational functions over Q, which needs a common denominator first (#746 tier 1) #934

Description

@Rafael-SOWNet

What this is

The last piece of #746 tier 1's canonicaliser that has to be built rather than composed out of parts that already exist.

Docs/Contributing/CanonicalForm.md §2 records why there is no canonical form for the whole language — zero-equivalence is undecidable for rationals with pi, exp, the trigonometric functions and abs (Richardson 1968). §5 records where there is one: rational functions over ℚ in finitely many variables. For those, equality is decidable, the form is classical, and since #918 and #923 the library has the parts.

Transformation.Canonicalisation (#933) canonicalises the commutative structure. This is the other half.

What is missing, measured

Not the GCD — PolynomialGcd.TryCancel already parses both sides, computes the multivariate GCD, divides it out and verifies by multiplying back. What is missing is putting an expression over a common denominator at all. Measured on master at b4385a86:

"1/x + 1/y".Simplify()          ->  1 / x + 1 / y
"1/x + 1/y".InnerSimplified     ->  1 / x + 1 / y
"1/x + 1/y".Factorize()         ->  1 / x + 1 / y

and Simplify actively goes the other way:

"(x+y)/(x*y)".Simplify()        ->  1 / x + 1 / y provided not y = 0

So 1/x + 1/y and (x+y)/(x*y) are the same rational function and no route in the library brings them to a common form. Without that, any "canonical form for rational functions" is really a canonical form for expressions already written as a single quotient, which is a much smaller claim and not the one worth making.

(The provided not y = 0 on that last line is redundant rather than wrong — both forms are undefined at y = 0 — but it is asymmetric in x and y, which is worth a look while someone is in there.)

The shape of it

An operation with the boundary in its signature — false meaning "not a rational function over ℚ, and no canonical form is claimed", never a normalisation that merely looks like one:

  1. Gather the expression as a single quotient N/D, combining a sum of quotients over a common denominator. This is the new part.
  2. Parse N and D as MultivariatePolynomial over a fixed variable order.
  3. Divide both by PolynomialGcd.Gcd(N, D) — existing, and it verifies its own result.
  4. Make D monic in the monomial order, carrying the reciprocal of its leading coefficient into N, so that 2x/(4y) and x/(2y) agree.
  5. Coefficients to lowest terms; ERational does not do this on its own.

Two rational functions are then equal exactly when this form is identical, which makes equality a structural comparison rather than a search.

Worth checking before starting

  • The domain. Combining over a common denominator and cancelling is where a domain silently widens: x/x is not 1, and the library's existing convention is to attach the condition ((x^2-1)/(x-1) is x + 1 provided not x - 1 = 0). Whether the canonical form carries conditions, or refuses where one would be needed, is a decision to take deliberately — a form whose whole value is that equal trees mean equal expressions must not quietly compare two things with different domains as equal.
  • That step 1 does not fight Simplify, which prefers the split form and will pull it apart again. This probably wants to be an explicit operation that nothing calls by default, as Transformation.Canonicalisation is.
  • work/canoncheck in the analysis workspace is where the properties are checked — idempotence, order independence, agreement between writings. A rational-function canonical form should make 1/x + 1/y against (x+y)/(x*y) a listed agreement that passes.

Why it is worth doing

It is the piece of the language where a canonical form is possible, and it is a decision procedure for equality on it. Everything above tier 1 that wants to know whether two expressions are the same — the rewrite graph's congruence classes, the theorem graph's citations — wants this rather than (a - b).Simplify() against zero.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions