Kahrs, Stefan Infinitary rewriting: closure operators, equivalences and models. (English) Zbl 1294.68098 Acta Inf. 50, No. 2, 123-156 (2013). Infinitary rewriting is concerned with infinite terms and transfinite reduction sequences. Infinite terms are obtained by metric completion using some metric on terms, and the definitions of infinite reduction sequences also involve forming limits in such metric spaces. However, it is not always clear how a concept should be defined for infinitary rewriting systems. This paper is an extensive and detailed study of some of such problematic notions. Proposing a new general way to view them, the author also suggests several alternative definitions. The starting point of his approach is the observation that the reduction and equivalence relations defined by a usual term rewriting system are obtained by applying certain closure operators to the set of reduction rules. He shows that in the case of infinitary rewriting the convergent reductions of N. Dershowitz et al. [Theor. Comput. Sci. 83, No. 1, 71–96 (1991; Zbl 0759.68044)] and the strongly continuous reductions of R. Kennaway et al. [Inf. Comput. 119, No. 1, 18–38 (1995; Zbl 0832.68063)] can also be defined this way. Moreover, he introduces several alternative notions of convergence and equivalence for infinitary rewriting systems. Some of these are obtained working on the more abstract level of topology. Furthermore, the author also introduces equational models for possibly infinite terms. All the concepts are carefully analyzed and compared with each other. Reviewer: Magnus Steinby (Turku) Cited in 1 Document MSC: 68Q42 Grammars and rewriting systems 54E35 Metric spaces, metrizability 08A70 Applications of universal algebra in computer science Keywords:term rewriting systems; infinitary rewriting; infinite terms; reduction sequences; metric completion; topological spaces; equational models Citations:Zbl 0759.68044; Zbl 0832.68063 PDFBibTeX XMLCite \textit{S. Kahrs}, Acta Inf. 50, No. 2, 123--156 (2013; Zbl 1294.68098) Full Text: DOI References: [1] Arnold, A., Nivat, M.: Metric interpretations of infinite trees and semantics of nondeterministic recursive programs. Theor. Comput. Sci. 11(2), 181–205 (1980) · Zbl 0427.68022 [2] Bahr, P.: Partial order infinitary term rewriting and Böhm Trees. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 67–84. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2010) doi: 10.4230/LIPIcs.RTA.2010.67 . http://drops.dagstuhl.de/opus/volltexte/2010/2645 · Zbl 1236.68122 [3] Barendregt, H., Klop, J.W.: Applications of infinitary lambda calculus. Inf. Comput. 207(5), 559–582 (2009). doi: 10.1016/j.ic.2008.09.003 · Zbl 1167.03010 [4] Barendregt, H.P.: The Lambda-Calculus, Its Syntax and Semantics. North-Holland, Amsterdam (1984) · Zbl 0551.03007 [5] Barr, M.: Terminal coalgebras in well-founded set theory. Theor. Comput. Sci. 114, 299–315 (1993) · Zbl 0779.18004 [6] Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990) · Zbl 0701.06001 [7] Dershowitz, N., Kaplan, S.: Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, $$\(\backslash\)ldots $$ . In: Principles of Programming Languages, pp. 250–259. ACM press (1989) [8] Dershowitz, N., Kaplan, S., Plaisted, D.: Rewrite, Rewrite, Rewrite, $$\(\backslash\)ldots $$ . Theor. Comput. Sci. 83(1), 71–96 (1991) [9] Endrullis, J., Grabmayer, C., Hendriks, D., Klop, J.W., Vrijer, R.: Proving infinitary normalization. In: Types for Proofs and Programs: International Conference, TYPES 2008 Torino, Italy, March 26–29, 2008 Revised Selected Papers, pp. 64–82. Springer, Berlin (2009) · Zbl 1246.68135 [10] Fox, R.: On topologies for function spaces. Bull. Am. Math. Soc. 51, 429–432 (1945) · Zbl 0060.41202 [11] Gamelin, T.W., Greene, R.E.: Introduction to Topology. Dover Mineola, New York (1999) · Zbl 0935.54001 [12] Hahn, H.: Reelle Funktionen. Chelsea Publishing Company, New York (1948) · JFM 58.0242.05 [13] Hajnal, A., Hamburger, P.: Set Theory. London Mathematical Society, London (1999) · Zbl 0934.03057 [14] Isihara, A.: Algorithmic Term Rewriting Systems. Ph.D. thesis, Vrije Universiteit Amsterdam (2010) [15] Jänich, K.: Topology. Springer, Berlin (1984) [16] Kahrs, S.: Infinitary rewriting: Meta-theory and convergence. Acta Informatica 44(2), 91–121 (2007) · Zbl 1120.68062 [17] Kahrs, S.: Modularity of convergence in infinitary rewriting. In: Treinen, R. (ed.) Rewriting Techniques and Applications, LNCS, vol. 5595, pp. 179–193. Springer, Berlin (2009) · Zbl 1242.68134 [18] Kahrs, S.: Infinitary rewriting: Foundations revisited. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 161–176. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2010). doi: 10.4230/LIPIcs.RTA.2010.161 . http://drops.dagstuhl.de/opus/volltexte/2010/2651 · Zbl 1236.68132 [19] Kahrs, S.: Modularity of convergence and strong convergence in infinitary rewriting. Log. Methods Comput Sci 6(3), 27 (2010) · Zbl 1214.68187 [20] Kennaway, R., Klop, J.W., Sleep, R., de Vries, F.J.: Transfinite reductions in orthogonal term rewriting systems. Inf. Comput. 119(1), 18–38 (1995) · Zbl 0832.68063 [21] Kennaway, R., van Oostrom, V., de Vries, F.J.: Meaningless terms in rewriting. J. Funct. Log. Program. 1, 1–35 (1999) · Zbl 0924.68107 [22] Kennaway, R., de Vries, F.J.: Term Rewriting Systems, chap. Infinitary Rewriting. Cambridge University Press (2003) [23] Ketema, J.: Böhm-Like Rrees for Rewriting. Ph.D. thesis, Vrije Universiteit Amsterdam (2006) [24] Ketema, J.: Comparing Böhm-like trees. In: Treinen, R. (ed.) RTA, Lecture Notes in Computer Science, vol. 5595, pp. 239–254. Springer, Berlin (2009) · Zbl 1242.68135 [25] Kuratowski, K.: Topology. Academic Press, New York (1966) [26] Lüth, C.: Compositional term rewriting: An algebraic proof of Toyama’s Theorem. In: Rewriting Techniques and Applications, pp. 261–275 (1996). LNCS 1103 [27] MacLane, S.: Categories for the Working Mathematician. Springer, Berlin (1971) · Zbl 0705.18001 [28] Meinke, K., Tucker, J.: Universal algebra. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 1, pp. 189–411. Oxford University Press, Oxford (1992) [29] Potter, M.D.: Sets: An Introduction. Oxford University Press, Oxford (1990) · Zbl 0746.04001 [30] Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Springer, Berlin (2012) · Zbl 1237.68129 [31] Simonsen, J.G.: Weak convergence and uniform normalization in infinitary rewriting. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 311–324. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2010). doi: 10.4230/LIPIcs.RTA.2010.311 . http://drops.dagstuhl.de/opus/volltexte/2010/2660 · Zbl 1236.68150 [32] Smyth, M.: Topology. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 1, pp. 641–762. Oxford University Press, Oxford (1992) [33] Steen, L.A., Seebach, J.A.: Counterexamples in Topology. Dover, New York (1995) · Zbl 1245.54001 [34] Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, chap. 4, pp. 133–191. Elsevier, Amsterdam (1990) · Zbl 0900.68316 [35] Urysohn, P.: Zum metrizations problem. Math. Ann. 94, 309–315 (1925) · JFM 51.0453.01 [36] Zantema, H.: Normalisation of infinite terms. In: RTA 2008, LNCS, vol. 5117, pp. 441–455. Springer, Berlin (2008) · Zbl 1146.68042 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.