Title
Adding algebraic rewriting to the untyped lambda calculus
Abstract
We investigate the system obtained by adding an algebraic rewriting system R toan untyped lambda calculus in which terms are formed using the function symbols fromR as constants. On certain classes of terms, called here "stable", we prove that theresulting calculus is confluent if R is confluent, and terminating if R is terminating. Thetermination result has the corresponding theorems for several typed calculi as corollaries.The proof of the confluence result suggests a general method ...
Year
DOI
Venue
1992
10.1016/0890-5401(92)90064-M
Information & Computation
Keywords
DocType
Volume
untyped lambda calculus,lambda calculus
Journal
101
Issue
ISSN
Citations 
2
Information and Computation
37
PageRank 
References 
Authors
2.31
5
1
Name
Order
Citations
PageRank
Daniel J. Dougherty141332.13