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. Dougherty | 1 | 413 | 32.13 |