TY - JOUR
T1 - Denotational and operational semantics for prolog
AU - Debray, Saumya K.
AU - Mishra, Prateek
N1 - Funding Information:
Tucson, Arizona 85721. Received June 1987; accepted July 1987. *A preliminary version of this paper appears in the Proceedings of the IFIP Conference on Formal Description of Programming Concepts, Ebberup, Denmark, Aug. 1986. This work was supported in part by the National Science Foundation under grant number DCR-8407688.
PY - 1988/3
Y1 - 1988/3
N2 - The semantics of PROLOG programs is usually given in terms of the model theory of first-order logic. However, this does not adequately characterizethe 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 nonlogical features like cut. In this work we develop a denotational semantics that captures thecomputational 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.
AB - The semantics of PROLOG programs is usually given in terms of the model theory of first-order logic. However, this does not adequately characterizethe 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 nonlogical features like cut. In this work we develop a denotational semantics that captures thecomputational 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.
UR - https://www.scopus.com/pages/publications/0023979551
UR - https://www.scopus.com/pages/publications/0023979551#tab=citedBy
U2 - 10.1016/0743-1066(88)90007-6
DO - 10.1016/0743-1066(88)90007-6
M3 - Article
AN - SCOPUS:0023979551
SN - 0743-1066
VL - 5
SP - 61
EP - 91
JO - Journal of Logic Programming
JF - Journal of Logic Programming
IS - 1
ER -