Do they exist? How are they implemented?
The coroutining predicates of SWI-Prolog (freeze
, when
, dif
etc.) have the functionality of guards. How do they fit in the preferred Prolog programming style?
I am very new to logic programming (with Prolog and altogether) and somewhat confused by the fact that it is not purely declarative, and requires procedural considerations even in very simple cases (see this question about using \==
or dif
). Am I missing something important?
First a terminological issue: Neither
freeze/2
norwhen/2
nordif/2
are called guards under any circumstance. Guards appear in such extensions as CHR, or related languages as GHC (link in Japanese) or other Concurrent logic programming languages ; you even (under certain restrictions) might consider clauses of the formas clauses containing a guard and the cut would be in this case rather called a commit. But none applies to above primitives. Guards are rather inspired by Dijkstra's Guarded Command Language of 1975.
freeze(X, Goal)
(originally calledgeler
) is the same aswhen(nonvar(X), Goal)
and they both are declaratively equivalent toGoal
. There is no direct relation to the functionality of guards. However, when used together with if-then-else you might implement such a guard. But that is pretty different.freeze/2
and similar constructs were for some time considered as a general way to improve Prolog's execution mechanism. However, they turned out to be very brittle to use. Often, they were too conservative thus delaying goals unnecessarily. That is, almost every interesting query produced a "floundering" answer as the query below. Also, the borderline between terminating and non-terminating programs is now much more complex. For pure monotonic Prolog programs that terminate, adding some terminating goal into the program will preserve termination of the entire program. However, withfreeze/2
this is no longer the case. Then from a conceptual viewpoint,freeze/2
was not very well supported by the toplevels of systems: Only a few systems showed the delayed goals in a comprehensive manner (e.g. SICStus) which is crucial to understand the difference between success/answers and solution. With delayed goals Prolog may now produce an answer that has no solution as this one:Another difficulty with
freeze/2
was that termination conditions are much more difficult to determine. So, whilefreeze
was supposed to solve all the problems with termination, it often created new problems.And there are also more technical difficulties related to
freeze/2
in particular w.r.t tabling and other techniques to prevent loops. Consider a goalfreeze(X, Y = 1)
clearly,Y
is now1
even if it is not yet bound, it still awaitsX
to be bound first. Now, an implementation might consider tabling for a goalg(Y)
.g(Y)
will now have either no solution or exactly one solutionY = 1
. This result would now be stored as the only solution forg/1
since thefreeze
-goal was not directly visible to the goal.It is for such reasons that
freeze/2
is considered the goto of constraint logic programming.Another issue is
dif/2
which today is considered a constraint. In contrast tofreeze/2
and the other coroutining primitives, constraints are much better able to manage consistency and also maintain much better termination properties. This is primarily due to the fact that constraints introduce a well defined language were concrete properties can be proven and specific algorithms have been developed and do not permit general goals. However, even for them it is possible to obtain answers that are not solutions. More about answer and success in CLP.There is a paper by Evan Tick explaining CC:
THE DEEVOLUTION OF CONCURRENT LOGIC PROGRAMMING LANGUAGES
Evan Tick - 1995
https://core.ac.uk/download/pdf/82787481.pdf
So I guess with some when/2 magic, a commited choice code can be rewritten into ordinary Prolog. The approach would be as follows. For a set of commited choice rules of the same predicate:
This can be rewritten into the following, where Hi' and Gi' need to implement passive unification. For example by using ISO corrigendum subsumes_term/2.
The above translation wont work for CHR, since CHR doesn't throw away candidates.
freeze/2 and when/2 are like a "goto" of logic programming. They are not pure, commutative, etc.
dif/2, on the other hand, is completely pure and declarative, monotonic, commutative etc. dif/2 is a declarative predicate, it holds if its arguments are different. As to the "preferred Prolog programming style": State what holds. If you want to express the constraint that two general terms are different, dif/2 is exactly what states this.
Procedural considerations are typically most needed when you do not program in the pure declarative subset of Prolog, but use impure predicates that are not commutative etc. In modern Prolog systems, there is little reason to ever leave the pure and declarative subset.