
2.
Continuation Semantics for Prolog with Cut
A. de Bruin
Faculty of Economics,
Erasmus Universiteit, P.O.Box 1738, NL3000 DR Rotterdam
E.P. de Vink
Department of Mathematics and Computer Science,
Vrije Universiteit, De Boelelaan 1081, NL1081 HV Amsterdam
ABSTRACT We present a denotational continuation semantics for Prolog with cut. First a uniform language B is studied, which captures the control flow aspects of Prolog. The denotational semantics for B is proven equivalent to a transition system based operational semantics. The congruence proof relies on the representation of the operational semantics as a chain of approximations and on a convenient induction principle. Finally, we interpret the abstract language B such that we obtain equivalent denotational and operational models for Prolog itself.
Section 1 Introduction
In the nice textbook of Lloyd [Ll] the cut, available in all Prologsystems, is described as a controversial control facility. The cut, added to the Horn clause logic for efficiency reasons, affects the completeness of the refutation procedure. Therefore the standard declarative semantics using Herbrand models does not adequately capture the computational aspects of the Prologlanguage. In the present paper we study the Prologcut operator in a sequential environment augmented with backtracking. Our aim is to provide a denotational semantics for Prolog with cut and to prove this semantics equivalent to an operational one.
First of all we separate the ?logic programming? details (such as most general unifiers and renaming indices) in Prolog from the specification of the flow of control, (e.g. backtracking, the cut operator). This is achieved by extracting the uniform language B from Prolog  uniform in the sense of [BKMOZ]  which contains only the latter issues. Fitting within the ?Logic Programming without Logic? approach, ([Ba2]), our denotational model developed for the abstract backtracking language has enough flexibility for further elaboration to a nonuniform denotational model of Prolog itself. Moreover, the equivalence of this denotational semantics and an operational semantics for Prolog is a straightforward generalization for the congruence proof of B.
Secondly, our denotational semantics uses continuations. This has several advantages over earlier semantics which (essentially) are based on a direct approach. (See [Br] for a discussion on the relative merits of continuations vs. direct semantics.) We arrive at a concise set of semantical equations in which there is no need for coding up the states using cut flags