Previous Up Next

18.2  Waiting for Binding

Sometimes we want a goal to be woken when a variable is bound to another one, e.g., to check for subsumption or disequality. As an example, let us construct the code for the built-in predicate ∼=/2. This predicate imposes the disequality constraint on its two arguments. It works as follows:

  1. It scans the two terms. If they are identical, it fails.
  2. If it finds a pair of different arguments at least one of which is a variable, it suspends. If both arguments are variables, the suspension is placed on the bound suspended list of both variables. If only one is a variable, the suspension is placed on its inst list, because in this case the constraint may be falsified only if the variable is instantiated.
  3. Otherwise, if it finds a pair of arguments that cannot be unified, it succeeds.
  4. Otherwise it means that the two terms are equal and it fails.

The code looks as follows. equal_args/3 scans the two arguments. If it finds a pair of unifiable terms, it returns them in its third argument. Otherwise, it calls equal_terms/3 which decomposes the two terms and scans recursively all their arguments.

dif(T1, T2) :-
    (equal_args(T1, T2, Vars) ->
        (nonvar(Vars) ->
            (Vars = inst(V) ->
                suspend(dif(T1, T2), 3, V->inst)
            ;
                suspend(dif(T1, T2), 3, Vars->bound)
            )
        ;
            fail     % nothing to suspend on, they are identical
        )
    ;
        true         % the terms are different
    ).

equal_args(A1, A2, Vars) :-
    (A1 == A2 ->
        true
    ;
    var(A1) ->
        (var(A2) ->
            Vars = bound(A1, A2)
        ;
            Vars = inst(A1)
        )
    ;
    var(A2) ->
        Vars = inst(A2)
    ;
        equal_terms(A1, A2, Vars)
    ).

equal_terms(R1, R2, Vars) :-
    R1 =.. [F|Args1],
    R2 =.. [F|Args2],
    equal_lists(Args1, Args2, Vars).

equal_lists([], [], _).
equal_lists([X1|A1], [X2|A2], Vars) :-
    equal_args(X1, X2, Vars),
    (nonvar(Vars) ->
        true     % we have already found a variable
    ;
        equal_lists(A1, A2, Vars)
    ).

Note that equal_args/3 can yield three possible outcomes: success, failure and delay. Therefore, if it succeeds, we have to make the distinction between a genuine success and delay, which is done using its third argument. The predicate dif/2 behaves exactly as the built-in predicate ∼=/2:

[eclipse 26]: dif(X, Y).

X = X
Y = Y

Delayed goals:
        dif(X, Y)
yes.
[eclipse 27]: dif(X, Y), X=Y.

no (more) solution.
[eclipse 28]: dif(X, Y), X=f(A, B), Y=f(a, C), B=C, A=a.

no (more) solution.
[eclipse 29]: dif(X, Y), X=a, Y=b.

X = a
Y = b
yes.

Note also that the scan stops at the first variable being compared to a different term. In this way, we scan only the part of the terms which is absolutely necessary to detect failure – the two terms can become equal only if this variable is bound to a matching term.

This approach has one disadvantage, though. We always wake the dif/2 call with the original terms as arguments. Each time the suspension is woken, we scan the two terms from the beginning and thus repeat the same operations. If, for instance, the compared terms are lists with thousands of elements and the first 10000 elements are ground, we spend most of our time checking them again and again.

The reason for this handling is that the system cannot suspend the execution of dif/2 while executing its subgoals: it cannot freeze the state of all the active subgoals and their arguments. There is however a possibility for us to do this explicitly: as soon as we find a variable, we stop scanning the terms and return a list of continuations for all ancestor compound arguments. In this way, equal_args returns a list of pairs and their continuations which will then be processed step by step:

dif2(T1, T2) :-
    equal_args(T1, T2, List, Link),
    !,
    diff_pairs(List, Link).
d2if(_, _).                % succeed if already different

equal_args(A1, A2, L, L) :-
    A1 == A2,  !.
equal_args(A1, A2, [A1-A2|Link], Link) :-
    (var(A1);var(A2)),
    !.
equal_args(A1, A2, List, Link) :-
    equal_terms(A1, A2, List, Link).

equal_terms(T1, T2, List, Link) :-
    T1 = [_|_],
    T2 = [_|_],
    !,
    equal_lists(T1, T2, List, Link).
equal_terms(T1, T2, List, Link) :-
    T1 =.. [F|Args1],
    T2 =.. [F|Args2],
    equal_lists(Args1, Args2, List, Link).

equal_lists([], [], L, L).
equal_lists([X1|A1], [X2|A2], List, Link) :-
    equal_args(X1, X2, List, L1),
    (nonvar(List) ->
        L1 = [A1-A2|Link]
    ;
        equal_lists(A1, A2, L1, Link)
    ).

