Normal Form for Polynomial Formulas

[dodo]

"Normal form" for formulas

I am about to set myself the following programming exercise; let me know if this would be useful in any way, or how can it be improved into something useful.

Suppose I restrict myself to formulas in polynomials of Q, including polynomial fractions. My intention is to define a "normal form" for such formulas, say, "reduce any possible formula to a polynomial or, if not possible, to a polynomial fraction where the highest coefficient in the denominator is 1". Namely, prefer {{2 \over 3} x^2 + {5 \over 3} x + {7 \over 3}} \over {x + {11 \over 3}} over {2x^2 + 5x + 7} \over {3x + 11}.

The intention is reduce to "normal form" any expression entered by the user. This way, two expressions can be proved equal if they reduce to the same normal form.

If a formula is reduced to a normal form by automated, reversible steps, then an "equation prover" is straightforward: just reduce the LHS and RHS to normal form, and compare if equal; if so, show the steps from LHS to normal form and, reversed, the steps to RHS.

Constants and variables would be stored in infinite precision, fractional form (a numerator and a denominator, with gcd=1). Calculations would be performed in the same manner.

 

[Tac-Tics]

I've done something similar for rational polynomials. The hardest part is probably going to be a toString method for your polynomial class =-) You wouldn't think it, but rules for writing algebraic expressions are arbitrary and complicated!

 

[dodo]

Yes, I know exactly what you mean... which is why I decided I won't spend a minute on output. The output will go on a text line, much like the input, period.

My major concern is: does it exist such a thing as a "normal form"?

That's why I'm limiting the domain, thus avoiding formulas like x^y. But I would really like to include formulas in many variables and, if possible, implement substitution. (Without the program deciding what to substitute in order to accomplish a proof; that might be hard.)

 

[Hurkyl]

You can normalize univariate rational functions the same way as rational numbers -- put it into lowest terms, normalize the numerator, denominator, and that fixes everything up to a choice of signs (you can flip the signs on both terms without changing the rational function), which you make an extra case for.

For the record, this means you're going to have to implement a polynomial GCD, along with polynomial division.

(I'm assuming you want to keep everything in the form of a single rational function expression, rather than other sorts of forms... e.g. the thing you get from partial fractions, or a list of sufficiently many point-value pairs)And for the record, things are a lot simpler because you're working with integer/rational coefficients... because you have unique factorization into irreducible elements (times a leading sign), and even more because the Euclidean algorithm is usable.

 

[dodo]

Indeed, part of the idea is to get an insight on the algebraic structures below. So this information is, as always, very valuable to me.