Semantics and Backtracking

Appeared in Volume 6/4, November 1993

billaud@LaBRI.U-Bordeaux.FR
Michel Billaud
20th June 1993

Many authors have published formal descriptions for more or less realistic subsets of Prolog. See the papers by Egon Boerger, or the formal descriptions by Pierre Deransart for example.

B. Arbab, D.M. Berry, Operational and Denotational Semantics of Prolog, Journal of LP 1987, vol. 4, pp. 309-329.

E. Börger, A logical Operational Semantics of Full Prolog, IBM Technical Report IKBS 117 (1990)

I agree that, in some sense, these formal descriptions (especially denotational semantics) provide a way to turn a Prolog Program into a mathematical expression. If we follow this line, Prolog has a logical basis, but we could say the same thing - for the same reasons - about Scheme, or Turing Machines, or subsets of Cobol!

So what about "direct" translations? My point is that the famous "declarative reading" of Prolog programs as logical formulas (Horn Clauses) is only partially correct (or definitely wrong, depending on the day of the week :-)).

As far as I remember the first satisfactory semantics, which dealt with such things as cut, var and negation by failure, was presented in a paper by Jones and Mycroft:

N.D. Jones and H. Mycroft, Stepwise Development of Operational and Denotational Semantics for Prolog, Proc. 1984 Int. Symp. on LP (1984) pp.281-288.

Instead of the "set-of-success" idea (which is perhaps pertinent for SLD-resolution but definitely not relevant for Prolog), it follows the stream-of-success approach which is more natural and can, for example, be extended in a rather simple way to take read/write predicates into account as well.

Another interesting point made in an earlier net posting was about specifying algebraic laws for ';' and ',' in the context of backtracking.

If we consider only the signature <true,false,and,or>, there is a complete finite axiomatization:

true and X = X and true = X or false = false or X = X
false and X = false
assoc of 'and' and 'or'
(X or Y) and Z = (X and) Z or (Y and Z)

See:

"Axiomatizations of Backtracking", M Billaud, Proc. STACS'92, A. Finkel, M.Jantzen (eds), LNCS 577, pp.71-82

But it is still an open problem in the case of "pure Prolog", where new laws appear, such as:

(X and Y) or Z or (X and false) = (X and Y) or Z

I conjecture there is no finite axiomatization in this case, as there is a family of arbitrarily complicated formulas that cannot (apparently) be reduced by simpler ones.

jamie@cs.sfu.ca
Jamie Andrews
21st June 1993

Do you mean in the absence of recursive predicate definitions? This is certainly true, but not very useful. It is the combination of the backtracking mechanism with recursive predicates that causes problems. Perhaps, I should say the combination of backtracking with unrestricted Horn clauses; of course you can make things well-behaved if you restrict function symbols to nullary, or prohibit variables appearing only in the body, etc.

In my thesis, I discussed ways in which we can consider the backtracking behaviour of depth-first, left-to-right logic programming to be logical. A reference is:

Andrews, James H., Logic Programming: Operational Semantics and Proof Theory, University of Edinburgh, Department of Computer Science, March, 1991, Cambridge University Press, Distinguished Dissertation Series

Some of that work was published earlier in:

Andrews, James H., The Logical Structure of Sequential Prolog, Proc. of the 1990 North American Conf. on LP, Austin, Texas, October-November, MIT Press, pp.585-602, 1990

These references give a very syntactic, proof-theoretic treatment of Prolog behaviour. I have lately been working on more abstract semantics which look more like traditional logical semantics.

A recent paper of mine discusses this semantic approach, and adds negation to the picture.

Basically, I don't think that we can characterize the behaviour of Prolog with only a truth functional least model and valuation approach, or with just a logical equivalences and finite axiomatization approach. However, a combination of these approaches seems to capture its behaviour using only constructs which we can easily accept as "logical". The way in which the constructs interact, though, is complex, and does detract from the logical flavour of the whole.