Infinitary Combinatory Reduction Systems
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
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 ¿-calculus are special cases. Furthermore,we generalise a number of knownresults fromfirst-order infinitary rewriting and infinitary ¿-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 anancillary 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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Information and Computation |
Vol/bind | 209 |
Udgave nummer | 6 |
Sider (fra-til) | 893-926 |
Antal sider | 34 |
ISSN | 0890-5401 |
DOI | |
Status | Udgivet - 2011 |
ID: 37440995