2002/04/09 by R. Giacobazzi, Roberto Giacobazzi, F. Ranzato +6
Computer Science · #D.3.1 #D.3.2 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.cs/0204016
20 pages
arxiv created 2002/04/09 · openalex publication_date 2002/04/09 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper we show that reversible analysis of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains. The idea is to include semantic structures into abstract domains in such a way that the refined abstract domain becomes rich enough to allow approximate bottom-up and top-down semantics to agree. These domains are known as condensing abstract domains. Substantially, an abstract domain is condensing if goal-driven and goal-independent analyses agree, namely no loss of precision is introduced by approximating queries in a goal-independent analysis. We prove that condensation is an abstract domain property and that the problem of making an abstract domain condensing boils down to the problem of making the domain complete with respect to unification. In a general abstract interpretation setting we show that when concrete domains and operations give rise to quantales, i.e. models of propositional linear logic, objects in a complete refined abstract domain can be explicitly characterized by linear logic-based formulations. This is the case for abstract domains for logic program analysis approximating computed answer substitutions where unification plays the role of multiplicative conjunction in a quantale of idempotent substitutions. Condensing abstract domains can therefore be systematically derived by minimally extending any, generally non-condensing domain, by a simple domain refinement operator.