Denotational Abstract Interpretation of Logic Programs

Kim Marriott, Harald Søndergaard, Neil D. Jones

Research output: Contribution to journalArticleResearchpeer-review

55 Citations (Scopus)

Abstract

Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism 1994. Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation. We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.

Original languageEnglish
Pages (from-to)607-648
Number of pages42
JournalACM Transactions on Programming Languages and Systems (TOPLAS)
Volume16
Issue number3
DOIs
Publication statusPublished - 5 Jan 1994

Keywords

  • abstract interpretation
  • Boolean functions
  • dataflow analysis
  • global analysis
  • groundness analysis

Cite this

Marriott, Kim ; Søndergaard, Harald ; Jones, Neil D. / Denotational Abstract Interpretation of Logic Programs. In: ACM Transactions on Programming Languages and Systems (TOPLAS). 1994 ; Vol. 16, No. 3. pp. 607-648.
@article{4bdb8e00c8124a1f91df28e9e699756e,
title = "Denotational Abstract Interpretation of Logic Programs",
abstract = "Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism 1994. Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation. We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.",
keywords = "abstract interpretation, Boolean functions, dataflow analysis, global analysis, groundness analysis",
author = "Kim Marriott and Harald S{\o}ndergaard and Jones, {Neil D.}",
year = "1994",
month = "1",
day = "5",
doi = "10.1145/177492.177650",
language = "English",
volume = "16",
pages = "607--648",
journal = "ACM Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery (ACM)",
number = "3",

}

Denotational Abstract Interpretation of Logic Programs. / Marriott, Kim; Søndergaard, Harald; Jones, Neil D.

In: ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, No. 3, 05.01.1994, p. 607-648.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Denotational Abstract Interpretation of Logic Programs

AU - Marriott, Kim

AU - Søndergaard, Harald

AU - Jones, Neil D.

PY - 1994/1/5

Y1 - 1994/1/5

N2 - Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism 1994. Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation. We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.

AB - Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism 1994. Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation. We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.

KW - abstract interpretation

KW - Boolean functions

KW - dataflow analysis

KW - global analysis

KW - groundness analysis

UR - http://www.scopus.com/inward/record.url?scp=0028427829&partnerID=8YFLogxK

U2 - 10.1145/177492.177650

DO - 10.1145/177492.177650

M3 - Article

VL - 16

SP - 607

EP - 648

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 3

ER -