The Pi-0-2-Completeness of most of the Properties of Rewriting You Care About (and Productivity)
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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. Bind 5595 Springer, 2009. s. 335-349 (Lecture notes in computer science, Bind 5595).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
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