A self-interpreter is a meta-circular interpreter where the host language is also the language being interpreted. A self-interpreter displays a
universal function for the language in question, and can be helpful in learning certain aspects of the language. Here is the core of a self-evaluator for the \lambda calculus. The abstract syntax of the \lambda calculus is implemented as follows in
OCaml, representing variables with their
de Bruijn index, i.e., with their lexical offset (starting from 0): type term = IND of int (* de Bruijn index *) | ABS of term | APP of term * term The evaluator uses an environment: type value = FUN of (value -> value) let rec eval (t : term) (e : value list) : value = match t with IND n -> List.nth e n | ABS t' -> FUN (fun v -> eval t' (v :: e)) | APP (t0, t1) -> apply (eval t0 e) (eval t1 e) and apply (FUN f : value) (a : value) = f a let main (t : term) : value = eval t [] Values (of type value) conflate expressible values (the result of evaluating an expression in an environment) and denotable values (the values denoted by variables in the environment), a terminology that is due to
Christopher Strachey. Environments are represented as lists of denotable values. The core evaluator has three clauses: • It maps a variable (represented with a de Bruijn index) into the value in the current environment at this index. • It maps a syntactic function into a semantic function. (Applying a semantic function to an argument reduces to evaluating the body of the corresponding syntactic function in its lexical environment, extended with the argument.) • It maps a syntactic application into a semantic application. This evaluator is
compositional in that each of its recursive calls is made over a proper sub-part of the given term. It is also
higher order since the domain of values is a function space. In "Definitional Interpreters", Reynolds answered the question as to whether such a self-interpreter is well defined. He answered in the negative because the
evaluation strategy of the defined language (the source language) is determined by the evaluation strategy of the defining language (the meta-language). If the meta-language follows call by value (as OCaml does), the source language follows call by value. If the meta-language follows call by name (as
Algol 60 does), the source language follows call by name. And if the meta-language follows call by need (as
Haskell does), the source language follows call by need. In "Definitional Interpreters", Reynolds made a self-interpreter well defined by making it independent of the evaluation strategy of its defining language. He fixed the evaluation strategy by transforming the self-interpreter into
continuation-passing style, which is evaluation-strategy independent, as later captured in
Gordon Plotkin's Independence Theorems. Furthermore, because
logical relations had yet to be discovered, Reynolds made the resulting continuation-passing evaluator first order by (1)
closure-converting it and (2)
defunctionalizing the continuation. He pointed out the "machine-like quality" of the resulting interpreter, which is the origin of the
CEK machine since Reynolds's CPS transformation was for call by value. For call by name, these transformations map the self-interpreter to an early instance of the
Krivine machine. The
SECD machine and many other abstract machines can be inter-derived this way. It is remarkable that the three most famous abstract machines for the \lambda calculus functionally correspond to the same self-interpreter.
Self-interpretation in total programming languages Total functional programming languages that are
strongly normalizing cannot be
Turing complete, otherwise one could solve the halting problem by seeing if the program type-checks. That means that there are computable functions that cannot be defined in the total language. In particular it is impossible to define a self-interpreter in a total programming language, for example in any of the
typed lambda calculi such as the
simply typed lambda calculus,
Jean-Yves Girard's
System F, or
Thierry Coquand's
calculus of constructions. Here, by "self-interpreter" we mean a program that takes a source term representation in some plain format (such as a string of characters) and returns a representation of the corresponding normalized term. This impossibility result does not hold for other definitions of "self-interpreter". For example, some authors have referred to functions of type \pi\,\tau \to \tau as self-interpreters, where \pi\,\tau is the type of representations of \tau-typed terms. To avoid confusion, we will refer to these functions as
self-recognizers. Brown and Palsberg showed that self-recognizers could be defined in several strongly-normalizing languages, including
System F and System Fω. This turned out to be possible because the types of encoded terms being reflected in the types of their representations prevents constructing a
diagonal argument. In their paper, Brown and Palsberg claim to disprove the "conventional wisdom" that self-interpretation is impossible (and they refer to Wikipedia as an example of the conventional wisdom), but what they actually disprove is the impossibility of self-recognizers, a distinct concept. In their follow-up work, they switch to the more specific "self-recognizer" terminology used here, notably distinguishing these from "self-evaluators", of type \pi\,\tau \to \pi\,\tau. They also recognize that implementing self-evaluation seems harder than self-recognition, and leave the implementation of the former in a strongly-normalizing language as an open problem. == Uses ==