Denotational and operational semantics for PROLOG.
Saumya Debray, Prateek Mishra · 1987
: 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 behavior 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 captures the computational behavior 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 a standard operational interpreter. As an application of our denotational semantics, we show the correctness of some standard "folk" theorems regarding transformations on Prolog programs. ############################# + A preliminary version of this paper appears in the Proceedings of the IFIP Conference on Formal Description of Programming Concepts, Ebberu...