BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-90-1337
       ENTRY:: September 14, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A simplifier for untyped lambda expressions
        TYPE:: Technical Report
      AUTHOR:: Galbiati, Louis
      AUTHOR:: Talcott, Carolyn
        DATE:: October 1990
       PAGES:: 29
    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.
       NOTES:: [Adminitrivia V1/RAM/19940914]
         END:: STAN//CS-TR-90-1337