#253 partial order asnwer subsumption question

[Christophe Rey]

Hi every one,
there is something I do not understand with partial order answer subsumption (or maybe it is a bug, I do not know). It is illustrated on the following program in which I define the tabled predicate testPO/2 such that it must table only most specific answers (wrt term subsumption):

:- import subsumes_term/2 from subsumes.

:- table testPO(po(isSubsumedBy/2),_) as incremental.
isSubsumedBy(T1,T2):- subsumes_term(T2,T1).

testPO(f(A,B),foo) :-
    write('Call: '),
    writeln(testPO(f(A,B),foo) ),
    A == B.

:- table test/2 as incremental.

test(f(A,B),foo) :-
    write('Call: '),
    writeln(test(f(A,B),foo) ),
    A == B.

After compiling and running 2 queries I obtain:

| ?- [Compiling X:\Dropbox\Recherche\WFS\Implementation\xsbcodes\testPOtabling]
[testPOtabling compiled, cpu time used: 0.078 seconds]
[testPOtabling loaded]

yes
| ?- testPO(f(1,1),foo).
Call: testPO(f(_h550,_h551),foo)

no
| ?- test(f(1,1),foo).
Call: test(f(1,1),foo)

yes
| ?-

The first query seems to generate a wrong answer, while the second is ok. The first difference is that testPO/2 is defined using partial order answer subsumption. More precisely, in the first query, I do not understand why variables inside the f() term are not instanciated.

Thanks in advance for any help

Christophe

[David S. Warren]

Hi Christophe,
The way an aggregate predicate is processed when it is called with a non-variable in the aggregated position is to abstract that to a variable, then call the aggregate predicate and then see if the result is what is passed it. So your
| ?- testPO(f(1,1),foo).
is treated as though it were written as:
| ?- testPO(X,foo), X = f(1,1).
To see why it essentially has to do this, think of an aggregate like sum. To see if the sum of some set of numbers is, say, k, one has to add them up and then see if that is equal to k. Only looking at the aggregated values that are k doesn't work.
So that is why you see the printout of testPO(f(_h550,_h551),foo), and then, of course, _h550 is not the same term as _h551, which causes the failure.
I also note that you table the aggregate predicate "as incremental". I'd be surprised if that worked for aggregates. I don't think aggregate tables can be processed correctly with our incremental algorithm.
Regards,
-David

[Christophe Rey]

Many Thanks David.
I understand my mistake now.
I also apologize because I now realize the explanation is given in the manual at section 5.4.1. And for adding "as incremental", it is written at section 5.8.
However, your answer made me understand. So thank you again.
Best regards
Christophe