Adding algebraic rewriting to the untyped lambda calculus

AbstractWe 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 “stable,” we prove that the resulting calculus is confluent if R is confluent, and is 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 β-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus