What is the goal behind abstract interpretation in programming languages?

Question

I am now trying to understand better what "abstract interpretation" in programming languages are. I found a good book chapter that explains the idea of extending the domain with a least fixed element, the four axioms that yield a fixed point for a continuous function, and so on. I understand these technical details (though I am not quite sure what is "abstract interpretation" exactly referring to in this whole scheme).

What I am not sure about is what motivates the use of abstract interpretation? Is it just identifying fixed points for computable functions? Is the main motivation coming from having recursion in most programming languages?

Would also be glad to get some high-level overview which does go technically deep enough for someone who has a degree in computer science. I find the Wikipedia page rather unsettling.

Answer 1

Abstract interpretation is a very general concept and depending on whom you ask, you will receive different explanations because versatile concepts admit multiple perspectives. The view in this answer is mine and I would not assume it is general.

Computational hardness as a motivation

Let's start with decision problems, whose solutions have a structure like this:

There is often an NP-hard lower bound on the procedure. Checking semantic properties of programs is even undecidable. What can we do?

Let's make two observations. First, we can sometimes solve specific problem instances even if we cannot solve the general problem. Second, applications like compiler optimization tolerate approximation in that a compiler that eliminates some but not all sources of inefficiency is useful. To make this intuition precise, we must answer:

1. What does it mean formally to solve some, but not all problem instances?
2. What is an approximate solution to a decision problem?

Abstract Interpretation Idea 1: Change the Problem Statement

To me, a major insight of abstract interpretation is to change the problem formulation so that instead of asking for a Yes/No answer, we ask for a Yes/No/Maybe answer.

As a consequence, every problem has a trivial, constant time solution (output Maybe). We can now shift our attention to deriving a procedure that does not always produce Maybe. To return to the questions above, a solution that works for some problem instances is one that returns Maybe on problems it cannot solve. Moreover, Maybe is an approximation of Yes and No because we are not certain what the answer is.

This idea is not restricted to decision problems. Consider these problems concerning programs.

1. Which lines of code in the program are dead (will never be executed)?
2. Which variables in the program have constant values?
3. Which assertions in the program are violated?

In all these situations, we can move from an exact solution to an approximate one by considering solutions that have some uncertainty.

1. What is a set of lines of code that is dead?
2. What is a set of variables in the program that have constant values?
3. What is a set of assertions in the program that is not violated?

The sets produced need not be the largest. This idea is extremely general and applies to problems that have little to do with program analysis.

1. Instead of adding $m$ and $n$, we can ask for a range $[a,b]$ in which the sum lies.
2. Instead of multiplying $m$ by $n$ we can ask for $k$ bits of the result (specific, common examples are the sign or the parity bit).
3. Instead of asking for the satisfying assignments to a formula, we can ask for a set that contains the satisfying assignments.

Note that we have not only changed the problem but also strictly generalized it because a solution to the original problem is still a solution to the modified problem. The big unanswered question now is: How can we find an approximate solution?

Abstract Interpretation Idea 2: Fixed Point Characterization of the Original Solutions

The second big idea is to observe that the set of solutions to many problems has a characterization as a fixed point in a lattice of candidate solutions. As an example, suppose you have a graph and you want to know if a vertex $t$ is reachable from a vertex $s$. We can break this down into finding the set $\mathit{Reach}(s)$ of all vertices reachable from $s$ and then checking if $t$ is in this set. We can further observe that $\mathit{Reach}(s)$ is the least solution to the equation:

$X = \{s\} \cup \{ w ~|~ v \text{ is in } X \text{ and } (v,w) \text{ is an edge}\}$

The value of a fixed point characterization is that the exact solution can be viewed as the limit of a series of approximations. In this example, the $n$-th element of the series is the set of graph vertices reachable in $n$ steps from $s$ and approximation is a subset of these vertices.

The fixed point characterization is a design decision. There are many different characterizations of a set of solutions. Each of them may have different advantages. In the case of programming languages, we have more structure than just dealing with a graph. The fixed point equations we care about can be defined by induction on structure of the input program. This idea is not specific to programs. When applying abstract interpretation to elements of a structured language such as a grammar, logical formula, program, arithmetic expression, etc. we can define fixed points by induction on the structure of some syntactic object.

By giving this fixed point characterization, we are committing to a specific way of computing solutions. We will not actually calculate this fixed point because it is at least as hard as solving the original problem, which brings us to the next step.

Abstract Interpretation Idea 3: Fixed Point Approximation

Instead of computing a fixed point of a function $F$ in a lattice $L$, we can compute a fixed point of another function $G$ in a lattice $M$. Provided certain conditions are met relating $M$ to $L$, a solution computed in $M$ is guaranteed to be an approximation of the solution in $L$. This is one of the foundational results of abstract interpretation, usually called the fixed point transfer theorem. The soundness condition is given either by Galois connections, or weaker settings involving abstraction or concretization functions, or soundness relations.

The fixed point transfer theorem guarantees that you do not have to prove that you are computing a sound approximation every time you design an approximate analysis. You only have to prove that the lattices $L$ (containing original solutions) and $M$ (containing approximations) and the functions $F$ and $G$ satisfy certain constraints. This is a big win if you are the designer of an analysis and you care about soundness.

