Compositionality in SLD-Derivations and their Abstractions.
Marco Comini, Giorgio Levi, Maria Chiara Meo · 1995
We define a semantic framework to reason about compositional properties of SLD-derivations and their abstractions (observables). The framework allows us to address problems such as the relation between the (top-down) operational semantics and the (bottom-up) denotational semantics, the existence of a denotation for a set of definite clauses and their properties (compositionality w.r.t. various syntactic operators, correctness and minimality). This leads us to a flexible classification of the observables, where we can reason about properties such as OR-compositionality and existence of abstract transition system. Using abstract interpretation techniques to model abstraction allows us to state very simple conditions on the observables which guarantee the validity of several general theorems. Keywords: SLD-derivations, abstract semantics, compositionality. 1 Introduction Our goal is the definition of a semantic framework, which allows us to reason about properties of SLD-derivations and...