Prolog. How to check if two math expressions are the same

logic, predicate, prolog

Solution

Math expressions can be very complex, I presume you are referring to arithmetic instead. The normal form (I hope my wording is appropriate) is 'sum of monomials'.

Anyway, it's not an easy task to solve generally, and there is an ambiguity in your request: 2 expressions can be syntactically different (i.e. their syntax tree differ) but still have the same value. Obviously this is due to operations that leave unchanged the value, like adding/subtracting 0.

From your description, I presume that you are interested in 'evaluated' identity. Then you could normalize both expressions, before comparing for equality.

To evaluate syntactical identity, I would remove all parenthesis, 'distributing' factors over addends. The expression become a list of multiplicative terms. Essentially, we get a list of list, that can be sorted without changing the 'value'.

After the expression has been flattened, all multiplicative constants must be accumulated.

a simplified example:

`a+(b+c)*5` will be `[[1,a],[b,5],[c,5]]` while `a+5*(c+b)` will be `[[1,a],[5,c],[5,b]]`

edit after some improvement, here is a very essential normalization procedure:

:- [library(apply)].

arith_equivalence(E1, E2) :-
    normalize(E1, N),
    normalize(E2, N).

normalize(E, N) :-
    distribute(E, D),
    sortex(D, N).

distribute(A, [[1, A]]) :- atom(A).
distribute(N, [[1, N]]) :- number(N).
distribute(X * Y, L) :-
    distribute(X, Xn),
    distribute(Y, Yn),
    % distribute over factors
    findall(Mono, (member(Xm, Xn), member(Ym, Yn), append(Xm, Ym, Mono)), L).
distribute(X + Y, L) :-
    distribute(X, Xn),
    distribute(Y, Yn),
    append(Xn, Yn, L).

sortex(L, R) :-
    maplist(msort, L, T),
    maplist(accum, T, A),
    sumeqfac(A, Z),
    exclude(zero, Z, S),
    msort(S, R).

accum(T2, [Total|Symbols]) :-
    include(number, T2, Numbers),
    foldl(mul, Numbers, 1, Total),
    exclude(number, T2, Symbols).

sumeqfac([[N|F]|Fs], S) :-
    select([M|F], Fs, Rs),
    X is N+M,
    !, sumeqfac([[X|F]|Rs], S).
sumeqfac([F|Fs], [F|Rs]) :-
    sumeqfac(Fs, Rs).
sumeqfac([], []).

zero([0|_]).
mul(X, Y, Z) :- Z is X * Y.

Some test:

?- arith_equivalence(a+(b+c), (a+c)+b).
true .

?- arith_equivalence(a+b*c+0*77, c*b+a*1).
true .

?- arith_equivalence(a+a+a, a*3).
true .

I've used some SWI-Prolog builtin, like include/3, exclude/3, foldl/5, and msort/2 to avoid losing duplicates.

These are basic list manipulation builtins, easily implemented if your system doesn't have them.

edit

foldl/4 as defined in SWI-Prolog apply.pl:

:- meta_predicate
    foldl(3, +, +, -).

foldl(Goal, List, V0, V) :-
    foldl_(List, Goal, V0, V).

foldl_([], _, V, V).
foldl_([H|T], Goal, V0, V) :-
    call(Goal, H, V0, V1),
    foldl_(T, Goal, V1, V).

handling division

Division introduces some complexity, but this should be expected. After all, it introduces a full class of numbers: rationals.

Here are the modified predicates, but I think that the code will need much more debug. So I allegate also the 'unit test' of what this micro rewrite system can solve. Also note that I didn't introduce the negation by myself. I hope you can work out any required modification.

/*  File:    arith_equivalence.pl
    Author:  Carlo,,,
    Created: Oct  3 2012
    Purpose: answer to http://stackoverflow.com/q/12665359/874024
             How to check if two math expressions are the same?
         I warned that generalizing could be a though task :) See the edit.
*/

:- module(arith_equivalence,
      [arith_equivalence/2,
       normalize/2,
       distribute/2,
       sortex/2
      ]).

:- [library(apply)].

arith_equivalence(E1, E2) :-
    normalize(E1, N),
    normalize(E2, N), !.

normalize(E, N) :-
    distribute(E, D),
    sortex(D, N).

distribute(A, [[1, A]]) :- atom(A).
distribute(N, [[N]]) :- number(N).
distribute(X * Y, L) :-
    distribute(X, Xn),
    distribute(Y, Yn),
    % distribute over factors
    findall(Mono, (member(Xm, Xn), member(Ym, Yn), append(Xm, Ym, Mono)), L).
distribute(X / Y, L) :-
    normalize(X, Xn),
    normalize(Y, Yn),
    divide(Xn, Yn, L).
distribute(X + Y, L) :-
    distribute(X, Xn),
    distribute(Y, Yn),
    append(Xn, Yn, L).

sortex(L, R) :-
    maplist(dsort, L, T),
    maplist(accum, T, A),
    sumeqfac(A, Z),
    exclude(zero, Z, S),
    msort(S, R).

dsort(L, S) :- is_list(L) -> msort(L, S) ; L = S.

divide([], _, []).
divide([N|Nr], D, [R|Rs]) :-
    (   N = [Nn|Ns],
        D = [[Dn|Ds]]
    ->  Q is Nn/Dn,  % denominator is monomial
        remove_common(Ns, Ds, Ar, Br),
        (   Br = []
        ->  R = [Q|Ar]
        ;   R =  [Q|Ar]/[1|Br]
        )
    ;   R = [N/D]    % no simplification available
    ),
    divide(Nr, D, Rs).

remove_common(As, [], As, []) :- !.
remove_common([], Bs, [], Bs).
remove_common([A|As], Bs, Ar, Br) :-
    select(A, Bs, Bt),
    !, remove_common(As, Bt, Ar, Br).
remove_common([A|As], Bs, [A|Ar], Br) :-
    remove_common(As, Bs, Ar, Br).

accum(T, [Total|Symbols]) :-
    partition(number, T, Numbers, Symbols),
    foldl(mul, Numbers, 1, Total), !.
accum(T, T).

sumeqfac([[N|F]|Fs], S) :-
    select([M|F], Fs, Rs),
    X is N+M,
    !, sumeqfac([[X|F]|Rs], S).
sumeqfac([F|Fs], [F|Rs]) :-
    sumeqfac(Fs, Rs).
sumeqfac([], []).

zero([0|_]).
mul(X, Y, Z) :- Z is X * Y.

:- begin_tests(arith_equivalence).

test(1) :-
    arith_equivalence(a+(b+c), (a+c)+b).

test(2) :-
    arith_equivalence(a+b*c+0*77, c*b+a*1).

test(3) :-
    arith_equivalence(a+a+a, a*3).

test(4) :-
    arith_equivalence((1+1)/x, 2/x).

test(5) :-
    arith_equivalence(1/x+1, (1+x)/x).

test(6) :-
    arith_equivalence((x+a)/(x*x), 1/x + a/(x*x)).

:- end_tests(arith_equivalence).

running the unit test:

?- run_tests(arith_equivalence).
% PL-Unit: arith_equivalence ...... done
% All 6 tests passed
true.

Problem

Original source