diff_pairs([A1-A2|List], Link) :-
    -?->
    (A1 == A2 ->
        diff_pairs(List, Link)
    ;
    (var(A1); var(A2)) ->
        suspend(diff_pairs([A1-A2|List], Link), 3, A1-A2->bound)
    ;
    equal_terms(A1, A2, NewList, NewLink) ->
        NewLink = List,             % prepend to the list
        diff_pairs(NewList, Link)
    ;
        true
    ).

Now we can see that compound terms are processed up to the first potentially matching pair and then the continuations are stored:

[eclipse 30]: dif2(f(g(X, Y), h(Z, 1)), f(g(A, B), h(2, C))).

X = X
...
Delayed goals:
        diff_pairs([X - A, [Y] - [B], [h(Z, 1)] - [h(2, C)]|Link], Link)
yes.

When a variable in the first pair is bound, the search proceeds to the next pair:

[eclipse 31]: dif2(f(g(X, Y), h(Z, 1)), f(g(A, B), h(2, C))), X=A.

Y = Y
...
Delayed goals:
        diff_pairs([Y - B, [] - [], [h(Z, 1)] - [h(2, C)]|Link], Link)
yes.

dif2/2 does not do any unnecessary processing, so it is asymptotically much better than the built-in ∼=/2.

This predicate, however, can be used only to impose a constraint on the two terms (i.e., it is a “tell” constraint only). It uses the approach of “eager failure” and “lazy success”. Since it does not process the terms completely, it sometimes does not detect success:

[eclipse 55]: dif2(f(X, a), f(b, b)).

X = X

Delayed goals:
        diff_pairs([X - b, [a] - [b]|Link], Link)
yes.

If we wanted to write a predicate that suspends if and only if the disequality cannot be decided, we have to use a different approach. The easiest way would be to process both terms completely each time the predicate is woken. There are, however, better methods. We can process the terms once when the predicate dif/2 is called, filter out all possibly matching pairs and then create a suspension for each of them. As soon as one of the suspensions is woken and it finds an incompatible binding, the dif/2 predicate can succeed. There are two problems:

dif3(T1, T2, Yes, No) :-
    compare_args(T1, T2, no, No, Yes).

compare_args(_, _, _, _, Yes) :-
    nonvar(Yes).
compare_args(A1, A2, Link, NewLink, Yes) :-
    var(Yes),
    (A1 == A2 ->
        Link = NewLink            % short-cut the links
    ;
    (var(A1);var(A2)) ->
        suspend(compare_args(A1, A2, Link, NewLink, Yes), 3,
     [[A1|A2]->bound, Yes->inst])
    ;
        compare_terms(A1, A2, Link, NewLink, Yes)
    ).

compare_terms(T1, T2, Link, NewLink, Yes) :-
    T1 =.. [F1|Args1],
    T2 =.. [F2|Args2],
    (F1 = F2 ->
        compare_lists(Args1, Args2, Link, NewLink, Yes)
    ;
        Yes = yes
    ).

compare_lists([], [], L, L, _).
compare_lists([X1|A1], [X2|A2], Link, NewLink, Yes) :-
    compare_args(X1, X2, Link, L1, Yes),
    compare_lists(A1, A2, L1, NewLink, Yes).

The variable Yes is instantiated as soon as the constraint becomes true. This will also wake all pending suspensions which then simply succeed. The argument No of dif3/4 becomes instantiated to no as soon as all suspensions are woken and their matched pairs become identical:

[eclipse 12]: dif3(f(A, B), f(X, Y), Y, N).

Y = Y
...

Delayed goals:
        compare_args(A, X, no, L1, Y)
        compare_args(B, Y, L1, N, Y)
yes.
[eclipse 13]: dif3(f(A, B), f(X, Z), Y, N), A = a, X = b.

Y = yes
N = N
...
yes.
[eclipse 14]: dif3(f(A, B), f(X, Z), Y, N), A=X, B=Z.

Y = Y
N = no
...
yes.

Now we have a constraint predicate that can be used both to impose disequality on two terms and to query it. For instance, a condition “if T1 = T2 then X = single else X = double” can be expressed as

cond(T1, T2, X) :-
    dif3(T1, T2, Yes, No),
    cond_eval(X, Yes, No).

cond_eval(X, yes, _) :- -?->
    X = double.
cond_eval(X, _, no) :- -?->
    X = single.
cond_eval(X, Yes, No) :-
    var(Yes),
    var(No),
    suspend(cond_eval(X, Yes, No), 2, Yes-No->inst).

This example could be further extended, e.g., to take care of shared variables, occur check or propagating from the answer variable (e.g., imposing equality on all matched argument pairs when the variable Y is instantiated). We leave this as a (rather advanced) exercise to the reader.


Previous Up Next