Optimal Semantics and Domains in Logic Program Analysis

Completeness is important in approximated semantics design by abstract interpretation, ensuring that abstract computations are as precise as possible wrt concrete ones. The authors recently proved that any abstract domain can be systematically refined or simplified in order to provide its closest possible complete domain. The key problem here remains is to find efficient and appropriate representations for objects in complete abstract domains. In this paper we show that these domain trensformations, when applied on abstract interpretations of quantales, can all be explicitly characterized by elegant linear logic-based formulations. We apply our results to logic program analysis, where unification can be interpreted as multiplicative conjunction in a quantale of idempotent substitutions. We characterize the objects in optimal semantics for logic program analysis, viz. the most abstract concrete semantics for any static program analysis property, and the structure of condensing domains in logic program analysis.