Freeze interferes with multiple solutions

Help!
1

Using freeze/2

test_cut(X) :-
    freeze(L, (X = 1 ; X = 2)),
    test_cut_list(L).

Then, these variations both have the same issue…

test_cut_list([]) :- !.

and

test_cut_list(L) :- 
    (L = [] -> true).

… both chop off the 2nd alternative, producing only:

?- test_cut(X).
X = 1.

… whereas either of these 2 predicates…

test_cut_list([]).

and

test_cut_list(L) :- 
    (L = [] *-> true).

… produce the 2 expected solutions:

?- test_cut(X).
X = 1 ;
X = 2.

Isn’t this a bug in freeze/2? The logic flow in test_cut_list seems to be strangely affecting the X = 2 freeze path.

2

No (provided I do not read this wrong). Considering test_cut_list([]) :- !.,
the head unification triggers the wakeup that is executed by inserting the wakeup goal at the “neck”. So, it first executes the frozen goal and then cuts. Other Prologs may do this differently.

Bottom line is that mixing cuts with coroutining (and constraints) is asking for trouble unless you know really well what is going on.

3

That’s a huge gotcha… and a huge disappointment.

Can’t the freeze/2 code be independent?

4

You’ve already given an example of how to avoid being disappointed: using *-> instead of -> or cut.

(I agree with @jan – this is not a bug; and mixing cut with coroutining is likely to end badly.)

5

I’m not seeing “likely to end badly” as a sensible language design goal.

How is this a desirable situation? Surely the freeze/2 goals being independent would be far better?

6

I wish there were a way of banishing “cut” from Prolog. It’s full of pitfalls for the unwary. Richard O’Keefe has written extensively on the issues of the scope of “cut” (for example, what should call(!) do?).

I suppose part of the problem is in the mechanism that freeze/2 uses, namely attributed variables. It’s a quite elegant mis-use of something that was originally intended to provide “narrowing” semantics for unification – for example, allowing a variable to constrained to a set of possible values, with unification succeeding by reducing the possible values (failure if it’s the empty set; regular unification if the result is a single value). The “hook” for attributed variables allows running an arbitrary predicate when the variable is instantiated. (And I wonder what it means to use freeze/2 on the “domain” attributed variable example in the manual.) (Also, there are some subtle problems with how the attributed variable “hook” is invoked, which apparently Sicstus Prolog solves (or is it ECLiPSe?) – would the Sicstus implementation solve the freeze/cut issue, I wonder? … see Markus Trika’s Attributed Variables in Prolog , which I’ve now added to my stack of things to read)

On the other hand, @jan has mentioned (somewhere) that freeze/2 is slower than he would like, so perhaps there’s an opportunity to change the implementation of freeze/2 (and when/2) to use something other than attributed variables.

1 Like
7

I suppose we should use *->/2 as the default, instead of ->/2, given the difference I highlighted above, despite it not being needed in the non-freeze context.

Erm… note to self: write better (more deterministic) code :joy:

8

One thing I’ve learned – sprinkling my code with cuts, in the hopes of removing some bugs or performance issues, does not usually improve it. :rofl:

1 Like
9

This is one of the areas ISO solved and where it did (IMO) a good job. Scoping of the cuts is well defined … for ISO Prolog. Attributed variables are not part of ISO. It is clear that unifying to them inserts a goal into the SLD resolution tree. It is not clear when exactly this happens. It is also clear that cuts can prune the alternatives of goals inserted by attributed variable wakeup, but exactly when is also undefined. I’ve implemented attributed variables with help from Bart Demoen and Tom Schrijvers and recall Bart already pointed at the lack of common practice on when exactly to do the wakeup. If now happens

  • After head unification, inserting the wakeup as first goal of the body (creating a body if the clause is a fact).
  • After success from calling a foreign predicate, inserting the wakeup right after the foreign goal
  • After inlined unification, inserting the wakeup right after the unification.

A cut further down in the body thus cuts the choices left by the wakeup.

SICStus does the wakeup differently. SWI-Prolog makes a single call after the unification that provides the attributes (from before the unification) and the term (can be another attvar) to which the variable is unified and does all of that in the state the system is in at the wakeup. SWI-Prolog unification with attvars is normal unification, where attvars are handled as normal variables, but unifying them schedules the wakeup call. SICStus has two calls, one before and one after unification and does these calls one unification after the other. So, effectively it does not execute the attvar unifications, but just schedules them. That makes some operations simpler and Markus claims it is necessary for implementing some solvers correctly. He never came with a convincing case though, although I won’t deny that in some scenarios SWI-Prolog’s approach is more complicated to program. Other systems typically implement something that share properties from the SICStus approach and the “Leuven” approach.

In general, you may combine coroutining and multiple constraints in a single computation. That is, if the subsystems nicely follow all (undocumented) guidelines. Unless the solvers know about each other, you cannot expect anything clever to happen.

I think implementing freeze/2 using attributed variables is fine. The entire attributes variable handling should be implemented with better performance. I don’t know how though. I also never did any detailed analysis on where the time is spent. The rough idea is simple: a unification adds a term to a global variable (implemented as a term reference at a well known location) using backtrackable assignments. At a wakeup moment, the system checks this global variable is nonvar and injects a call to $wakeup/1, passing the value of this global variable (after resetting the variable itself to var).

1 Like
10

Maybe just my perspective but I have to disagree. Prolog is a nondeterministic langauage - it’s based on logic and “or” is an “any of” choice, not a “one of”. Cuts provide an efficient way of turning an uncommitted choice to a committed one, i.e. pruning the search tree. There are committed choice languages around (Erlang is one IIRC) if that’s your preference.

I think the main issue with the ISO cut is that it’s context sensitive; that’s why call(!) is semantically different than !. But that’s not something you normally want to do unless you’re looking at meta-interpretation. Pre-ISO days, I used a Prolog that had ancestor cuts which were not context sensitive, so call(cut(some_pred_name) did work as you would expect. But I can’t say as I really miss that feature very much. (There was also a clause level (local) cut, but that can be easily done using “if-then”.)

Co-routines/constraints raise the possibility that any unification can turn into the insertion/execution of arbitrary code. I agree that mixing that with cuts is a potential disaster which can best be avoided by ensuring that “frozen” goals (including any attr_unify_hook’s) are deterministic. It also makes the code much easier to understand IMO (no backtracking into un-frozen goals totally disconnected with the predicate being executed.) Now maybe that’s something that could be enforced by the system, i.e., attr_unify_hook is always called with a once wrapper, somewhat like the “if-then” condition.

Now not “sprinkling my code with cuts” is good advice. But banning cuts isn’t the answer (besides being impractical at this point in history). Cuts are easy to misuse (takes just two characters) so use them only when the reason they’re necessary is understood and they have the desired (and only the desired) effect. That’s not always easy but it’s better to do it while writing the code rather than later in the game.

11

Cuts to force determinism are OK – although I wish the compiler was smart enough to figure that out.
If-then-else (especially the *-> kind) is also OK, if it’s a shorthand for listing out all the possibilities (e.g., the Picat-style of matching).

But I’m having trouble with the following, which doesn’t seem to have a straightforward transformation to if-than-else that doesn’t also leave a choicepoint (code by @j4n_bur53).

runs([X-N|R]) --> [X], {var(N)}, !, run(X, M), {N is M+1}, runs(R).
runs([X-N|R]) --> [X], {N > 0}, !, {M is N-1}, run(X, M), runs(R).
runs([]) --> [].

run(X, N) --> [X], {var(N)}, !, run(X, M), {N is M+1}.
run(X, N) --> [X], {N > 0}, !, {M is N-1}, run(X, M).

There’s a more elegant solution using freeze/2 and when/2, but it leaves choicepoints: Logically pure/impure predicate implementations in the std lib - #16 by peter.ludemann

12

That is not enough. It is typically hard to predict when a wakeup happens and thus whether it is before or after the cut. So, a cut may be reached because some constraint (or frozen goal, there is not much difference) that will fail has not yet been triggered. Had the constraint been triggered, then the cut would not have been reached. If you know exactly what you are doing you can deal with that. It remains a little shaky though :frowning: Especially when it comes to portability as the moment when the wakeup happens vary and constraint solvers differ in their propagation strategy and thus may or may not have resolved some constraint at some point in the computation.

1 Like
13

For this example, really? If the constraint was fired in head unification, can the attr_unify_hook be executed after the ‘!’ in the body? Is ‘!’ different than any other goal in this situation?

14

Here’s a (hopefully clearer) example of freeze/2 (and when/2) making ->/2 unsafe:

freeze_test(A, B) :-
    (   A = 2
    ->  B = two
    ;   A = 1
    ->  B = one
    ).

freeze_test2(A, B) :-
    (   A = 2,
        B = two
    ;   A = 1,
        B = one
    ).

Results:

?- freeze(A, member(A, [1, 2])), freeze_test(A, B).
A = 2,
B = two.

?- when(ground(A), member(A, [1, 2])), freeze_test(A, B).
A = 2,
B = two.

vs

?- member(A, [1, 2]), freeze_test(A, B).
A = 1,
B = one ;
A = 2,
B = two.

?- freeze(A, member(A, [1, 2])), freeze_test2(A, B).
A = 2,
B = two ;
A = 1,
B = one ;
false.

I am wondering whether this can be made nicer than a huge gotcha for the unwary - perhaps adding a runtime warning if the frozen/2 Goal succeeds more than once?

A fragile workaround, purely for example:

freeze_test3(A, B) :-
    (frozen(A, freeze(A, Goal)) -> Goal ; true),
    (   A = 2
    ->  B = two
    ;   A = 1
    ->  B = one
    ).

Results:

?- freeze(A, member(A, [1, 2])), freeze_test3(A, B).
A = 1,
B = one ;
A = 2,
B = two.