Abstract
Term rewriting for rational terms, i.e. infinite terms with a finite number of different subterms, has been considered e.g. in Corradini & Gadducci (1998) and Aoto & Ketema (2012). In this paper, we consider rational term rewriting by a set of commutativity rules i.e. rules of the form \(f(x,y) \rightarrow f(y,x)\), based on the framework of Aoto & Ketema (2012). A rewrite step with a commutativity rule is specified via a regular set of redex positions, thus via a finite automaton. We present some finite automata constructions that correspond to (in particular) taking inverse rewrite steps, merging two branching rewrite steps, and merging two consecutive rewrite steps. As a corollary, we show that rational rewrite steps by the commutativity rules are closed under taking equivalence of the rewrite steps.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To ease the readability, however, we omit below the equation \(x_\bot = \bot (x_\bot ,\ldots ,x_\bot )\) if the equation is not necessary, i.e. if there is no equation in E such that its right hand side is a variable or all \(f \in \mathcal {F}\) originally have the same arity.
References
Aoto, T., Ketema, J.: Rational term rewriting revisited: decidability and confluence. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 172–186. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33654-6_12
Ariola, Z.M., Klop, J.W.: Equational term graph rewriting. Fundam. Informaticae 26, 207–240 (1996)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning vol. 1, pp. 445–533. Elsevier (2001)
Corradini, A.: Term rewriting in \({CT}_{\Sigma }\). In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 468–484. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56610-4_83
Corradini, A., Gadducci, F.: Rational term rewriting. In: Nivat, M. (ed.) FoSSaCS 1998. LNCS, vol. 1378, pp. 156–171. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053548
Courcelle, B.: Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95–169 (1983)
Inverardi, P., Zilli, M.V.: Rational rewriting. In: Prívara, I., Rovan, B., Ruzička, P. (eds.) MFCS 1994. LNCS, vol. 841, pp. 433–442. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58338-6_90
Kozen, D.C.: Automata and Computability. Springer, New York (1997)
Plump, D.: Term graph rewriting. In: Handbook of Graph Grammars and Computing by Graph Transformation Volume 2: Applications, Languages and Tools, pp. 3–61. World Scientific (1999)
Terese (ed.): Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Acknowledgement
Thanks are due to anonymous referees and Akihisa Yamada for helpful comments. This work was partially supported by a grant from JSPS No. 18K11158.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Ishizuka, M., Aoto, T., Iwami, M. (2021). Commutative Rational Term Rewriting. In: Leporati, A., Martín-Vide, C., Shapira, D., Zandron, C. (eds) Language and Automata Theory and Applications. LATA 2021. Lecture Notes in Computer Science(), vol 12638. Springer, Cham. https://doi.org/10.1007/978-3-030-68195-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-68195-1_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-68194-4
Online ISBN: 978-3-030-68195-1
eBook Packages: Computer ScienceComputer Science (R0)