Prolog delayed evaluation: LIFO or FIFO wake-up?

Question

Many Prolog systems have a freeze/2 predicate, a predicate that should possibly have the name geler/2 since it was even invented before Prolog-II.

Assume I have a condition on the same variable, but two different goals, i.e.:

 ?- freeze(X, G1), freeze(X, G2), X=1.

What is the preferred wake-up strategy, is G1 first executed or is G2 first executed? What if G1 and G2 do spawn new freezes, which are also woken up:

 G1 :- freeze(Y, G3), Y=1.
 G2 :- freeze(Z, G4), Z=1. 

Is G3 or G4 always executed in-between G1 and G2, or could it be that G3 or G4 is executed after G1 and G2, or even any time later?

Bye

Answer 1

It depends a little bit how freeze/2 is implemented under the hood. The two main types of attribute variable interfaces that can come into play are type 1 and type 2 with respect to wake-up. Namely:

Type 1: Post-Unify
The wake-up would happen after X is instantiated and the current goal succeeded, before the next goal is called. With this type the frozen goal would see any instantiations but the execution is not immediate and not always.

Type 2: Pre-Unify
The wake-up would happen before X is instantiated during unification. A pre-unify doesn't make any sense for freeze/2, since then the frozen goal wouldn't see any instantiation.

In the above example the goal that succeeds is X=1, and the next goal is the pseudo goal of the end of the query. The woken-up goals, read off from the attribute value of the variable, are pushed on a list so that they are available for this next goal.

Lets see whether this list is a FIFO:

SWI-Prolog:

?- freeze(X, write('ha ')), freeze(X, write('tschi ')), X=1, nl.
ha tschi 
X = 1.

?- freeze(X, write('ha ')), freeze(X, write('tschi ')), (X=1; X=2), nl.
ha tschi 
X = 1 ;
ha tschi 
X = 2.

Jekejeke Prolog with Minlog Extension:

?- use_module(library(term/suspend)).
% 5 consults and 0 unloads in 90 ms.
Yes

?- freeze(X, write('ha ')), freeze(X, write('tschi ')), X=1, nl.
ha tschi 
X = 1

?- freeze(X, write('ha ')), freeze(X, write('tschi ')), (X=1; X=2), nl.
ha tschi 
X = 1 ;
ha tschi 
X = 2

So the list is a FIFO. So freezing and immediately waking up, gives left to right execution in the above two Prolog systems. From this one can also deduce what would happen if the goals do further freezing and immediate wake up by themselves.