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)
giaco@di.unipi.it
Abstract:
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:
giaco@sci.univr.it