Infinitary Combinatory Reduction Systems

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Infinitary Combinatory Reduction Systems. / Ketema, Jeroen; Simonsen, Jakob Grue.

In: Information and Computation, Vol. 209, No. 6, 2011, p. 893-926.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Ketema, J & Simonsen, JG 2011, 'Infinitary Combinatory Reduction Systems', Information and Computation, vol. 209, no. 6, pp. 893-926. https://doi.org/10.1016/j.ic.2011.01.007

APA

Ketema, J., & Simonsen, J. G. (2011). Infinitary Combinatory Reduction Systems. Information and Computation, 209(6), 893-926. https://doi.org/10.1016/j.ic.2011.01.007

Vancouver

Ketema J, Simonsen JG. Infinitary Combinatory Reduction Systems. Information and Computation. 2011;209(6):893-926. https://doi.org/10.1016/j.ic.2011.01.007

Author

Ketema, Jeroen ; Simonsen, Jakob Grue. / Infinitary Combinatory Reduction Systems. In: Information and Computation. 2011 ; Vol. 209, No. 6. pp. 893-926.

Bibtex

@article{9b60b56387e04d80aad04e8bc4f14df7,
title = "Infinitary Combinatory Reduction Systems",
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 ¿-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.",
author = "Jeroen Ketema and Simonsen, {Jakob Grue}",
year = "2011",
doi = "10.1016/j.ic.2011.01.007",
language = "English",
volume = "209",
pages = "893--926",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Academic Press",
number = "6",

}

RIS

TY - JOUR

T1 - Infinitary Combinatory Reduction Systems

AU - Ketema, Jeroen

AU - Simonsen, Jakob Grue

PY - 2011

Y1 - 2011

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 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.

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 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.

U2 - 10.1016/j.ic.2011.01.007

DO - 10.1016/j.ic.2011.01.007

M3 - Journal article

VL - 209

SP - 893

EP - 926

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 6

ER -

ID: 37440995