Making Abstract Domains Condensing

TL;DR

This paper introduces condensing abstract domains that preserve analysis precision in logic languages by refining domains to align goal-driven and goal-independent semantics, leveraging linear logic structures.

Contribution

It formalizes condensing abstract domains as a property and provides a systematic method to refine any domain to be condensing using linear logic-based techniques.

Findings

Condensing domains ensure goal-driven and goal-independent analyses agree.

Refinement of domains can be achieved via a simple operator based on linear logic.

Condensing domains can be explicitly characterized using linear logic formulations.

Abstract

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.