subsumes/2 vs. subsumes_chk/2

[Ulrich Neumerkel]

Have you written any form of loop checker or subsumption test?  Does
anybody use the built-in predicate subsumes/2?  Please tell me!

While I have used subsumes_chk/2 a lot for various forms of loop
checkers and theorem provers, I have not seen a single case of
subsumes/2.  But currently only subsumes/2 is part of WG17's core
document.  See

http://www.complang.tuwien.ac.at/ulrich/iso-prolog/built-in_predicates

I believe subsumes/2 should be replaced by subsumes_chk/2.  Or at
least subsumes/2 should be defined in terms of subsumes_chk/2 only.
Here is why:


Both date back to the early 1980s to the DEC library's library
METUL.PL written by Richard O'Keefe 1983-05-20.  Quite surprisingly,
its subsumes/2 implementation seems to be correct - in contrast to
many newer implementations.

Both subsumes/2 and subsumes_chk/2 can be expressed by each other as
long as syntactic unification is considered.

subsumes(General, Specific) :-
   subsumes_chk(General, Specific),
   General = Specific.

subsumes_chk(General, Specific) :-
   \+ \+ subsumes(General, Specific).

If both can be expressed by each other - why bother?

The difference appears when constraints come into play. (Of course
constraints are not part of the standard, but all relevant systems
have them in the meantime, so avoiding unnecessary collisions is
helpful.)

In principle the built-in predicates cannot understand constraints as
their meaning is pretty difficult to describe and to decide (sometimes
impossible), so we could only go for syntactic unification and ignore
constraints.  SWI behaves here quite unintuitively:

?- use_module(library(clpfd)).

?- X in 1..2, subsumes_chk(General,X).
false.

?- X in 1..2, subsumes_chk(X,X).
false.

?- Y = a, freeze(X,write(wakeup(X))), subsumes_chk(X,Y).
wakeup(a)
Y = a,
freeze(X, write(wakeup(X))).

?- freeze(X,write(wakeup(X))), subsumes_chk(X,Y).
false.

This means, by removing Y = a (from an unconstrained variable) we can
turn success to failure.

The best would be to define subsumes_chk/2 exclusively as a test for
syntactic unification only - without waking up any constraints.  This
is the way it is done in SICStus.  Based on subsumes_chk/2, subsumes/2
can be defined as a bootstrapped built-in predicate.  Now unification
would trigger constraints - but that seems to be inevitable for a
predicate that is supposed to perform general unification.



BTW, the following case is NSTO, still an error is produced.

?- set_prolog_flag(occurs_check, error).
true.

?- subsumes_chk(X, f(X)).
ERROR: subsumes_chk/2: Cannot unify _G1513 with f(_G1513): would create an infinite tree

subsumes_chk/2 never creates an infinite tree - nor does subsumes/2.
Well, actually subsumes/2 may produce one in case some extra goal is
triggered, like ?- freeze(X, Y=s(Y)), subsumes(X,a).
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Bart Demoen-2]

> Have you written any form of loop checker or subsumption test?  Does
> anybody use the built-in predicate subsumes/2?  Please tell me!

I always end up writing (or reusing) my own subsumes/2 - mainly
because it seems different in different implementations (although I do
not check whether this is still true).

I am always surprised (in the negative sense) when subsumes/2 also
unifies the arguments. Seems like that functionality warrants a
different name.

And also when the occurence of the same variable X in both arguments
of subsumes/2 confuses the predicate:

   ?- subsumes_check(f(X,Y),f(Z,X)).

I think it succeeds in some systems, and does not in others.


> I believe subsumes/2 should be replaced by subsumes_chk/2.
If I understand you correctly, I agree :-)

> This means, by removing Y = a (from an unconstrained variable) we can
> turn success to failure.

That's not uncommon - consider the goals

?- Y = a, Y == a.
and
?- Y == a.



> The best would be to define subsumes_chk/2 exclusively as a test for
> syntactic unification only - without waking up any constraints.

It feels like you want to work towards consistent behaviour of
builtins (or lib preds) wrt constraints - I applaud that. It would
help if you had some general principles.

> BTW, the following case is NSTO, still an error is produced.
>
> ?- set_prolog_flag(occurs_check, error).
> true.
>
> ?- subsumes_chk(X, f(X)).
> ERROR: subsumes_chk/2: Cannot unify _G1513 with f(_G1513): would create an infinite tree

That feels like a bug to me. Using copy_term_nat/2 before doing the
implementation would solve that, no ?

Cheers

Bart Demoen

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

Bart Demoen writes:
>I am always surprised (in the negative sense) when subsumes/2 also
>unifies the arguments. Seems like that functionality warrants a
>different name.

