Modular properties of conditional term rewriting systems (Q689098)

Rewriting techniques arise in the specification of abstract data types. Integrating functional and logical programming ideas therein requires the study of confluence and normalization for conditional rewriting systems. The author presents his results of the last years published in several reports and conference proceedings. \textit{Y. Toyama} proved 1987 [J. ACM 34, No. 1, 128-143] that confluence is a modular property of term rewriting systems (TRS). This means that the disjoint union of two confluent TRS is confluent too. The author extends this result to conditional TRS (CTRS). More precisely, he shows that the modularity of the confluence holds for join and semi-equational CTRS. (Part of this material was already presented at the CTRS Workshop in Montreal 1990 [in: Lect. Notes Comput. Sci. 516, 295-306 (1991)].) For other properties of TRS the situation is much more complicated. It is shown that local confluence is not modular for CTRS, whereas it is so for TRS. Since for strongly normalizing TRS (all reductions ends in a normal form) from its locally confluence follows the confluence, it is interesting to know what happens with the (strong) normalization properties. In the paper it is shown that strong normalization is a modular property of join CTRS without collapsing rules. This result extends an already known result for TSR. For join CTRS's without duplicating rules the extention of the corresponding TSR result is proved only for confluent CTRS's. Without going into the details we note that the results given for semi- equational CTRS's are similar. The paper finishes with the proof that the existence of a unique normal form is also a modular property of semi-equational CTRS, generalizing the TRS property. The same question for join CTRS remains open.