You may find the intuition behind fixed point transfer insightful. We can think of a fixed point as the limit of a (possibly transfinite) chain of elements. Computing approximate solutions amounts to approximating this limit, which we can do by approximating elements of the chain.

The notion of approximation depends on the application. If you are using graph reachability to plan a trip, you may accept an approximation that tells you there is no path between $s$ and $t$ even if there is a path, but you will not be happy if the algorithm says there is a path from $s$ to $t$ where there is no path.

Abstract Interpretation Idea 4: Fixed Point Approximation Algorithms

Everything seen so far has been a mathematical existence result. The final step is to compute the approximation. When the lattice of approximations is finite (or if the ascending/descending chain condition is met), we can use a simple iterative procedure. If the lattice is infinite an iterative procedure may not suffice, though computing a fixed point may still be decidable. In this situation, many techniques are used to further approximate the solution, or to jump to an exact solution faster than a naive iteration algorithm. In the context of computing a solution, you hear terms like widening, narrowing, strategy iteration, acceleration, etc.

Summary

In my opinion, abstract interpretation provides a mathematical basis for the notion of abstraction in the same way that mathematical logic provides a mathematical basis for reasoning. The solutions to many problems we care about have characterizations as fixed points. This observation is not restricted to programming language problems and even to computer science. Approximate solutions can be characterized as approximations of fixed points and are computed with specialized algorithms. These characterizations and algorithms will exploit the structure of the problem instance. In the case of programs, this structure is given by the syntax of the language.

Computing approximations to problems that do not have a natural metric is an art constantly developed and refined by practitioners. Abstract interpretation is one mathematical theory for the science behind this art.

References There are several good tutorials on abstract interpretation that you can read.

1. A casual introduction to Abstract Interpretation, Patrick Cousot (Joint work with Radhia Cousot), Workshop on Systems Biology and Formals Methods (SBFM'12)
2. A gentle introduction to formal verification of computer systems by abstract interpretation, Patrick and Radhia Cousot, Marktoberdorf Summer School 2010.
3. Lecture 13: Abstraction Part I, Patrick Cousot, Abstract interpretation, MIT Course.
4. Introduction to Abstract Interpretation, Samson Abramsky and Chris Hankin, Abstract Interpretation of Declarative Languages, 1987.
5. Abstract interpretation and application to logic programs, Patrick and Radhia Cousot, 1992. The first two sections have a general, high-level overview with several examples.

Answer 2

I agree that it's often hard to extract the main point from all those details. (In fact, my big issue with every treatment of abstract interpretation I've seen is that they present so much machinery without motivating it.)

Here's how I think of it:

Abstract interpretation is running programs, approximately, on large sets of inputs all at once.

This doesn't cover everything, but it holds up well in general.

The canonical example is evaluating arithmetic expressions to determine the sign of the result. You can imagine a hypothetical, infinitely fast machine that can evaluate an expression on every positive input and return the set of results. If you had one of those, you could in principle determine things like "this program returns positive numbers when given positive numbers."

But of course you don't actually have that machine. You're stuck in real life, so you have to either do the same thing symbolically, which can give exact answers sometimes but often fail, or approximately, in a way that always returns answers but they may not be exact. The latter is what abstract interpretation does.

You can't even represent the set of all positive numbers directly. Instead, you need an abstraction of that set. You also need to abstract the negative numbers and zero. You end up with a family of finite abstract sets $\{neg,zero,pos\}$, that represent the concrete sets $\{\{...,-2,-1\},\{0\},\{1,2,...\}\}$.

Now you can come up with rules, such as "adding two positive numbers results in a positive number," or $add : pos \times pos \to pos$. Come up with rules for each of your language primitives, and you can pretend to evaluate arithmetic expressions on large sets of inputs all at the same time.

Of course, the "adding a positive and a negative number" rule will give you trouble, because additions like that can return anything. The abstract interpretation framework helps you out, here: it says you should return a sound approximation that is as tight as possible. If your rules are sound, and they say addition returns something in an abstract set, any concrete evaluation should return a number in the corresponding concrete set. For example, the $add : pos \times pos \to pos$ rule is sound if $add(a,b)$ is positive for every positive $a$ and $b$. Also, $pos \times neg \to (pos \sqcup zero \sqcup neg)$ is sound, where "$\sqcup$" is your abstract sets' union operation.

I believe even the youngest PL researcher could code up an abstract interpretation like this in an afternoon. It's actually not that hard, and you should try it before reading much more to get a feel for the basics. While you do, you'll discover that your abstract sets need some notion of intersection (denoted "$\sqcap$") and subset (denoted "$\sqsubseteq$"). They should correspond with concrete intersection and subset.

When you want to prove that your abstract interpretation is as tight as possible, you'll want a Galois connection to formalize this correspondence. Just having one ensures that, for any given concrete set, a tightest abstract set exists.

When you want to work with a language with loops or recursion, your programs may not terminate, so you'll need a $\bot$ value to represent nontermination. You'll need to "compute" (in a mathematical sense) concrete functions as fixpoints, and compute abstract functions similarly. If you have higher-order functions, you'll find that typical topological machinery doesn't handle them at all (higher-order application is generally not continuous), and need Scott domains.

IOW, what you've identified as the motivation for abstract interpretation is really the motivation for the machinery required for doing abstract interpretation on Turing-equivalent languages. The actual motivation is usefully summarizing the behavior of programs by running them on many inputs at once.