Report Number: CS-TR-90-1337
Institution: Stanford University, Department of Computer Science
Title: A simplifier for untyped lambda expressions
Author: Galbiati, Louis
Author: Talcott, Carolyn
Date: October 1990
Abstract: Many applicative programming languages are based on the
call-by-value lambda calculus. For these languages tools such
as compilers, partial evaluators, and other transformation
systems often make use of rewriting systems that incorporate
some form of beta reduction. For purposes of automatic
rewriting it is important to develop extensions of beta-value
reduction and to develop methods for guaranteeing
termination. This paper describes an extension of beta-value
reduction and a method based on abstract interpretation for
controlling rewriting to guarantee termination. The main
innovations are (1) the use of rearrangement rules in
combination with beta-value reduction to increase the power
of the rewriting system and (2) the definition of a
non-standard interpretation of expressions, the generates
relation, as a basis for designing terminating strategies for
rewriting.
http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1337/CS-TR-90-1337.pdf