Denotational and operational semantics for prolog

Saumya K Debray, Prateek Mishra

Research output: Contribution to journalArticle

50 Citations (Scopus)

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 languageEnglish (US)
Pages (from-to)61-91
Number of pages31
JournalJournal of Logic Programming
Volume5
Issue number1
DOIs
StatePublished - 1988
Externally publishedYes

Fingerprint

Denotational Semantics
Operational Semantics
Prolog
PROLOG (programming language)
Semantics
Folk Theorem
Model Theory
First-order Logic
Congruence
Correctness
Evaluation
Standards

ASJC Scopus subject areas

  • Logic

Cite this

Denotational and operational semantics for prolog. / Debray, Saumya K; Mishra, Prateek.

In: Journal of Logic Programming, Vol. 5, No. 1, 1988, p. 61-91.

Research output: Contribution to journalArticle

Debray, Saumya K ; Mishra, Prateek. / Denotational and operational semantics for prolog. In: Journal of Logic Programming. 1988 ; Vol. 5, No. 1. pp. 61-91.
@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",
year = "1988",
doi = "10.1016/0743-1066(88)90007-6",
language = "English (US)",
volume = "5",
pages = "61--91",
journal = "Journal of Logic Programming",
issn = "1567-8326",
publisher = "Elsevier Inc.",
number = "1",

}

TY - JOUR

T1 - Denotational and operational semantics for prolog

AU - Debray, Saumya K

AU - Mishra, Prateek

PY - 1988

Y1 - 1988

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 - http://www.scopus.com/inward/record.url?scp=0023979551&partnerID=8YFLogxK

UR - http://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

VL - 5

SP - 61

EP - 91

JO - Journal of Logic Programming

JF - Journal of Logic Programming

SN - 1567-8326

IS - 1

ER -