Adding Algebraic Rewriting to the Untyped Lambda Calculus. Dougherty, D. J.\ Information and Computation, 101(2):251--267, 1992.
Adding Algebraic Rewriting to the Untyped Lambda Calculus [pdf]Paper  abstract   bibtex   
We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from $R$ as constants. On certain classes of terms, called here \emphstable, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

Downloads: 0