challenge my equational reasoner!

[gusl]

I'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.

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).

Comments

Karatsuba

[r6.livejournal.com]

Oh, this is exactly what I need today.

1. (a*c)*2^(m+m) = (a*2^m)*(c*2^m)
2. (a*c)*2^(m+m) + (a*d)*2^m = (a*2^m)*(d + c*2^m)
3. (a*c)*2^(m+m) + (b*c)*2^m = (b + a*2^m)*(c*2^m)
4. (a*c)*2^(m+m) + ((a+b)*(c+d) - (a*c + b*d))*2^m + b*d = (b + a*2^m)*(d + c*2^m)

Re: Karatsuba

[gustavolacerda.livejournal.com]

uhm... how do you get 4? (it passes my refuter, so no doubts about its truth)

Re: Karatsuba

[gustavolacerda.livejournal.com]

EBE> (simpl '(* (+ b (* a (^ 2 m))) (+ d (* c (^ 2 m)))))
(+ (* A C (^ 2 (* 2 M))) (* A D (^ 2 M)) (* B C (^ 2 M)) (* B D))

EBE> (simpl '(+ (* (* a c) (^ 2 (+ m m)))  (* (- (* (+ a b) (+ c d)) (+ (* a c) (* b d))) (^ 2 m)) (* b d)))
(+ (* A C (^ 2 (* 2 M))) (* A D (^ 2 M)) (* B C (^ 2 M)) (* B D))

They reduce to the same.

Re: Karatsuba

[gustavolacerda.livejournal.com]

my baby is obviously better than me!

[(Anonymous)]

What about

(a) ( X^5 - 1 ) / ( X - 1 )
(b) ( X^4 + X^3 + X^2 + X + 1 )

or does the fact that (a) is not defined at x=1 break it? If it does matter, division is basically pointless in your list of valid operators, since there's always a zero root.

[gustavolacerda.livejournal.com]

you got me! Factoring is its main weakness, I think. But I'd be surprised if you found anything else.

I basically ignore the division-by-zero problem, by saying that you can always cancel out.

Would you care to tell me who you are?

Sorry :)

[maustin.livejournal.com]

Sorry, I thought I was logged on. I can't remember how I ended up friending you, but it was many months ago.

[(Anonymous)]

So, I think if you remove "/" from the list, it'll work. After that it's simply a matter of distributing/associating/commuting.

It'd be interesting to see if the following work:

(1a) ( X + 1 ) ^ 100
(1b) ( X^2 + X + 1 ) ^ 50

(2a) X ^ ( X + 1 ) / X ^ ( X - 1 )
(2b) X ^ 2

(3a) (( X + X ) ^ ( X + X )) ^ ( X + X )
(3b) (( 2 * X ) ^ 4 ) ^ ( X ^ 2 )