Building Complete Abstract Interpretations in a Linear Logic-based Setting

Completeness is a precious and rather uncommon property of abstract interpretations, which depends only on the underlying abstract domains, and arises especially in comparative semantics. We distinguish here between the standard formulation of completeness, called full completeness, and a novel and particularly interesting one, called observation completeness. Recently, the first two authors showed that least fully complete extensions exist in most cases. 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 explicitly exhibit such complete abstract domains by showing that they enjoy a particularly elegant and linear logic-based formulation. As an application in the field of logic program analysis, 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. In particular, this general result is instantiated to the case of groundness analysis.