Making Abstract Domains Condensing

Details Making Abstract Domains Condensing Making Abstract Domains Condensing

2002-04-09

arxiv.org/abs/cs/0204016v1

Computer Science

Programming Languages

20 pages

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Making Abstract Domains Condensing does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Making Abstract Domains Condensing, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Making Abstract Domains Condensing will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-387262