[<<][staapl][>>][..]
Fri Sep 18 19:09:10 CEST 2009

Abstract Interpretation: Lattices

While intuitively, abstract interpretation for staging (symbolic
computation) is quite straightforward to do, the mathematical
definition relies on order-preserving functions on lattices.

A canonical example of a lattice is the set of subsets of a set,
together with union and intersection (a boolean lattice[1]).

I.e. arithmetic can be approximated over the lattice made up of the
subsets of {+,0,-}.

        {+} add {+}  -> {+}
        {-} add {+}  -> {+,0,-} = T
        x   mul {0}  -> {0}
        ...

So..  The missing links and terminology seem to come from denotational
semantics[2].  As far as I get it now, an abstract semantics is
related to a full denotational semantics in some structure-preserving
way.

Attempt:

In the following diagram L and L' are lattices, f is a concrete
function, f' an abstract function, a : L->L' is the abstraction
function and c : L'->L is the concretization function.  The a and c
are ``semi-inverses'' in that they preserve order: they form a Galois
Connection[5].

The abstraction is sound when whenever c acts as a
``semi-homomorphism'' f . c < c . f' respecting the order relation
instead of an equivalence, i.e. the following diagram commutes:

                              f
                       L  --------->  L

                       ^              ^
                       |              |
                       | c            | c
                       |              |
                       |              |
                              f'
                       L' --------->  L'

In other words, soundness means that for any concrete operation forall
x, f x = y, if x \in c(x') then y \in c(f' x') meaning that for all x,
if x' is an abstraction of x and f' is an abstraction of f then f'x'
is an abstraction of y.

It's convenient to picture the original semantics L as the powerset of
some set |L (i.e. the natural numbers |N): already containing all
approximations.

In this case the abstract representation L' is related to |L by
mapping elements l' to subsets of |L.  The order relation in L
represents ``level of abstraction''.  I.e. the element + in L' could
map to the element {0,1,2,...} in L.

Now, from the first lecture of Cousot[7], we find: Abstract
interpretation is considering an abstract semantics that is a
_superset_ of the concrete semantics of the program, hence it covers
all possible concrete cases.  This leads to the requirements: 1. sound
(cover all cases) 2. precise (avoid false alarms) and 3. simple (avoid
combinatorial explosion).

So, conclusions: what I'm doing at the moment is a combination of
several techniques: it produces a trace (abstract evaluation of the
interpretation step function) + approximates values by values U
variables / expressions.  It would be interesting to try to formalize
this.  Soundness seems ``obvious'' in my case, so te proof shouldn't
be too difficult (probably trivial once there's a formal model).  In
general however, it does seem like a good idea to try to keep the
theory in mind next time I need to do some analysis, and use specific
applications as an example.


[1] http://en.wikipedia.org/wiki/Boolean_lattice
[2] http://en.wikipedia.org/wiki/Denotational_semantics
[3] http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk1p.pdf
[4] http://santos.cis.ksu.edu/schmidt/Escuela03/home.html
[5] http://en.wikipedia.org/wiki/Galois_connection
[6] http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk3p.pdf
[7] http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/




[Reply][About]
[<<][staapl][>>][..]