This name subsumes/2 *is* irritating. It has been around since 1983.
semi_unify/2 would be an imperative name.  Actually, there is a
forall-quantor for the specific part - so equal(s)_forall/2 ...

I have so far only seen uses of subsumes/2 where subsumes_chk/2 would
have been just as good, so maybe we can just give up searching a
better name.

>And also when the occurence of the same variable X in both arguments
>of subsumes/2 confuses the predicate:
>
>   ?- subsumes_check(f(X,Y),f(Z,X)).
>
>I think it succeeds in some systems, and does not in others.

?- subsumes(X, f(X)).

Even succeeds frequently (and incorrectly).

At least, since Pasadena it is now clearly defined.  subsumes/2
implements semi-unification.  That is like unification, but it fails
if Specific is affected.
http://www.complang.tuwien.ac.at/ulrich/iso-prolog/built-in_predicates#subsumes_chk_2

>> I believe subsumes/2 should be replaced by subsumes_chk/2.
>If I understand you correctly, I agree :-)
...
>> The best would be to define subsumes_chk/2 exclusively as a test for
>> syntactic unification only - without waking up any constraints.
>
>It feels like you want to work towards consistent behaviour of
>builtins (or lib preds) wrt constraints - I applaud that. It would
>help if you had some general principles.

Currently, I rather try to avoid useless collisions ahead.  By
defining subsumes_chk/2 alone (and thus only syntactically), some
problems could be avoided.  It does not make sense to take constraints
into account by subsumes_chk/2, as constraints can be anything from

    freeze(X, true) or  dif(X, _)

up to

    freeze(X, false) or X #> Y, Y #> X.

In between those extremes lies the wondrous world of constraints.
Since constraints can imply any terms, any default action would be
futile.  To see this, rewrite a particular test by wrapping each
argument of subsumes_chk/2 like freeze(Arg, Arg = some(term,Y)).

And for those who have to take constraints into account, copy_term/3
can help out.  They would need to analyse the constraints in detail
anyway.

>> BTW, the following case is NSTO, still an error is produced.
>>
>> ?- set_prolog_flag(occurs_check, error).
>> true.
>>
>> ?- subsumes_chk(X, f(X)).
>> ERROR: subsumes_chk/2: Cannot unify _G1513 with f(_G1513): would create an infinite tree
>
>That feels like a bug to me. Using copy_term_nat/2 before doing the
>implementation would solve that, no ?

Maybe subsumes_chk could turn off temporally occurs-check checking
similar to unifiable/3.
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Richard O'Keefe]

I think the main issue is that a lot of decisions that made sense
back in the 1980s make rather less sense when we have
  - officially blessed cyclic terms
  - constraints

Getting this right is going to require extreme attention to detail.
Ulrich pointed me to a thread and I've now forgotten the name of
who made the observation, but given the ground (but cyclic) terms
        A = f(B, 0),
        B = f(A, 1),
there's no *obvious* way to extend the classic definition of term
ordering to compare(R, A, B).  (Under the usual lexicographic order,
if A @< B, then since the first argument of A is B and that of B is
A, it follows that A @> B.  Oops.)


_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

There is one buring question open: Have you ever used subsumes/2 in a
situation where subsumes_chk/2 would not have been as good?

Would you agree to remove subsumes/2 entirely?  And replace it by
subsumes_chk/2?

>I think the main issue is that a lot of decisions that made sense
>back in the 1980s make rather less sense  when we have
>  - officially blessed cyclic terms

We can take for granted that syntactic unification terminates always.
Cycles are an option.  The best support for cycles is in SWI
currently.  Here, only asserta/1 doesn't work.  It would help if

  ?- X = s(X), asserta(S).

would produce a representation error, as this can be considered an
implementation defined limit which has been breached (7.12.2 f).  It
cannot be a type error as that fact is as well defined as any other
rational tree.  As a resource errorthis could be misinterpreted for
having not enough memory.

>  - constraints

Here is one thing that I stumbled over when reading your definition in
METUTL.PL - actually from AIAI Note No. 103 of 1987-11-12, (which has
some accidental code duplication).  variables_of/2 is term_variables/2.

% subsumes(+General, +Specific)
% True if Specific can be found by instantiating variables in General
% for instance, subsumes(foo(X), foo(bar)) is true.

subsumes(General, Specific) :-
        variables_of(Specific, Vars),
        subsumes(General, Specific, Vars).

subsumes(General, Specific, Vars) :-
        var(General),
        var_member_chk(General, Vars),
        !,
        General == Specific.

subsumes(General, Specific, _) :-
        var(General),
        !,
        General = Specific. %  binds

