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.

Building Complete Abstract Interpretations in a Linear Logic-based Setting

GIACOBAZZI, Roberto;
1998

Abstract

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.
3540650148
Completeness; abstract interpretation; semantics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/438346
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 9
social impact