A Compositional Semantics for eval in Scheme

Abstract

The Scheme programming language was introduced in 1975 as a lexically-scoped dialect of Lisp. It has subsequently been improved and extended through many rounds of standardization, documented by the Scheme Reports. In Lisp, eval is a function taking a single argument; when the value of the argument represents an expression, eval proceeds to evaluate it in the current environment. The Scheme procedure eval is similar, but takes an extra argument that determines the evaluation environment. The so-called classic standards for Scheme and its latest modern standard all include a denotational semantics of core expressions and of some required procedures. However, the semantics does not cover eval. When Muchnick and Pleban compared the denotational semantics of Lisp and Scheme in 1980, they wrote that it was not possible to give a structural semantics of eval expressions. Similarly, in 1984, Clinger pointed out that the semantics of eval violates compositionality; he suggested to define eval using a non-compositional copy of the semantic function. This paper adapts Clinger’s suggestion by letting the semantic function take an extra argument, then defining that argument by an explicit fixed point. The resulting semantics of eval expressions is fully compositional. The wellformedness of the semantics has been tested using a lightweight Agda formalization; verifying that the denotations have expected properties is work in progress.