序言。如何检查两个数学表达式是否相同

Question

我正在编写一个序言程序，该程序将检查两个数学表达式是否实际上相同。例如，如果我的数学表达式目标是:(a + b) + c，则以下任何表达式都被视为相同:

(a+b)+c

a+(b+c)

(b+a)+c

(c+a)+b

a+(c+b)

c+(a+b)

以及其他组合

当然，我不希望检查可能答案的组合，因为表达式可能比这更复杂。

目前，这是我的方法:例如，如果我想检查 a + b *c 是否与另一个表达式(例如 c*b+a)相同，那么我将两个表达式递归地存储为二进制表达式，并且我应该创建一个规则(例如 ValueOf)，它将给出我是第一个表达式和第二个表达式的“值”。然后我只是检查两个表达式的“值”是否相同，然后我可以说两个表达式是相同的。问题是，由于表达式的内容不是数字，而是标识符，所以我无法使用 prolog 的“is”关键字来获取值。

有什么建议吗？

非常感谢

% represent a + b * c
binExprID(binEx1).
hasLeftArg(binEx1, a).
hasRightArg(binEx1, binEx2).
hasOperator(binEx1, +).

binExprID(binEx2).
hasLeftArg(binEx2, b).
hasRightArg(binEx2, c).
hasOperator(binEx2, *).

% represent c * b + a
binExprID(binEx3).
hasLeftArg(binEx3, c).
hasRightArg(binEx3, b).
hasOperator(binEx3, *).

binExprID(binEx4).
hasLeftArg(binEx4, binEx3).
hasRightArg(binEx4, a).
hasOperator(binEx4, +).

goal:- valueOf(binEx1, V),
       valueOf(binEx4, V).

Answer 1

数学表达式可能非常复杂，我认为您指的是算术。正常形式(我希望我的措辞合适)是“单项式之和”。

无论如何，这通常不是一件容易解决的任务，并且您的请求存在歧义:两个表达式在语法上可能不同(即它们的语法树不同)，但仍然具有相同的值。显然，这是由于操作使值保持不变，例如加/减 0。

根据您的描述，我推测您对“评估”身份感兴趣。然后，您可以在比较相等性之前对两个表达式进行标准化。

为了评估语法同一性，我会删除所有括号，将因素“分配”到加数上。该表达式成为乘法项的列表。本质上，我们得到一个列表列表，可以在不更改“值”的情况下对其进行排序。

表达式展平后，必须累加所有乘法常数。

一个简化的例子:

a+(b+c)*5 将是 [[1,a],[b,5],[c,5]] 而 a+5*(c+b) 将是 [[1,a],[5,c],[5,b]]

编辑经过一些改进，这是一个非常基本的规范化过程:

:- [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.

一些测试:

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

我使用了一些 SWI-Prolog 内置函数，例如 include/3、exclusion/3、foldl/5 和 msort/2 以避免丢失重复项。

这些是基本的list manipulation内置函数，如果您的系统没有它们，则可以轻松实现。

编辑

foldl/4 在 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).

处理部门

除法引入了一些复杂性，但这应该是预料之中的。毕竟，它引入了完整的数字类别:有理数。

这里是修改后的谓词，但我认为代码需要更多的调试。所以我还声称这个微重写系统可以解决什么问题的“单元测试”。另请注意，我没有自己引入否定。我希望您能做出任何需要的修改。

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

运行单元测试:

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