- #1
dodo
- 697
- 2
"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 [tex]{{2 \over 3} x^2 + {5 \over 3} x + {7 \over 3}} \over {x + {11 \over 3}}[/tex] over [tex]{2x^2 + 5x + 7} \over {3x + 11}[/tex].
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.
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 [tex]{{2 \over 3} x^2 + {5 \over 3} x + {7 \over 3}} \over {x + {11 \over 3}}[/tex] over [tex]{2x^2 + 5x + 7} \over {3x + 11}[/tex].
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.