Infinitary Combinatory Reduction Systems

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

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

I: Information and Computation, Bind 209, Nr. 6, 2011, s. 893-926.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Ketema, J & Simonsen, JG 2011, 'Infinitary Combinatory Reduction Systems', Information and Computation, bind 209, nr. 6, s. 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. I: Information and Computation. 2011 ; Bind 209, Nr. 6. s. 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