Denotational and operational semantics for prolog

Saumya K. Debray; Prateek Mishra

doi:10.1016/0743-1066(88)90007-6

Denotational and operational semantics for prolog

Saumya K. Debray, Prateek Mishra

Computer Science

Research output: Contribution to journal › Article › peer-review

51 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	61-91
Number of pages	31
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	5
Issue number	1
DOIs	https://doi.org/10.1016/0743-1066(88)90007-6
State	Published - Mar 1988

ASJC Scopus subject areas

Logic

Access to Document

10.1016/0743-1066(88)90007-6

Cite this

@article{394c5ca2b683448f8a6245aaec3c2e42,

title = "Denotational and operational semantics for prolog",

abstract = "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.",

author = "Debray, \{Saumya K.\} and Prateek Mishra",

note = "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.",

year = "1988",

month = mar,

doi = "10.1016/0743-1066(88)90007-6",

language = "English (US)",

volume = "5",

pages = "61--91",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "0743-1066",

publisher = "Elsevier Inc.",

number = "1",

}

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/inward/citedby.url?scp=0023979551&partnerID=8YFLogxK

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 Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

IS - 1

ER -

Denotational and operational semantics for prolog

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this