Is there a whened/2 predicate?

General
1

I find that SWI-Prolog has a frozen/2 predicate. It allows to query freezed variables:

?- freeze(X,X=1), frozen(X,R).
R = freeze(X, user:(X=1))

Is there some analogue for when/2. frozen/2 doesn’t show anything:

?- when((nonvar(Y);nonvar(Z)), let(X, Y+Z)), frozen(X,R).
R = true
2

when/2 and friends use attributes, so term_attvars/2, attr_portray_hook/2, attribute_goals//1, or similar might do what you want.

4

Because the delays are on Y and Z, not on X …

102 ?- when((nonvar(Y);nonvar(Z)), let(X, Y+Z)), frozen(Y,R).
Correct to: "get(X,Y+Z)"? yes
R = when((nonvar(Y);nonvar(Z)), user:get(X, Y+Z)).
6

But this does indeed require a recent version. Older versions (including 8.2.x) indeed only report delays from freeze/2.

9

frozen/2 is built on top of the same hooks as copy_term/3. Thus, if it doesn’t do the right thing for when/2 or whatever constraint, the implementation of that constraint is to be blamed. This hook (Module:attribute_goals//1) is responsible for translating the attributes back to a goal that re-instantiates the attributes. This indeed isn’t always the most elegant goal. It is only buggy if the implications of the re-instantiated attributes differ from the original attributes. More elegant is better though :slight_smile:

11

See attribute_goals//1

13

I guess it depends on your reading. when(ground(f(X,Y), true) delays only on one of the two variables and will put a delay on the next variable of the pool if the variable on which the current delay is set is instantiated. So, frozen/2 is correct in reporting that one of the variables has no delay.

Whether this behavior is desirable is another issue. It is surely not the fault of frozen/2 though. There is simply no way it can know better. It is a design decision of when/2 not to put attributes on all involved variables. Note that you can use frozen(f(X,Y), Goal) to always get the intended result.

15

This is a known problem of attributed variables based constraints as the docs of
call_residue_vars/2 tell you. I’m not aware of any solutions for this. call_residue_vars/2 is merely for debugging as it avoids garbage collecting attributed variables and thus may run out of memory in otherwise perfectly fine code. It is also scales poorly in most systems, although I managed to find a fairly efficient way to handle this with the help of Bart Demoen.

17

Not very good. Now there is no promise that the reported constraints are minimal or pretty. I had a brief look at the source. Seems this should be fixed by one of the hooks unifying the other variables to avoid double results. Must be a nice puzzle for anyone who considers this important enough or fancying a puzzle :slight_smile: For those interested, the hook code is with when/2. The hooks are called from the code around copy_term/3. There you also find a brief comment on duplicate results.

19

I simplified this to the program below, which does not terminate. If we use normal unification rather then unify_with_occurs_check/2 this also doesn’t terminate in SICStus. I guess this depends on how unify_with_occurs_check/2 is implemented. At this moment this does

  1. Normal unification
  2. Examine the trail to find the bindings created and see whether one of these bindings is a cycle (the bound variable appears in the term it is bound to).

Normal unification involves triggering the constraints. We could do the cycle detection before evaluating the pending constraints. This would make sense if this is a sufficient check. I’m a little in doubt. Can constraint evaluation create cycles? I think so as, in the current implementation, the above cycle detection does not go into attributed variables. Seems this is correct as also SICStus agrees this succeeds:

?- freeze(X, write(Y)), unify_with_occurs_check(X,Y).

Correct is of course a bit ambiguous as ISO says nothing about constraints.

t :-
    Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],

    expr(_3434),
    expr(_3514),
    expr(_3206),

    P=[_3434|_3514],

    expr(_3434),
    expr(_3514),

%   Q = P,
    unify_with_occurs_check(Q, P),

    true.

expr(X) :- freeze(X, expr2(X)).

% expr(+Term)
expr2([X|Y]) :-
   expr(X),
   expr(Y).
expr2(quote).
expr2([]).
expr2(cons).
expr2(lambda).
expr2(symbol(_)).
22

Reported in simplified form in https://github.com/SWI-Prolog/swipl-devel/issues/758. Fixed. Thanks.

Also fixes quine:

101 ?- time((dif(Q, []), quine(Q, 6, N))).
% 209,677,737 inferences, 7.698 CPU in 7.700 seconds (100% CPU, 27236214 Lips)
Q = [[lambda, symbol(_59492), [cons, symbol(_59492), [cons, [...|...]|...]]], [quote, [lambda, symbol(_59492), [cons, symbol(...)|...]]]],
N = 5 .