Beyond the s-Semantics: a Theory of Observables
Marco Comini, Giorgio Levi · 2017
We give an algebraic formalization of SLD -trees and their abstractions (observables). We can state and prove in the framework several useful theorems (lifting, 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, finite failures, call patterns, correct call patterns and ground dependencies call patterns).