Building Complete Abstract Interpretations in a Linear Logic-based Setting

Completeness is rather uncommon, although important, property of abstract interpretations, which arises especially in comparative semantics. Recently, the first two authors proved that in most cases, given any abstract domain $A$, there exists the most abstract domain, called least complete extension of $A$, which includes $A$ and provides a complete abstract interpretation. In this paper we distinguish between the standard formulation of completeness, called full completeness, and a novel and particularly interesting one, called observation completeness. In particular we consider the problem of full and observation completeness in the context of quantales, i.e. models of linear logic, as concrete interpretations. We prove that various types of least complete extensions exist and, more importantly, we show that these extensions can all be specified in terms of an elegant linear logic-based formulation. As an application, we determine the least fully complete extension of a generic abstract domain w.r.t. a standard bottom-up concrete semantics characterizing computed answer substitutions. This general result is further instantiated to the case of groundness analysis