Name
Abstract | ||
|---|---|---|
We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary @l-calculus are special cases. Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary @l-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes U has a complete development, then all complete developments of U end in the same term and that (2) any tiling diagram involving strongly convergent reductions S and T can be completed iff at least one of S/T and T/S is strongly convergent. We also prove an ancillary result of independent interest: a set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1016/j.ic.2011.01.007 | Information & Computation |
Keywords | Field | DocType |
higher-order term rewriting,complete development iff,u end,combinatory reduction systems,infinitary rewriting,complete development,convergent reduction,ordinary infinitary term,infinitary higher-order,infinitary combinatory reduction systems,left-linear icrss,first-order infinitary,orthogonal icrss,higher order | Discrete mathematics,Computer science,Algorithm,Confluence,Rewriting | Journal |
Volume | Issue | ISSN |
209 | 6 | Information and Computation |
Citations | PageRank | References |
14 | 0.73 | 24 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeroen Ketema | 1 | 160 | 13.52 |
| Jakob Grue Simonsen | 2 | 317 | 44.16 |