An Algebraic Theory of Observables.
Marco Comini, Giorgio Levi · 1994
We give an algebraic formalization of SLD-trees and their abstractions (observables) . We can state and prove in the framework several useful theorems (AND-compositionality, correctness and full abstraction of the denotation, equivalent top-down and bottom-up constructions) about semantic properties of various observables. Observables are represented by Galois co-insertions and can be used to model abstract interpretation. The constructions and the theorems are inherited by all the observables which can be formalized in the framework. The power of the framework is shown by reconstructing some known examples (answer constraints, call patterns, correct call patterns and ground dependencies call patterns). 1 Introduction SLD-trees are structures used to describe the operational semantics of logic programs. From an SLD-tree we can derive several operational properties which are useful for reasoning about programs. Examples are SLD - derivations, resultants, call patterns, partial answers,...