A Simplifier for Untyped Lambda Expressions,

Abstract

Many applicative programming languages are based on the call-by-value lambda calculus. For these languages tools such as compilers, partial evaluations, 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1990
Accession Number
ADA326084

Entities

People

  • Carolyn Talcott
  • Louis Galbiati

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automatic
  • Calculus
  • Classification
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Confluence
  • Guarantees
  • Language
  • Programming Languages
  • Sequences
  • Standards
  • Test And Evaluation

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design