×

A logical analysis on theory of conditional rewriting. (English) Zbl 0667.68106

Conditional term rewriting systems, 1st. int. Workshop, Orsay/France 1987, Lect. Notes Comput.Sci. 308, 179-196 (1988).
[For the entire collection see Zbl 0639.00039.]
Logical relations between systems of the form \(s_ i=t_ i\Rightarrow \ell =r\), \(s_ i\downarrow t_ i\Rightarrow \ell \to r\) (standard: \(s\downarrow t\) means that E u(s\(\to^{*}u \& u\leftarrow^{*}t)\), where \(s\to^{*}t\) is a many-step reduction), \(s_ i=^{*}t_ i\Rightarrow \ell \to r\) (natural; \(s=^{*}t\) means E \(u_ 1,...,u_ n\) such that \(s\downarrow u_ 1\downarrow...\downarrow u_ n\downarrow t)\), are analyzed. It is shown how, having a normal system R, (of the form \(s_ i\downarrow N_ i\Rightarrow \ell \to r\), where \(N_ i\) is in normal form), to construct a non-normal system \(R^*\), such that \(R\vdash s\downarrow t\) implies R*\(\vdash s\downarrow t.\)
It is shown that the expressive power of normal systems is the same as of general systems and for terminating systems R and R* are logically equivalent. A class of decreasing systems is introduced and it is shown that such systems are terminating, their basic notions are decidable, joinability of critical pairs guarantees confluency. Both the simplification systems of Kaplan and reductive systems of Jouannaud- Waldmann are subclasses of decreasing systems.
Full normalization and strong Church-Rosser property are introduced (both as generalizations from the unconditional case). It is shown that any equational proof in a natural conditional system which is overlay (critical pairs are obtained by unifying at the roots only) is fully normalizable, therefore having the strong Church-Rosser property.
For decreasing systems the joinability has the same consequence.
Reviewer: T.Tammet

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations

Citations:

Zbl 0639.00039