subsumes(General, Specific, Vars) :-
        nonvar(Specific), %  mustn't bind it
        functor(General,  FunctionSymbol, Arity),
        functor(Specific, FunctionSymbol, Arity),
        subsumes(Arity, General, Specific, Vars).

subsumes(0, _, _, _) :- !.

subsumes(N, General, Specific, Vars) :-
        arg(N, General,  GenArg),
        arg(N, Specific, SpeArg),
        subsumes(GenArg, SpeArg, Vars),
        M is N-1, !,
        subsumes(M, General, Specific, Vars).


Why is this sooo complex?, I thought.  Why not simply:

subsumes(General, Specific) :-
        term_variables(Specific, Vars1),
        General = Specific,
        \+ \+ maplist(\X^(var(X),X=a), Vars1).

In systems with constraints waking up constraints due to X=a could
lead to unexpected failure or even type errors in library(clpfd).  So
we have to circumscribe it:

        maplist(var,Vars1),
        term_variables(Vars1, Vars2),
        Vars1 == Vars2.

I was aware of possible cycles created by General = Specific.  But if
a cycle gets created, some variables in Vars1 would be bound and
maplist(var,Vars1) would fail over the evil cycle.  No need to go
through all the terms in detail.

I was wrong: The code had to be that complex for systems not
supporting cyclic terms.  I will leave the answer open, maybe someone
wants to look at it.


But then, there are further problems with BOTH implementations - even
if cycles are supported and constraints politely ignored!  The biggest
problem is that its runtime is always proportional to the size of
Specific.  Even if I do - say

?- \ ( length(L, 1600000), repeat, time(subsumes([], L)) ).
% 1 inferences, 0.45 CPU in 0.75 seconds (60% CPU, 2 Lips)

(I put that lambda around to avoid getting L printed.)  You can see
how much time subsumes/2 needlessly consumes!  2 Lips ...

Maybe it is better to first gather, effectively mark, the variables of
General?  Not sure.

But one thing seems to make sense: Prior to performing the actual
semi-unification, a test for equality/disequality can rule out all
cases were general unification would fail or unconditionally succeed:

bettersubsumes_chk(General, Specific) :-
   (  ?=(General, Specific)
   -> General == Specific
   ;  subsumes_chk(General, Specific)
   ).

An actual implementation could go even further: If the first attempted
unification in ?= would bind a variable in the right hand side,
subsumes_chk/2 could fail over immediately.  Also, there would be no
need for the extra ==/2 check.
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

>Ulrich pointed me to a thread and I've now forgotten the name of
>who made the observation, but given the ground (but cyclic) terms
> A = f(B, 0),
> B = f(A, 1),
>there's no *obvious* way to extend the classic definition of term
>ordering to compare(R, A, B).  (Under the usual lexicographic order,
>if A @< B, then since the first argument of A is B and that of B is
>A, it follows that A @> B.  Oops.)

Mats Carlsson reported this 1996-07-16:

http://groups.google.at/group/comp.lang.prolog/browse_thread/thread/3a6f1b4d9fcca26e/

In that thread Bernhard Pfahringer and others discussed various
attempts to find a new term order.  I do not completely recall it but
as far as I remember it did collide "too much" with what one expects
from term ordering.

Maybe someone wants to go through it?
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Jan Wielemaker-3]

On Monday 02 November 2009 04:52:56 pm Ulrich Neumerkel wrote:

> >Ulrich pointed me to a thread and I've now forgotten the name of
> >who made the observation, but given the ground (but cyclic) terms
> > A = f(B, 0),
> > B = f(A, 1),
> >there's no *obvious* way to extend the classic definition of term
> >ordering to compare(R, A, B).  (Under the usual lexicographic order,
> >if A @< B, then since the first argument of A is B and that of B is
> >A, it follows that A @> B.  Oops.)
>
> Mats Carlsson reported this 1996-07-16:
>
> http://groups.google.at/group/comp.lang.prolog/browse_thread/thread/3a6f1b4
>d9fcca26e/
>
> In that thread Bernhard Pfahringer and others discussed various
> attempts to find a new term order.  I do not completely recall it but
> as far as I remember it did collide "too much" with what one expects
> from term ordering.
>
> Maybe someone wants to go through it?

