2.

Retractions in Comparing Prolog Semantics

A. de Bruin

Faculty of Economics, Erasmus Universiteit, P.O. Box 1738, NL-3000 DR Rotterdam

E.P. de Vink

Department of Mathematics and Computer Science,
Vrije Universiteit, De Boelelaan 1081, NL-1081 HV Amsterdam

ABSTRACT We present an operational model O and a continuation based denotational model D for a uniform variant of Prolog, including the cut operator. The two semantical definitions make use of higher order transformations F and Y, respectively. We prove O and D equivalent in a novel way by comparing yet another pair of higher order transformations F? and Y? , that yield F and Y, respectively, by application of a suitable abstraction operator.

Section 1 Introduction

In [BV] we presented both an operational and a denotational continuation based semantics for the core of Prolog, and we proved these two semantics equivalent. We used a two step approach, by first deriving these results for an intermediate language, obtained by stripping the logic programming aspects (substitutions, most general unifiers and all that) from Prolog. This resulted in the abstract language B in which only the control structure from Prolog remained, such as the backtrack mechanism and the cut operator. After having compared the operational and denotational meanings for B successfully we generalized as a next step the two semantics to the case of Prolog while preserving their equivalence.

The language B will be investigated again in this paper, but now more as a guinea pig. We will use it to test a new idea for proving equivalence of operational and denotational semantics based on cpo's. The main virtue of B in this respect is that although it is a sequential language it has a nontrivial control structure. In fact, the denotational semantics of this language needs three continuations to adequately describe the flow of control.

We will discuss our new approach to equivalence proofs by comparing it with the standard way these proofs have been conducted so far. To this end, we first spend a few words on operational semantics. The main idea behind this brand of semantics is to describe how an abstract machine executes a program in the language of interest. The abstract machine is defined by specifying the configurations it can be in, and by introducing a step function, mapping configurations to configurations, thus describing the behavior of the abstract machine. Starting from an initial configuration Co , repeatedly applying the step function will deliver a number of intermediate configurations Co, C1 , C 2, with Ci+1 = step Ci . The computation