Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics

We introduce the notion of functional dependencies of abstract interpretations relatively to a binary operator of composition. Functional dependencies are obtained by a functional composition of abstract domains, and provide a systematic approach to construct new abstract domains. In particular, we study the case of autodependencies, namely monotone operators on a given abstract domain. Under suitable hypotheses, this corresponds to a Moore-set completion of the abstract domain, providing a compact lattice-theoretic representation for dependencies. We prove that the abstract domain Def for ground-dependency analysis of logic programs can be systematically derived by autodependencies of a more abstract (and simple) domain for pure groundness analysis. Furthermore, we show that functional dependencies can be applied in collecting semantics design by abstract interpretation to systematically derive compositional semantics for logic programs