Infinitary rewriting: closure operators, equivalences and models (Q2376981)

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 \textit{N. Dershowitz} et al. [Theor. Comput. Sci. 83, No. 1, 71--96 (1991; Zbl 0759.68044)] and the strongly continuous reductions of \textit{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.