kirancodes.me
To Proof Maintenance & Beyond!

Transformations and Reduction Strategies for Typed Lambda Expressions

Michael P. Georgeff

Abstract

A scheme is described that allows languages supporting higher order functions to be efficiently implemented using a standard run-time stack.A machine for evaluating typed lambda expressions is first constructed.In essence, the machine simply extends the standard SECD machine to allow partial application of abstractions representing multiadic functions.Some transformations of these typed lambda expressions into a so-called simple form are then described.Evaluation of simple-form expressions on the extended SECD machine produces stacklike environment structures rather than the treelike structures produced by expressions of arbitrary form.This allows implementation of the machine using a standard runtime stack.The SECD machine is then further modified so that closures are applied "in situ" rather than returned as values.The order of reduction is also changed so that the evaluation of function-valued expressions is deferred until they can be applied to sufficient arguments to allow reduction to nonfunctional values.It is shown that this function-deferring machine can be implemented using a standard run-time stack and thus can evaluate arbitrary lambda expressions without prior transformation to simple form.Finally, application of the above schemes to standard programming languages, such as ALGOL, Pascal, Ada, and LISP, is considered.

Related papers