Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements

By: R. Giacobazzi and F. Ranzato

Roberto Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso Italia 40, 56125 Pisa (Italy)


We introduce the notion of uniform closure operator, and we show how this concept surfaces in two different areas of application of abstract interpretation theory, notably in the field of the hierarchies of semantics for logic programs, and in the theory of refinement operators of abstract domains. In logic programming, uniform closures permit to generalize from an order-theoretic perspective the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the model-theoretic characterization of the well known s-semantics using pure order-theoretic concepts only. On the other hand, we consider the systematic operators of refinement (as far as precision is concerned) of abstract domains, and we show that uniform closures model precisely the property of an abstract domain refinement of being invertible, namely of admitting a related operator that simplifies in the best possible way a given domain for that refinement. Exploiting the same argument used to reconstruct the s-semantics of logic programming, that is uniform closures, we give a precise relationship between domain refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.

Available: DVI, PostScript, BibTeX Entry.

Related works by the authors:
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2):333-336, 1996)
  • Optimal domains for disjunctive abstract interpretation (To appear in Sci. of Comp. Prog.)
  • Refining and compressing abstract domains (ICALP'97, 1997).
  • Complementation in Abstract Interpretation (ACM TOPLAS 19(1), 1997).

  • giaco@sci.univr.it