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.
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.
| Original language | English |
|---|---|
| Title of host publication | Rewriting Techniques and Applications : 20th International Conference, RTA 2009 |
| Number of pages | 15 |
| Volume | 5595 |
| Publisher | Springer |
| Publication date | 2009 |
| Pages | 335-349 |
| ISBN (Print) | 978-3-642-02347-7 |
| DOIs | |
| Publication status | Published - 2009 |
| Event | Rewriting Techniques and Applications - Brasilia, Brazil Duration: 29 Jun 2009 → 1 Jul 2009 Conference number: 20 |
Conference
| Conference | Rewriting Techniques and Applications |
|---|---|
| Number | 20 |
| Country/Territory | Brazil |
| City | Brasilia |
| Period | 29/06/2009 → 01/07/2009 |
| Series | Lecture notes in computer science |
|---|---|
| Volume | 5595 |
| ISSN | 0302-9743 |