In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a nice basis for a wide variety of collecting semantics, abstract interpretations, symbolic executions, and their intermixings. But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called "pushdown control flow" property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language. The first approaches to achieve this property for higher-order languages appeared within the last ten years, and have since been the subject of many papers. These approaches start from a state-machine semantics and uniformly involve significant technical engineering to recover the precision of pushdown control flow. In contrast, starting from a definitional interpreter, the pushdown control flow property is inherent in the metalanguage and requires no further technical mechanism to achieve. the set of reachable states is straightforward. The essence of the state-machine based approach was distilled by Van Horn and Might in their "abstracting abstract machines" (AAM) technique, which provides a systematic method for constructing abstract interpreters from standard abstract machines like the CEK-or Krivine-machines [Van Horn and Might 2010] . Language designers who would like to build abstract interpreters and program analysis tools for their language can now, in principle at least, first build a state-machine interpreter and then turn the crank to construct the approximating abstract counterpart. A natural question to arise from this past work is to wonder: can a systematic abstraction technique similar to AAM be carried out for interpreters written, not as state-machines, but instead as high-level definitional interpreters, i.e. recursive, compositional evaluators? This functional pearl answers in the affirmative and demonstrates some of the interesting consequences of doing so. First, we show the AAM recipe can be applied to definitional interpreters with only a slight adaptation of the original method. The primary technical challenge in this new setting is handling interpreter fixed-points in a way that is both sound and always terminates-a naive abstraction of fixed-points will be sound but isn't always terminating, and a naive use of caching for fixedpoints will guarantee termination but is inherently unsound. We address this technical challenge with a caching fixed-point-finding algorithm which is both sound and guaranteed to terminate when abstracting arbitrary definitional interpreters. Second, we claim that the abstract definitional interpreter perspective is fruitful in two regards. The first is unsurprising: high-level abstract interpreters offer the usual beneficial properties of their concrete counterparts in terms of being re-usable and extensible. In particular, we show that abstract interpreters can be structured with monad transformers to good effect. The second regard is more surprising, and we consider its observation to be the main contribution of this pearl. Definitional interpreters, in contrast to abstract machines, can leave aspects of computation implicit, relying on the semantics of the defining-language to define the semantics of the definedlanguage, an observation made by Reynolds [1972] in his landmark paper, Definitional Interpreters for Higher-order Programming Languages. For example, Reynolds showed it is possible to write a definitional interpreter such that it defines a call-by-value language when the metalanguage is callby-value, and defines a call-by-name language when the metalanguage is call-by-name. Inspired by Reynolds, we show that abstract definitional interpreters can likewise inherit properties of the metalanguage. In particular we construct an abstract definitional interpreter where there is no explicit representation of continuations or a call stack. Instead the interpreter is written in a straightforward recursive style, and the call stack is implicitly handled by the metalangauge. What emerges from this construction is a total abstract evaluation function that soundly approximates all possible concrete executions of a given program. But remarkably, since the abstract evaluator relies on the metalanguage to manage the call stack implicitly, it is easy to observe that it introduces no approximation in the matching of calls and returns, and therefore implements a "pushdown" analysis [Earl et al. 2010; Vardoulakis and Shivers 2011] , all without the need for any explicit machinery to do so.
Definitional interpreters have been suggested as a technique for building compositional abstract interpreters REF .
Abstracting definitional interpreters (functional pearl)
PACMPL
Computer Science