The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity)

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity). / Simonsen, Jakob Grue.

Rewriting Techniques and Applications: 20th International Conference, RTA 2009. Vol. 5595 Springer, 2009. p. 335-349 (Lecture notes in computer science, Vol. 5595).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Simonsen, JG 2009, The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity). in Rewriting Techniques and Applications: 20th International Conference, RTA 2009. vol. 5595, Springer, Lecture notes in computer science, vol. 5595, pp. 335-349, Rewriting Techniques and Applications, Brasilia, Brazil, 29/06/2009. https://doi.org/10.1007/978-3-642-02348-4_24

APA

Simonsen, J. G. (2009). The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity). In Rewriting Techniques and Applications: 20th International Conference, RTA 2009 (Vol. 5595, pp. 335-349). Springer. Lecture notes in computer science Vol. 5595 https://doi.org/10.1007/978-3-642-02348-4_24

Vancouver

Simonsen JG. The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity). In Rewriting Techniques and Applications: 20th International Conference, RTA 2009. Vol. 5595. Springer. 2009. p. 335-349. (Lecture notes in computer science, Vol. 5595). https://doi.org/10.1007/978-3-642-02348-4_24

Author

Simonsen, Jakob Grue. / The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity). Rewriting Techniques and Applications: 20th International Conference, RTA 2009. Vol. 5595 Springer, 2009. pp. 335-349 (Lecture notes in computer science, Vol. 5595).

Bibtex

@inproceedings{b0ee72d0e65111deba73000ea68e967b,
title = "The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity)",
abstract = "Most of the standard pleasant properties of term rewriting systems are undecidable; to wit: local confluence, confluence, normalization, termination, and completeness.Mere undecidability is insufficient to rule out a number of possibly useful properties: For instance, if the set of normalizing term rewriting systems were recursively enumerable, there would be a program yielding “yes” in finite time if applied to any normalizing term rewriting system.The contribution of this paper is to show (the uniform version of) each member of the list of properties above (as well as the property of being a productive specification of a stream) complete for the class $\Pi^0_2$. Thus, there is neither a program that can enumerate the set of rewriting systems enjoying any one of the properties, nor is there a program enumerating the set of systems that do not.For normalization and termination we show both the ordinary version and the ground versions (where rules may contain variables, but only ground terms may be rewritten) $\Pi^0_2$-complete. For local confluence, confluence and completeness, we show the ground versions $\Pi^0_2$-complete.",
author = "Simonsen, {Jakob Grue}",
year = "2009",
doi = "10.1007/978-3-642-02348-4_24",
language = "English",
isbn = "978-3-642-02347-7",
volume = "5595",
series = "Lecture notes in computer science",
publisher = "Springer",
pages = "335--349",
booktitle = "Rewriting Techniques and Applications",
address = "Switzerland",
note = "null ; Conference date: 29-06-2009 Through 01-07-2009",

}

RIS

TY - GEN

T1 - The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity)

AU - Simonsen, Jakob Grue

N1 - Conference code: 20

PY - 2009

Y1 - 2009

N2 - Most of the standard pleasant properties of term rewriting systems are undecidable; to wit: local confluence, confluence, normalization, termination, and completeness.Mere undecidability is insufficient to rule out a number of possibly useful properties: For instance, if the set of normalizing term rewriting systems were recursively enumerable, there would be a program yielding “yes” in finite time if applied to any normalizing term rewriting system.The contribution of this paper is to show (the uniform version of) each member of the list of properties above (as well as the property of being a productive specification of a stream) complete for the class $\Pi^0_2$. Thus, there is neither a program that can enumerate the set of rewriting systems enjoying any one of the properties, nor is there a program enumerating the set of systems that do not.For normalization and termination we show both the ordinary version and the ground versions (where rules may contain variables, but only ground terms may be rewritten) $\Pi^0_2$-complete. For local confluence, confluence and completeness, we show the ground versions $\Pi^0_2$-complete.

AB - Most of the standard pleasant properties of term rewriting systems are undecidable; to wit: local confluence, confluence, normalization, termination, and completeness.Mere undecidability is insufficient to rule out a number of possibly useful properties: For instance, if the set of normalizing term rewriting systems were recursively enumerable, there would be a program yielding “yes” in finite time if applied to any normalizing term rewriting system.The contribution of this paper is to show (the uniform version of) each member of the list of properties above (as well as the property of being a productive specification of a stream) complete for the class $\Pi^0_2$. Thus, there is neither a program that can enumerate the set of rewriting systems enjoying any one of the properties, nor is there a program enumerating the set of systems that do not.For normalization and termination we show both the ordinary version and the ground versions (where rules may contain variables, but only ground terms may be rewritten) $\Pi^0_2$-complete. For local confluence, confluence and completeness, we show the ground versions $\Pi^0_2$-complete.

U2 - 10.1007/978-3-642-02348-4_24

DO - 10.1007/978-3-642-02348-4_24

M3 - Article in proceedings

SN - 978-3-642-02347-7

VL - 5595

T3 - Lecture notes in computer science

SP - 335

EP - 349

BT - Rewriting Techniques and Applications

PB - Springer

Y2 - 29 June 2009 through 1 July 2009

ER -

ID: 16239368