Adding algebraic rewriting to the untyped lambda calculus (extended abstract)

Abstract

We investigate the system obtained by adding an algebraic rewriting system R to the untyped lambda calculus. On certain classes of terms, called here “stable”, 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 yields a general method for proving confluence of typed β reduction plus rewriting; we sketch the application to the polymorphic calculus Fω.