Infinitary Combinatory Reduction Systems

TY - JOUR

T1 - Infinitary Combinatory Reduction Systems

AU - Ketema, Jeroen

AU - Simonsen, Jakob Grue

PY - 2011/6

Y1 - 2011/6

N2 - 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 known results from first-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 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.

AB - 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 known results from first-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 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.

U2 - 10.1016/j.ic.2011.01.007

DO - 10.1016/j.ic.2011.01.007

M3 - Journal article

SN - 0890-5401

VL - 209

SP - 893

EP - 926

JO - Information and Computation

JF - Information and Computation

IS - 6

ER -