TY - CHAP

T1 - Reduction strategies for left-linear term rewriting systems

AU - Toyama, Yoshihito

PY - 2005/1/1

Y1 - 2005/1/1

N2 - Huet and Lévy (1979) showed that needed reduction is a normalizing strategy for orthogonal (i.e., left-linear and non-overlapping) term rewriting systems. In order to obtain a decidable needed reduction strategy, they proposed the notion of strongly sequential approximation. Extending their seminal work, several better decidable approximations of left-linear term rewriting systems, for example, NV approximation, shallow approximation, growing approximation, etc., have been investigated in the literature. In all of these works, orthogonality is required to guarantee approximated decidable needed reductions are actually normalizing strategies. This paper extends these decidable normalizing strategies to left-linear overlapping term rewriting systems. The key idea is the balanced weak Church-Rosser property. We prove that approximated external reduction is a computable normalizing strategy for the class of left-linear term rewriting systems in which every critical pair can be joined with root balanced reductions. This class includes all weakly orthogonal left-normal systems, for example, combinatory logic CL with the overlapping rules pred ·(succ · x) → x and succ · (pred · x) → x, for which leftmost-outermost reduction is a computable normalizing strategy.

AB - Huet and Lévy (1979) showed that needed reduction is a normalizing strategy for orthogonal (i.e., left-linear and non-overlapping) term rewriting systems. In order to obtain a decidable needed reduction strategy, they proposed the notion of strongly sequential approximation. Extending their seminal work, several better decidable approximations of left-linear term rewriting systems, for example, NV approximation, shallow approximation, growing approximation, etc., have been investigated in the literature. In all of these works, orthogonality is required to guarantee approximated decidable needed reductions are actually normalizing strategies. This paper extends these decidable normalizing strategies to left-linear overlapping term rewriting systems. The key idea is the balanced weak Church-Rosser property. We prove that approximated external reduction is a computable normalizing strategy for the class of left-linear term rewriting systems in which every critical pair can be joined with root balanced reductions. This class includes all weakly orthogonal left-normal systems, for example, combinatory logic CL with the overlapping rules pred ·(succ · x) → x and succ · (pred · x) → x, for which leftmost-outermost reduction is a computable normalizing strategy.

UR - http://www.scopus.com/inward/record.url?scp=37149054694&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=37149054694&partnerID=8YFLogxK

U2 - 10.1007/11601548_13

DO - 10.1007/11601548_13

M3 - Chapter

AN - SCOPUS:37149054694

SN - 354030911X

SN - 9783540309116

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 198

EP - 223

BT - Processes, Terms and Cycles

PB - Springer Verlag

ER -