It reminds me of a similar problem I studied recently: ordering of RDF
triples consisting of blank nodes that form a cycle. According to the
literature, there is a `solution' to this problem, but it is
computational very expensive. I don't have the reference at hand right
now.

        --- Jan

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

On my quest to find one (1) instance where subsumes/2 is used in a
manner different to subsumes_chk/2,  i.e., where the bindings of
subsumes(General, Specifc) are exploited for good, I came across a
review of Richard O'Keefe about the first edition of Knowledge Systems
and Prolog by Adrian Walker, Michael McCord, J.F. Sowa, and Walter
G. Wilson.

From the PROLOG Digest Sunday, 10 July 1988 Volume 6 : Issue 42:

http://groups.google.at/group/comp.lang.prolog/msg/687ebae095200e9e

Quote

For now I'd just like to comment on one particular example, found
found on page 413.  I'll transliterate it into Edinburgh syntax.

...

%   most_general_terms_in_order(TermsInOrder, GeneralTerms)
%   is just like most_general_terms/2, except that less general terms
%   precede more general terms in TermsInOrder (that is, if X and Y
%   are both in TermsInOrder and X subsumes Y, X must follow Y).  The
%   order of terms in the result is the same as the order in the input.

most_general_terms_in_order([], []).
most_general_terms_in_order([Term|Terms], GeneralTerms) :-
        member(MoreGeneral, Terms),
        subsumes(MoreGeneral, Term),
        !,
        most_general_terms_in_order(Terms, GeneralTerms).
most_general_terms_in_order([Term|Terms], [Term|GeneralTerms]) :-
        most_general_terms_in_order(Terms, GeneralTerms).

End Quote

What happens here, is that MoreGeneral terms will be bound to the more
specific term it is supposed to subsume.  Clearly, this cannot work.

?- most_general_terms_in_order([f(1),f(2),f(X)], Xs).
X = 1,
Xs = [f(2), f(1)].

The X = 1 is telling it all!  So we get the opposite of what was
intended. We get in this case the most specific instances.  Could be a
typo.  subsumes_chk/2 works as expected:

?- most_general_terms_in_order([f(1),f(2),f(X)], Xs).
Xs = [f(X)].

In the original book it reads on page 413 in VM/Prolog syntax:

most_gen1(nil,nil).
most_gen1(R.Rs,Gs) <-
    member(G,Rs) & mg(G,R) & / & most_gen1(Rs,Gs).
most_gen1(R.Rs,R.Gs) <- most_gen1(Rs,Gs).

mg(U,V) <- -+ -+(U=V) & copy(U,UU) & copy(V,VV) &
    UU=VV & V=*=VV & -+(U=*=UU).

-+ should be a logical not sign (EBCDIC decimal 95).

So that would be today:

mg(U,V) :- \+ \+(U=V), copy_term(U,UU), copy_term(V,VV),
    UU=VV, variant(V,VV), \+ variant(U,UU).

In any case, no binding takes place anywhere.

In summary, this was a case where subsumes/2 leads to an incorrect
program even without constraints.

It really seems to be the best to abandom the unifying subsumes/2
altogether.
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Paulo Moura]

Hi,

The name subsumes_chk/2 is an ugly name for a standard predicate.  
Moreover, when no other "checking" predicate in the current standard  
or in the current standardization proposals uses such an ugly suffix.

Given that subsumes/2 seems to be almost never used (as per Ulrich's  
findings), I suggest that subsumes/2 takes the role of subsumes_chk/2  
as the *built-in* predicate for checking term subsumption and that the  
older definition of both subsumes/2 and subsumes_chk/2 be added as a  
library for backward portability.

Cheers,

Paulo


-----------------------------------------------------------------
Paulo Jorge Lopes de Moura, PhD
Assistant Professor
Dep. of Computer Science, University of Beira Interior
6201-001 Covilhã, Portugal

Office 3.18  Ext. 3276
Phone: [phone] Fax: [phone]
Email: <mailto:pmoura@...>

Home page: <http://www.di.ubi.pt/~pmoura>
Research:  <http://logtalk.org/> Blog: <http://blog.logtalk.org/>
-----------------------------------------------------------------

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Feliks Kluzniak-2]

This proposal sounds very reasonable to me.

-- Feliks



-----Original Message-----
From: swi-prolog-admin@...
[mailto:swi-prolog-admin@...] On Behalf Of Paulo Moura
Sent: Tuesday, November 10, 2009 5:53 AM
To: SWI-Prolog mailinglist
Subject: Re: [SWIPL] subsumes/2 vs. subsumes_chk/2


Hi,

The name subsumes_chk/2 is an ugly name for a standard predicate.  
Moreover, when no other "checking" predicate in the current standard  
or in the current standardization proposals uses such an ugly suffix.

Given that subsumes/2 seems to be almost never used (as per Ulrich's  
findings), I suggest that subsumes/2 takes the role of subsumes_chk/2  
as the *built-in* predicate for checking term subsumption and that the  
older definition of both subsumes/2 and subsumes_chk/2 be added as a  
library for backward portability.

Cheers,

Paulo


-----------------------------------------------------------------
Paulo Jorge Lopes de Moura, PhD
Assistant Professor
Dep. of Computer Science, University of Beira Interior
6201-001 Covilhã, Portugal

Office 3.18  Ext. 3276
Phone: [phone] Fax: [phone]
Email: <mailto:pmoura@...>

Home page: <http://www.di.ubi.pt/~pmoura>
Research:  <http://logtalk.org/> Blog: <http://blog.logtalk.org/>
-----------------------------------------------------------------

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Richard O'Keefe]

On Nov 11, 2009, at 12:52 AM, Paulo Moura wrote:

>
> Hi,
>
> The name subsumes_chk/2 is an ugly name for a standard predicate.

Ugly it may be, but it is intention-revealing.
subsumes : subsumes_chk :: member : memberchk

These predicates were originally developed for "expert systems"
where both versions were useful, and it was important to know
whether one was going to bind variables (in a form of one-way
matching) or not.  Simply replacing subsumes_chk by subsumes
isn't ideal, especially as there is a wider reading of subsumption
where we ask if one _clause_ (= disjunction of goals) subsumes
another.  I suggest that something like term_subsumes/2 might
avoid that ambiguity.

For me, the big problem, indeed, a real show-stopper of a
problem, is that we know perfectly well what subsumption
of terms OUGHT to mean:  G1 subsumes G2 if and only if
any possible instance of G2 is a possible instance of G1,
and "possible" here has to mean "consistent with constraints"
if the predicate is to be useful for the kind of thing it was
invented for.  A purely syntactic test that ignores constraints
seems as though it is bound to give wrong answers.

If we can't get that right, it's better to leave the operation
out.  Don't you think it would be confusing to have a
unification that _does_ respect constraints but a subsumption
that _doesn't_?


_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Bart Demoen-2]

> I suggest that something like term_subsumes/2 might
> avoid that ambiguity.

I second that. Re-using old names with a new meaning seems not right.

> A purely syntactic test that ignores constraints
> seems as though it is bound to give wrong answers.

One could also go the following way: if any of the arguments of
term_subsumes/2 contains constrained variables, throw an error.

Or as an alternative (using copy_term_nat and maybe applicable to
other situations) define (in this case):

term_subsumes(T1,T2) :-
                     copy_term_nat(T1,S1),
                     copy_term_nat(T2,S2),
                     subsumes_chk(S1,S2). % the old subsumes_chk


> If we can't get that right, it's better to leave the operation out.

The operation seems too useful to be left out completely.

Cheers

Bart Demoen

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Paulo Moura]

On 2009/11/10, at 21:22, Richard O'Keefe wrote:

> On Nov 11, 2009, at 12:52 AM, Paulo Moura wrote:
>
>> The name subsumes_chk/2 is an ugly name for a standard predicate.
>
> Ugly it may be, but it is intention-revealing.
> subsumes : subsumes_chk :: member : memberchk

But both member/2 and memberchk/2 perform instantiations, subsumes_chk/
2 doesn't. I see a subsumes/2 predicate that (only) checks for  
subsumption in the same class as ground/1, integer/1, etc.

> These predicates were originally developed for "expert systems"
> where both versions were useful, and it was important to know
> whether one was going to bind variables (in a form of one-way
> matching) or not.  Simply replacing subsumes_chk by subsumes
> isn't ideal, especially as there is a wider reading of subsumption
> where we ask if one _clause_ (= disjunction of goals) subsumes
> another.  I suggest that something like term_subsumes/2 might
> avoid that ambiguity.

Which would also avoid trouble with backward portability.

> For me, the big problem, indeed, a real show-stopper of a
> problem, is that we know perfectly well what subsumption
> of terms OUGHT to mean:  G1 subsumes G2 if and only if
> any possible instance of G2 is a possible instance of G1,
> and "possible" here has to mean "consistent with constraints"
> if the predicate is to be useful for the kind of thing it was
> invented for.  A purely syntactic test that ignores constraints
> seems as though it is bound to give wrong answers.
>
> If we can't get that right, it's better to leave the operation
> out.  Don't you think it would be confusing to have a
> unification that _does_ respect constraints but a subsumption
> that _doesn't_?

I agree that constraints are an important extension to Prolog but I  
would really like to see a constraints standardization proposal before  
discussing what we should do or not do in a Prolog standard.

Best regards,

Paulo


-----------------------------------------------------------------
Paulo Jorge Lopes de Moura, PhD
Assistant Professor
Dep. of Computer Science, University of Beira Interior
6201-001 Covilhã, Portugal

Office 3.18  Ext. 3276
Phone: [phone] Fax: [phone]
Email: <mailto:pmoura@...>

Home page: <http://www.di.ubi.pt/~pmoura>
Research:  <http://logtalk.org/> Blog: <http://blog.logtalk.org/>
-----------------------------------------------------------------

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Bill McEnaney]

Is subsumes_chk(X, Y) another way to say that X subsumes Y?  If it is
another way to say that, then why not shorten the name to "subsumes?"

I wonder why some Prolog programmers name their clauses as though those
clauses were procedures in an imperative language.  They'll call a
procedure, say, "remove_duplicates" instead of "have_removed_duplicates."

Bill

> On Nov 11, 2009, at 12:52 AM, Paulo Moura wrote:
>
> >
> > Hi,
> >
> > The name subsumes_chk/2 is an ugly name for a standard predicate.
>
> Ugly it may be, but it is intention-revealing.
> subsumes : subsumes_chk :: member : memberchk
>
> These predicates were originally developed for "expert systems"
> where both versions were useful, and it was important to know
> whether one was going to bind variables (in a form of one-way
> matching) or not.  Simply replacing subsumes_chk by subsumes
> isn't ideal, especially as there is a wider reading of subsumption
> where we ask if one _clause_ (= disjunction of goals) subsumes
> another.  I suggest that something like term_subsumes/2 might
> avoid that ambiguity.
>
> For me, the big problem, indeed, a real show-stopper of a
> problem, is that we know perfectly well what subsumption
> of terms OUGHT to mean:  G1 subsumes G2 if and only if
> any possible instance of G2 is a possible instance of G1,
> and "possible" here has to mean "consistent with constraints"
> if the predicate is to be useful for the kind of thing it was
> invented for.  A purely syntactic test that ignores constraints
> seems as though it is bound to give wrong answers.
>
> If we can't get that right, it's better to leave the operation
> out.  Don't you think it would be confusing to have a
> unification that _does_ respect constraints but a subsumption
> that _doesn't_?
>
>
> _______________________________________________
> SWI-Prolog mailing list
> SWI-Prolog@...
> https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
>
>

________________________________________________________________
Please visit a saintly hero:
http://www.jakemoore.org
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

Richard O'Keefe:

>Paulo Moura:
>> The name subsumes_chk/2 is an ugly name for a standard predicate.
>
>Ugly it may be, but it is intention-revealing.
>subsumes : subsumes_chk :: member : memberchk
>
>These predicates were originally developed for "expert systems"
>where both versions were useful, and it was important to know
>whether one was going to bind variables (in a form of one-way
>matching) or not.  Simply replacing subsumes_chk by subsumes
>isn't ideal, especially as there is a wider reading of subsumption
>where we ask if one _clause_ (= disjunction of goals) subsumes
>another.

Still, I would like to see one case were (the unifying) subsumes/2 is
actually used for good!  In particular since I was quite involved in
some of those - expert systems.  And it happend to me more than once:
The sirens' songs of the beautiful declarative name subsumes/2 is so
much attracting that the ugly but reliable duck of subsumes_chk/2 has
no chance.  Wreckage guaranteed.

>          I suggest that something like term_subsumes/2 might
>avoid that ambiguity.

subsumes_chk/2 has the big advantage that it already exists in many
systems.  Yes, it is not "declarative sounding".  But as you say it is
intention-revealing.

>For me, the big problem, indeed, a real show-stopper of a
>problem, is that we know perfectly well what subsumption
>of terms OUGHT to mean:  G1 subsumes G2 if and only if
>any possible instance of G2 is a possible instance of G1,
>and "possible" here has to mean "consistent with constraints"
>if the predicate is to be useful for the kind of thing it was
>invented for.  A purely syntactic test that ignores constraints
>seems as though it is bound to give wrong answers.

>If we can't get that right, it's better to leave the operation
>out.  Don't you think it would be confusing to have a
>unification that _does_ respect constraints but a subsumption
>that _doesn't_?

(=)/2 is often not much more than a purely syntactic test.  This
happens in case consistency cannot be maintained.  So we have a
similar problem here already.  The idea is that in place of an answer
substitution we can have also a conditional answer that shows us the
remaining constraints that have to be true in order to have solutions.

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

?- Zs = [X,Y,Z], Zs ins 1..2, all_different(Zs).
Zs = [X, Y, Z],
X in 1..2,
all_different([X, Y, Z]),
Y in 1..2,
Z in 1..2.

Here we get answers that do not contain a single solution.  However,
the solver for clpfd is incapable to resolve this - it is optimized
for other cases.  Actually, clp(Q) would detect the first
inconsistence, but has similar problems with nonlinear constraints.

If you want definitive answers, you have to remove the remaining
constraints somehow.  In the first case that's currently impossible,
but in the second case it is possible.

?- Zs = [X,Y,Z], Zs ins 1..2, all_different(Zs), labeling([], Zs).
false.

Should any of this be done automatically during
semi-unification/subsumption checking?  That's so open ended!

Subsumption checking can often be reduced to syntactic checks,
provided the kinds of constraints present are restricted.  Think of
dif/2 which does not change much.  And often you are happy to detect
*some* cases of subsumption.  E.g. when trying to prove that something
does not terminate, it often is useful to "wait" another inference to
get the simpler subsumption check.  After all, we are here in
uncharted, undecidable territory.


If we would drop subsumes_chk/2 (or subsumes/2 or term_subsumes/2)
people would continue with their half backed solutions they use now:
Just look how many systems succeed for

?- subsumes_chk(X, f(X)).

or

?- subsumes_chk(g(X), g(f(X))).

Or take a numbervars term like '$VAR'(1) into an argument.  By
codifying subsumes_chk/2 we can at least improve the quality of
systems in that respect.  And we get (more) predictible behaviour
w.r.t constraints compared to what happens now.

?- dif(X,_), subsumes_chk(Y,X).
false.

Simply isn't good.

Constraints are an open ended area.  We cannot provide a solution for
everything.  But we can provide reliable elements that have to be put
together by the programmer.
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Paulo Moura]

On 2009/11/10, at 22:37, Ulrich Neumerkel wrote:

> Richard O'Keefe:
>> Paulo Moura:
>>> The name subsumes_chk/2 is an ugly name for a standard predicate.
>>
>> Ugly it may be, but it is intention-revealing.
>> subsumes : subsumes_chk :: member : memberchk
>> ...
>> These predicates were originally developed for "expert systems"
>> where both versions were useful, and it was important to know
>> whether one was going to bind variables (in a form of one-way
>> matching) or not.  Simply replacing subsumes_chk by subsumes
>> isn't ideal, especially as there is a wider reading of subsumption
>> where we ask if one _clause_ (= disjunction of goals) subsumes
>> another.
>
> Still, I would like to see one case were (the unifying) subsumes/2 is
> actually used for good!  In particular since I was quite involved in
> some of those - expert systems.  And it happend to me more than once:
> The sirens' songs of the beautiful declarative name subsumes/2 is so
> much attracting that the ugly but reliable duck of subsumes_chk/2 has
> no chance.  Wreckage guaranteed.
>
>>         I suggest that something like term_subsumes/2 might
>> avoid that ambiguity.
>
> subsumes_chk/2 has the big advantage that it already exists in many
> systems.

Usually as a library predicate, not as a built-in predicate (the Core  
Revision standardization proposal, which I wrote, cares about built-in  
predicates, not library predicates).

>  Yes, it is not "declarative sounding".  But as you say it is
> intention-revealing.


And confusion-inducing given that memberchk/2, also a library  
predicate, can further instantiate its arguments, something that  
doesn't happen with subsumes_chk/2. Or should the users spot the  
difference based on the presence (or absence) of an underscore in the  
name? :-) As someone wrote, elegance is not (or shouldn't be) optional.

Cheers,

Paulo


-----------------------------------------------------------------
Paulo Jorge Lopes de Moura, PhD
Assistant Professor
Dep. of Computer Science, University of Beira Interior
6201-001 Covilhã, Portugal

Office 3.18  Ext. 3276
Phone: [phone] Fax: [phone]
Email: <mailto:pmoura@...>

Home page: <http://www.di.ubi.pt/~pmoura>
Research:  <http://logtalk.org/> Blog: <http://blog.logtalk.org/>
-----------------------------------------------------------------

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Richard O'Keefe]

On Nov 11, 2009, at 10:37 AM, Bart Demoen wrote:
>> A purely syntactic test that ignores constraints
>> seems as though it is bound to give wrong answers.
>
> One could also go the following way: if any of the arguments of
> term_subsumes/2 contains constrained variables, throw an error.

It beats ignoring the problem.  That would do.

>
>
> Or as an alternative (using copy_term_nat and maybe applicable to
> other situations) define (in this case):
>
> term_subsumes(T1,T2) :-
>     copy_term_nat(T1,S1),
>     copy_term_nat(T2,S2),
>     subsumes_chk(S1,S2). % the old subsumes_chk
>

The problem with this is that I know what it DOES but I don't
know what it MEANS.

By the way, talk about ugly names!  What does copy_term_nat/2 have
to do with natural numbers?  It should be something like
copy_term_sans_attributes/2.

What this definition does is to ignore the attributes of T1 and T2.
But that's precisely the wrong-answer-giving approach I was afraid
of.  Given copy_term_nat/2 and a version of term_subsumes/2 that
throws an error when it hits an attributed variable (except, I hope,
in the case X ? X; one would hope term_subsumes(T, T) for any T),
anyone who _wants_ a subsumption test that ignores variables can
program it, and maybe making them do so will make them think about
what they're doing.  But I really don't think it's a good idea for
ignoring attributes ever to be a default choice.


_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

Paulo Moura:
>> subsumes_chk/2 has the big advantage that it already exists in many
>> systems.
>
>Usually as a library predicate, not as a built-in predicate (the Core
>Revision standardization proposal, which I wrote, cares about built-in
>predicates, not library predicates).

It does not make much of a difference for such common predicates
whether it is built-in or in a library.  These predicates will be
present in most programs - no matter how.  After all, weren't
length/2, member/2 and append/3 relegated into libraries recently?

What does matter is a precise and useful definition.

Consider length/2: It would be a waste of effort to dismiss your
definition altogether.  It is quite good and would improve systems -
no matter where length/2 is located.

>>  Yes, it is not "declarative sounding".  But as you say it is
>> intention-revealing.
>And confusion-inducing given that memberchk/2, also a library
>predicate, can further instantiate its arguments, something that
>doesn't happen with subsumes_chk/2. Or should the users spot the
>difference based on the presence (or absence) of an underscore in the
>name? :-) As someone wrote, elegance is not (or shouldn't be) optional.

I thought the chk/2 suffix is something of a -p.  Not entirely.  I
never use memberchk/2.  I thought it does == comparison.  In fact, now
I remember someone complaining about constraints not awoken in
memberchk/2, that cannot work ...
_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Richard O'Keefe]

On Nov 11, 2009, at 10:40 AM, Paulo Moura wrote:

> But both member/2 and memberchk/2 perform instantiations,  
> subsumes_chk/2 doesn't. I see a subsumes/2 predicate that (only)  
> checks for subsumption in the same class as ground/1, integer/1, etc.

You're right.  I can't have been getting enough sleep to be so stupid.

>> another.  I suggest that something like term_subsumes/2 might
>> avoid that ambiguity.
>
> Which would also avoid trouble with backward portability.

Agreement?  Lovely.  It also establishes a link with things like
copy_term/2.
>
> I agree that constraints are an important extension to Prolog but I  
> would really like to see a constraints standardization proposal  
> before discussing what we should do or not do in a Prolog standard.

(A) Constraints have been around for a while.  We know enough about
     how they're likely to work to be aware that there is an _issue_.
     (Come to think of it, constraint programming in a more or less
     logical form, is older than Prolog.  AbSys/AbSet.)
(B) The only occurrence of "standard" in my message in the phrase
     "standard predicate" quoted from one Paulo Moura.  What I wrote had
     nothing to do with the Prolog standard or any other standard.  The
     message subject has [SWIPL] in the subject line, the thread is
     discussing what should be done about subsumption tests in SWI  
Prolog,
     and SWI Prolog already has attributed variables and CHR.  Whatever
     is done about subsumption in SWI PRolog should do something  
sensible
     with cyclic terms, attributed variables, and CHR.

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

[Ulrich Neumerkel]

>On Nov 11, 2009, at 10:37 AM, Bart Demoen wrote:
>>> A purely syntactic test that ignores constraints
>>> seems as though it is bound to give wrong answers.
>>
>> One could also go the following way: if any of the arguments of
>> term_subsumes/2 contains constrained variables, throw an error.
>
>It beats ignoring the problem.  That would do.

Why not: Error, if the constrained variables are of *relevance*?
Could that be defined more precisely?  Otherwise, we have minimal
runtime proportional to the sum of both terms.

I.e.  term_subsumes(X,X)  always succeeds no matter what X is.

>> Or as an alternative (using copy_term_nat and maybe applicable to
>> other situations) define (in this case):
>>
>> term_subsumes(T1,T2) :-
>>     copy_term_nat(T1,S1),
>>     copy_term_nat(T2,S2),
>>     subsumes_chk(S1,S2). % the old subsumes_chk

This definition is no longer subsumes_chk/2 or semi-unification for
syntactic terms.  Consider ?- term_subsumes(X, f(X)).

While subsumes_chk(X, f(X)) fails, this would succeed.

It should be

term_subsumes(T1,T2) :-
                     copy_term_nat(T1+T2,S1+S2),
                     subsumes_chk(S1,S2). % the old subsumes_chk

That would be nice - except that so far there has been some resistance
against too many errors in built-ins.  But well.

>By the way, talk about ugly names!  What does copy_term_nat/2 have
>to do with natural numbers?  It should be something like
>copy_term_sans_attributes/2.

I am often tempted to desire copy_term/2 meaning copying without.
Now, that errors are out, why not produce errors for copy_term/2?
copy_term/3 is for the more complex things.

_______________________________________________
SWI-Prolog mailing list
SWI-Prolog@...
https://mailbox.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog