Freeze/findall Interaction

Appeared in Volume 10/2, May 1997

ken@als.com
Ken Bowen
23rd January 1997

Does anyone know of any posted discussion on the interaction between freeze and all solution predicates? For example, if findall freezes a variable during (attempted) execution of one of its solution goals, should/should-not that freeze be destroyed (i.e., completely deleted) upon backtracking?

ridoux@merab.irisa.fr
Olivier Ridoux
24th January 1997

I don't know of any posted discussion on this subject, but I have an opinion.

As an implementor, I have several times implemented all solution predicates and freeze in the usual way: they are considered as separate problems, and implemented almost separately, with just enough care so that they don't kill each other.

My implementation strategy would now be different. I think all delayed (frozen, postponed, etc.) stuff that comes from an all solution computation should be reified as a goal formula and attached in some way to the corresponding solution.

The easy way is to construct a pair <solution,proviso> in which proviso is the summary of the delayed stuff. In LambdaProlog, the proviso should be represented as a function of the solution. I call it a proviso because the reading of such a pair is "solution satisfies the goal unless proviso is false".

If you think about it, the usual way of delaying by attaching delayed stuff to the variable that can trigger its reactivation does not work well. It is not structured enough, and does not allow you to tell what belongs to which subcomputation. Don't forget that all solution predicates can be nested!

In some sense, this resembles the problem of implementing negation as failure by executing negated goal until a binding of a global variable occurs, in which case the computation of the negated goal is frozen. This seems easy until you realise that negations can be nested.

I believe that an implementation of this kind of stuff should seriously consider the idea that sub-computations (negated goals or all solution predicates) are executed by their own copy of the interpreter.

In this framework, freezing and resuming computation becomes a matter of scheduling processes. This may cause a slight shift in the semantics of freeze because you are moving from an interruption-oriented semantics to a kind of monitor-oriented semantics.

The relationship with negation makes me think that there may be also a link with tabulation "á la XSB".