Name
Abstract | ||
|---|---|---|
We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fully-extended, orthogonal iCRSs are confluent modulo identification of hypercollapsing sub-terms. As a corollary, we obtain that fully-extended, orthogonal iCRSs have the normal form property and the unique normal form property (with respect to reduction). We also show that, unlike the case in first-order infinitary rewriting, almost non-collapsing iCRSs are not necessarily confluent. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.2168/LMCS-5(4:3)2009 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
term rewriting,higher-order computation,combinatory reduction systems,lambda-calculus,infinite computation,confluence,normal forms | Discrete mathematics,Modulo,Confluence,Rewriting,Corollary,Mathematics | Journal |
Volume | Issue | ISSN |
5 | 4 | 1860-5974 |
Citations | PageRank | References |
7 | 0.55 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeroen Ketema | 1 | 160 | 13.52 |
| Jakob Grue Simonsen | 2 | 317 | 44.16 |
| Henk Barendregt | 3 | 588 | 92.49 |