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.
What is the goal behind abstract interpretation in programming languages?
pl.programming languages;program analysis
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 motivationLet'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:What does it mean formally to solve some, but not all problem instances?What is an approximate solution to a decision problem?Abstract Interpretation Idea 1: Change the Problem StatementTo 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.Which lines of code in the program are dead (will never be executed)?Which variables in the program have constant values?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.What is a set of lines of code that is dead? What is a set of variables in the program that have constant values?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.Instead of adding $m$ and $n$, we can ask for a range $[a,b]$ in which the sum lies. 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).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 SolutionsThe 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 ApproximationInstead 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 AlgorithmsEverything 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.SummaryIn 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.ReferencesThere are several good tutorials on abstract interpretation that you can read.A casual introduction to Abstract Interpretation, Patrick Cousot (Joint work with Radhia Cousot), Workshop on Systems Biology and Formals Methods (SBFM'12)A gentle introduction to formal verification of computer systems by abstract interpretation, Patrick and Radhia Cousot, Marktoberdorf Summer School 2010.Lecture 13: Abstraction Part I, Patrick Cousot, Abstract interpretation, MIT Course.Introduction to Abstract Interpretation, Samson Abramsky and Chris Hankin, Abstract Interpretation of Declarative Languages, 1987.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.