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.

Building Complete Abstract Interpretations in a Linear Logic-based Setting

RANZATO, FRANCESCO;
1998

Abstract

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.
1998 Joint Conference on Declarative Programming, APPIA-GULP-PRODE'98, A Coruña, Spain
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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: https://hdl.handle.net/11577/2509492
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 9
social impact