Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Guidelines for implementing predicates like dif/2

Suppose I have a predicate foo/2 which defines a relation between its first and second argument.

What is the most idiomatic and efficient way to change the implementation of foo/2 such that:

  • if both of its arguments are ground, it acts as before (succeeds if the relation holds, fails otherwise).

  • if one of the two arguments (or both) are free, it "constrains" those two arguments so that when they will get grounded, the relation will be checked.

In other words, how to correctly implement the behaviour exhibited by dif/2 but with any kind of user-defined relation?

listing(dif/2). was of little help.

like image 230
Fatalize Avatar asked Feb 18 '17 18:02

Fatalize


People also ask

What is a dif 2?

dif( @A, @B ) The dif/2 predicate is a constraint that is true if and only if A and B are different terms. If A and B can never unify, dif/2 succeeds deterministically. If A and B are identical, it fails immediately. Finally, if A and B can unify, goals are delayed that prevent A and B to become equal.

How do you check if an element is a list Prolog?

To check if a variable is bound to a list, you can use is_list/1 .


2 Answers

Different Prolog implementations provide different features to accomplish this. The mechanism is variously known as coroutining, delayed goals, constraints, and your Prolog system's manual will provide more information.

Here are two variants, which are available in SICStus Prolog and also some other systems.

block/1 directive

In SICStus Prolog (and possibly some other systems), one way to lift a user-defined predicate to such a constrained version is available via the declarative block declaration.

Interestingly, this does not require any changes to the predicate itself!

Suppose you have an impure version of dif/2, using the non-monotonic (\=)/2 predicate:

madif(X, Y) :-
    X \= Y.

Then you can turn it into a delayed version for example with:

:- block madif(-, ?),
         madif(?, -).

madif(X, Y) :-
    X \= Y.

Sample queries and answers:

| ?- madif(a, b).
yes
| ?- madif(a, X).
user:madif(a,X) ? ;
no
| ?- madif(a, X), X = b.
X = b ? ;
no
| ?- madif(X, Y).
user:madif(X,Y) ? ;
no

As required, the evaluation of the goal is delayed until both arguments are instantiated.

when/2

A second way to accomplish this with SICStus Prolog (and other systems that provide this feature) is to use when/2. This requires changes to the predicate itself.

For example, using when/2, you can implement madif/2 like this:

madif(X, Y) :-
    when((ground(X),
          ground(Y)), X \= Y).

Sample queries and answers:

| ?- madif(X, a).
prolog:trig_ground(X,[],[X],_A,_A),
prolog:when(_A,(ground(X),ground(a)),user:(X\=a)) ? ;
no
| ?- madif(X, a), X = b.
X = b ? ;
no
like image 68
mat Avatar answered Sep 28 '22 07:09

mat


First and foremostly,

Take the user's viewpoint

... and not that of an implementer. All too often this is ignored – also in existing constraint implementations. And it shows. So here are the most salient aspects to take into account.

Correctness

Obviously this should hold. It is always better to produce clean errors, mostly instantiation errors, better to flounder forever, even better to loop forever than to fail incorrectly. If all else breaks you can wrap your attempt with freeze(_, G_0). Note that you do need a working toplevel to actually see such floundering goals. SICStus has such a toplevel1, in SWI you need to wrap your query as call_residue_vars(Query_0, Vs) to see all attached constraints.

Consistency

Next you want to ensure that your constraint ensures consistency as much as possible. There are many notions of consistency like, domain and bounds consistency. To take your precise requirement think of difgrn/2 and compare it to the built-in dif/2:

difgrn(X, Y) :-
   when((ground(X), ground(Y)), X \== Y).

| ?- difgrn(X, X).
prolog:trig_ground(X,[],[X],_A,_B),
prolog:trig_ground(X,[],[X],_A,_C),
prolog:trig_and(_C,[],_A,_B,_A),
prolog:when(_A,(ground(X),ground(X)),user:(X\==X)) ? ;
no
| ?- dif(X, X).
no


| ?- difgrn([], [_]).
prolog:trig_ground(_A,[],[_A],_B,_C),
prolog:trig_and(_C,[],_B,1,_B),
prolog:when(_B,(ground([]),ground([_A])),user:([]\==[_A]))

| ?- dif([], [_]).
yes

One way to implement dif/2 in full strength is to use the very special condition (?=)/2:

difwh(X,Y) :- when(?=(X,Y), X\==Y).

which should answer your question as best as one can:

In other words, how to correctly implement the behaviour exhibited by dif/2 but with any kind of user-defined relation?

But unfortunately, this does not extend to anything else.

The situation becomes even more complex if one considers consistency between various constraints. Think of X in 1..2, dif(X, 1), dif(X, 2).

Answer projections

(For lack of a better word.) Sometimes you want to see your constraints nicely on the toplevel - and the best way is to represent them as goals that themselves will reestablish the exact state required to represent an answer. See above trig_ground answers, which certainly could be beautified a bit.

Variable projections

Same as answer projections but possible at any point in time, via frozen/2 or copy_term/3.

Subsumption checking

This is useful for diagnostic purposes and loop checks. For purely syntactic terms, there is subsumes_term/2 which ignores constraints. A prerequisite to perform an effective test is to connect each involved variable to the actual constraint. Consider the goal freeze(X, Y = a) and imagine some subsumption checking with Y as an argument. If Y is no longer attached to the information (as it usually is with current implementations of freeze/2) you will come to the wrong conclusion that this Y subsumes b.

Note as for the actual example of dif/2, this was the very first constraint ever (1972, Prolog 0). A more elaborate description gives Michel van Caneghem in L'anatomie de Prolog, InterÉditions 1986 and Lee Naish in Papers about MU-Prolog.


1 Half-true. For library(clpfd) you need assert(clpfd:full_answer).

like image 31
false Avatar answered Sep 28 '22 06:09

false