1% This file is part of the Attempto Parsing Engine (APE).
    2% Copyright 2008-2013, Attempto Group, University of Zurich (see http://attempto.ifi.uzh.ch).
    3%
    4% The Attempto Parsing Engine (APE) is free software: you can redistribute it and/or modify it
    5% under the terms of the GNU Lesser General Public License as published by the Free Software
    6% Foundation, either version 3 of the License, or (at your option) any later version.
    7%
    8% The Attempto Parsing Engine (APE) is distributed in the hope that it will be useful, but WITHOUT
    9% ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
   10% PURPOSE. See the GNU Lesser General Public License for more details.
   11%
   12% You should have received a copy of the GNU Lesser General Public License along with the Attempto
   13% Parsing Engine (APE). If not, see http://www.gnu.org/licenses/.
   14
   15
   16:- module(are_equivalent, [
   17		check_equivalence/2,
   18		are_equivalent/2,
   19		are_equivalent/3
   20	]).

Equivalence checking of two Attempto DRSs

author
- Kaarel Kaljurand
version
- 2011-07-21

BUG: Think if this code is correct and complete.

OBSOLETE COMMENT: Note that the DRACE-tester also uses the notion of equivalence defined here, but for DRACE it is sometimes too strict, e.g. DRACE NP considers reversing the arguments of `be' equivalence-preserving, to be able to perform the transformation:

John is every man. --> Every man is John.

But given the definition of equivalence here, they are not. Similarly:

If there is a man then it is necessary that a human is the man. --> Every man must be a human.

*/

   48:- use_module(drs_to_ascii).   49:- use_module(is_wellformed).   50:- use_module(drs_ops).   51
   52:- dynamic conds_unify/2.
 check_equivalence(+Drs1:term, +Drs2:term) is det
Arguments:
Drs1- is an Attempto DRS
Drs2- is an Attempto DRS
   60check_equivalence(Drs1, Drs2) :-
   61	are_equivalent(Drs1, Drs2),
   62	write('OK: the DRSs are equivalent.'), nl,
   63	!.
   64
   65check_equivalence(Drs1, Drs2) :-
   66	write('ERROR: the DRSs are NOT equivalent.'), nl,
   67	display_drs(Drs1),
   68	display_drs(Drs2).
 are_equivalent(+Drs1:term, +Drs2:term) is det
 are_equivalent(+Drs1:term, +Drs2:term, +Options:list) is det
 are_equivalent_x(+Drs1:term, +Drs2:term) is det
Arguments:
Drs1- is an Attempto DRS
Drs2- is an Attempto DRS
Options- is a list of options

The DRSs are equivalent iff they are well-formed and every condition list of Drs1 is a subset of some condition list of Drs2, and the other way around.

Valid options are:

ignore_sid(Bool)
If true then the sentence IDs are ignored during comparison, otherwise (default) the sentence IDs are taken into consideration.
   89are_equivalent(Drs1, Drs2) :-
   90	are_equivalent(Drs1, Drs2, []).
   91
   92are_equivalent(Drs1, Drs2, []) :-
   93	are_equivalent(Drs1, Drs2, [ignore_sid(false)]).
   94
   95are_equivalent(Drs1, Drs2, [ignore_sid(false)]) :-
   96	retractall(conds_unify(_, _)),
   97	assert(conds_unify(C-Id, C-Id)),
   98	assert(conds_unify(C-SId/_, C-SId)),
   99	assert(conds_unify(C-SId, C-SId/_)),
  100	!,
  101	are_equivalent_x(Drs1, Drs2).
  102
  103are_equivalent(Drs1, Drs2, [ignore_sid(true)]) :-
  104	retractall(conds_unify(_, _)),
  105	assert(conds_unify(C-_, C-_)),
  106	!,
  107	are_equivalent_x(Drs1, Drs2).
  108
  109are_equivalent_x(Drs1, Drs2) :-
  110	is_wellformed(Drs1),
  111	is_wellformed(Drs2),
  112	is_subdrs_of(Drs1, Drs2),
  113	is_subdrs_of(Drs2, Drs1).
 is_subdrs_of(+Drs1:term, +Drs2:term) is det
 is_subdrs_of_x(+Drs1:term, +Drs2:term) is det
Arguments:
Drs1- is an Attempto DRS
Drs2- is an Attempto DRS

Both DRSs are first copied to protect the original variables. The 2nd DRS is then numbervared. It is then checked if all the conditions of the 1st DRS occur (i.e. can be unified with some condition) in the 2nd DRS.

  127is_subdrs_of(drs(_, Conds1), drs(_, Conds2)) :-
  128	copy_term(Conds1, Conds1Copy),
  129	copy_term(Conds2, Conds2Copy),
  130	numbervars(Conds2Copy, 0, _),
  131	is_subdrs_of_x(drs(_, Conds1Copy), drs(_, Conds2Copy)).
  132
  133is_subdrs_of_x(drs(_, Conds1), drs(_, Conds2)) :-
  134	is_subcl_of(Conds1, Conds2).
 is_subcl_of(+ConditionList1:list, +ConditionList2:list) is det
Arguments:
ConditionList1- is a list of DRS conditions
ConditionList2- is a list of DRS conditions

eq:is_subcl_of([a(X)-1, b(Y)-1, c(X,Y)-1], [a(y)-1, b(x)-1, c(y,x)-1]). NOT eq:is_subcl_of([a(X)-1, b(Y)-1, c(X,Y)-1], [a(y)-1, b(x)-1, c(x,x)-1]).

  145is_subcl_of([], _).
  146
  147is_subcl_of([Condition | ConditionList1], ConditionList2) :-
  148	member_of_conds(Condition, ConditionList2),
  149	is_subcl_of(ConditionList1, ConditionList2).
 member_of_conds(+Condition:term, +ConditionList:list) is det
Arguments:
Condition- is a DRS condition
ConditionList- is a list of DRS conditions

BUG: it is probably better to use select/3 in order not to match the same condition more than once.

  160member_of_conds([H1|T1], [[H2|T2] | _]) :-
  161	is_subdrs_of_x(drs([],[H1|T1]), drs([],[H2|T2])).
  162
  163member_of_conds(Drs1, [Drs2 | _]) :-
  164	Drs1 =.. [Op, SubDrs1],
  165	Drs2 =.. [Op, SubDrs2],
  166	unary_drs_operator(Op),
  167	is_subdrs_of_x(SubDrs1, SubDrs2).
  168
  169% Experimental: allow (binary) disjunctions to match if they match
  170% after reordering of the elements, e.g. the DRS of "John drinks or eats."
  171% is equivalent to the DRS of "John eats or drinks."
  172member_of_conds(v(SubDrs1a, SubDrs1b), [v(SubDrs2a, SubDrs2b) | _]) :-
  173	is_subdrs_of_x(SubDrs1a, SubDrs2b), is_subdrs_of_x(SubDrs1b, SubDrs2a).
  174
  175member_of_conds(Drs1, [Drs2 | _]) :-
  176	Drs1 =.. [Op, SubDrs1a, SubDrs1b],
  177	Drs2 =.. [Op, SubDrs2a, SubDrs2b],
  178	binary_drs_operator(Op),
  179	is_subdrs_of_x(SubDrs1a, SubDrs2a),
  180	is_subdrs_of_x(SubDrs1b, SubDrs2b).
  181
  182member_of_conds(Label:Drs1, [Label:Drs2 | _]) :-
  183	is_subdrs_of_x(Drs1, Drs2).
  184
  185member_of_conds(Cond1, [Cond2 | _]) :-
  186	conds_unify(Cond1, Cond2).
  187
  188member_of_conds(Cond, [_ | CondsTail]) :-
  189	member_of_conds(Cond, CondsTail)