Functional dependencies and Moore-set completions of abstract interpretations and semantics

We introduce the notion of functional dependencies of abstract interpretations rela- tively 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 autodepen- dencies, 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 depen- dencies can be applied in collecting semantics design by abstract interpretation to systematically derive compositional semantics for logic programs.