Modular properties of conditional term rewriting systems
type: Item
instance of: scholarly article
title: Modular properties of conditional term rewriting systems
zbMATH Open document ID: 0804.68071
author: Aart Middeldorp
published in: Information and Computation
publication date: 1994-09-06T00:00:00Z
full work available at URL: https://ir.cwi.nl/pub/5607
review text: 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.
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 439989
zbMATH Keywords: conditional term rewriting
zbMATH Keywords: modularity
zbMATH Keywords: confluence
zbMATH Keywords: normalization
MaRDI profile type: Publication
OpenAlex ID: W2061404638
DOI: 10.1006/INCO.1993.1027
Recommended article: Modular properties of composable term rewriting systems
Recommended article: Q4537514
Recommended article: Sufficient conditions for modular termination of conditional term rewriting systems
Recommended article: Modularity in term rewriting revisited
Recommended article: Modular aspects of properties of term rewriting systems related to normal forms
Recommended article: Modular term rewriting systems and the termination
Recommended article: On the modularity of termination of term rewriting systems
Recommended article: On modularity in term rewriting and narrowing
Recommended article: Determinization of conditional term rewriting systems
Recommended article: Generalized sufficient conditions for modular termination of rewriting
description: scientific article; zbMATH DE number 439989