Undecidable properties of flat term rewrite systems. (English) Zbl 1187.68274
Reachability, joinability, termination or strong normalization, confluence, weak normalization, and unique normalization are some fundamental properties of term rewrite systems (TRS) that are known to be undecidable in general. Their decidablity has been investigated for some particular classes. In this paper, the authors give new simple proofs for the undecidability of reachability, joinability, and confluence for flat TRS. They also give proofs for the undecidability of weak and unique normalizations for flat TRS.
Reviewer: Francine Blanchet-Sadri (Greensboro)
MSC:
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, New York (1998) · Zbl 0948.68098 |
| [2] | Godoy, G., Huntingford, E., Tiwari, A.: Termination of rewriting with right-flat rules. In: Baader, F. (ed.) Term Rewriting and Applications, 18th International Conference, RTA, LNCS, vol. 4533, pp. 200–213. Springer, Heidelberg (2007) · Zbl 1203.68074 |
| [3] | Godoy, G., Tison, S.: On the normalization and unique normalization properties of term rewrite systems. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction (CADE-21), LNCS, vol. 4603, pp. 247–262 (2007) · Zbl 1213.68348 |
| [4] | Godoy, G., Tiwari, A.: Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure. In: Basin, D., Rusinowitch, M. (eds.) International Joint Conference on Automated Deduction, IJCAR, LNAI, vol. 3097, pp. 91–106. Springer, Heidelberg (2004) · Zbl 1126.68566 |
| [5] | Godoy, G., Tiwari, A.: Confluence of shallow right-linear rewrite systems. In: Ong, C.H.L. (ed.) 19th International Workshop of Computer Science Logic, CSL, LNCS, vol. 3634, pp. 541–556. Springer, Heidelberg (2005) · Zbl 1136.68411 |
| [6] | Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) 20th International Symposium on Theoretical Aspects of Computer Science STACS 2003, Lecture Notes in Computer Science, vol. 2607, pp. 85–96. Springer, Heidelberg (2003) · Zbl 1035.68058 |
| [7] | Jacquemard F.: Reachability and confluence are undecidable for flat term rewriting systems. Inf. Process. Lett. 87(5), 265–270 (2003) · Zbl 1161.68502 · doi:10.1016/S0020-0190(03)00310-7 |
| [8] | Mitsuhashi, I., Oyamaguchi, M., Jacquemard, F.: The confluence problem for flat TRSs. In: Proceedings of 8th International Conference on Artificial Intelligence and Symbolic Computation (AISC’06), LNAI, vol. 4120, pp. 68–81. Springer, Heidelberg (2006) · Zbl 1156.68433 |
| [9] | Nagaya T., Toyama Y.: Decidability for left-linear growing term rewriting systems. Inf. Comput. 178(2), 499–514 (2002) · Zbl 1049.68075 · doi:10.1006/inco.2002.3157 |
| [10] | Sipser, M.: Introduction to the Theory of Computation. Course Technology (2006) · Zbl 1191.68311 |
| [11] | Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Rewriting Techniques and Applications, RTA, LNCS, vol. 1833, pp. 246–260 (2000) · Zbl 0964.68073 |
| [12] | Verma R., Hayrapetyan A.: A new decidability technique for ground term rewriting systems. ACM Trans. Comput. Log. 6(1), 102–123 (2005) · doi:10.1145/1042038.1042042 |
| [13] | Wang, Y., Sakai, M.: Decidability of termination for semi-constructor trss, left-linear shallow trss and related systems. In: Proceedings of the 17th International Conference of RTA, LNCS, vol. 4098, pp. 343–356. Springer, Heidelberg (2006) · Zbl 1151.68455 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
