LISP and Symbolic Computation, 6(3/4)259-288
Lambda-Calculus SchemataMichael J. Fischer, Department of Computer Science, Yale University, Box 2158 Yale Station, New Haven, CT 06520-2158, U.S.A.
|
Abstract: A lambda-calculus schema is an expression of the
lambda calculus augmented by uninterpreted constant and operator
symbols. It is an abstraction of programming languages such as LISP
which permit functions to be passed to and returned from other
functions. When given an interpretation for its constant and operator
symbols, certain schemata, called lambda abstractions, naturally
define partial functions over the domain of interpretation. Two
implementation strategies are considered: the retention strategy in
which all variable bindings are retained until no longer needed
(implying the use of some sort of garbage-collected store) and the
deletion strategy, modeled after the usual stack implementation of
ALGOL 60, in which variable bindings are destroyed when control leaves
the procedure (or block) in which they were created. Not all lambda
abstractions evaluate correctly under the deletion
strategy. Nevertheless, both strategies are equally powerful in the
sense that any lambda abstraction can be mechanically translated into
another that evaluates correctly under the deletion strategy and
defines the same partial function over the domain of interpretation as
the original. Proof is by translation into continuation-passing
style. Keywords: lambda calculus, LISP, continuation-passing style, closures, functional objects, retention strategy, deletion strategy, bindings, stack |
[local copy]