Term Rewriting in CT-Sigma

We extend the classical theory of term rewriting systems to infinite and partial terms (i.e., to the elements of algebra CT ∑ ), fully exploiting the complete partially ordered structure of CT ∑ . We show that redexes and rules, as well as other operations on terms, can be regarded as total functions on CT ∑ . As a consequence, we can study their properties of monotonicity and continuity. For rules, we show that nonleft-linear rules are in general not. monotonic, and that left-infinite rules are in general not continuous. Moreover, we show that the well-known Church-Rosser property of non-overlapping redexes holds for monotonic redexes. This property allows us to define a notion of parallel application of a finite set of monotonie redexes, and, using standard algebraic techniques, we extend the definition to the infinite case. We also suggest that infinite parallel term rewriting has interesting potential applications in the semantics of cyclic term, graph rewriting.