challenge my equational reasoner!
Sep. 15th, 2005 05:00 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslI'm really proud of my equational reasoner. Challenge me!
Using the operations of +, -, *, /, ^, and the alphabet of numbers and variables, please come up with two very different finite expressions, which are equivalent under equational algebra. My claim is that my system will reduce them both to the same normal form, unless one (or both) of them is a polynomial division.
(I have a vague suspicion that I'm reinventing Knuth-Bendix about 30 years too late).
Using the operations of +, -, *, /, ^, and the alphabet of numbers and variables, please come up with two very different finite expressions, which are equivalent under equational algebra. My claim is that my system will reduce them both to the same normal form, unless one (or both) of them is a polynomial division.
EXPRS := EXPR EXPRS EXPRS := [] EXPR := (+ EXPRS) EXPR := (* EXPRS) EXPR := (^ EXPR EXPR) EXPR := VAR EXPR := NUMBER
(I have a vague suspicion that I'm reinventing Knuth-Bendix about 30 years too late).