Denotational and Operational Semantics for Prolog
Department of Computer Science
SUNY at Stony Brook
Stony Brook, NY 11794, U.S.A.
The semantics of Prolog programs is usually given in terms of the model theory of first order logic. However, this does not adequately characterize the computational behaviour of Prolog programs. Prolog implementations typically use a sequential evaluation strategy based on the textual order of clauses and literals in a program, as well as non-logical features like ``cut''. In this work we develop a denotational semantics that expresses the computational behaviour of Prolog. We present a semantics for ``cut-free'' Prolog, which is then extended to Prolog with cut. For each case we develop a congruence proof that relates the semantics to an abstract interpreter. As an application of our denotational semantics, we show the correctness of some standard ``folk'' theorems regarding transformations on Prolog programs.