Infinitary Combinatory Reduction Systems

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfæ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.
OriginalsprogEngelsk
TidsskriftInformation and Computation
Vol/bind209
Udgave nummer6
Sider (fra-til)893-926
Antal sider34
ISSN0890-5401
DOI
StatusUdgivet - 2011

ID: 37440995