Conditional rewrite rules: Confluence and termination (Q1111368): Difference between revisions

The authors consider conditional rewrite rules: \[ \bigwedge^{n}_{i=0}(t_ i\@s_ i)\quad \Rightarrow \quad (t\to s)\quad,\quad where\quad \@\in (=,|,\to \to \}\quad, \] and four corresponding term rewriting systems (TRS); 0 for \(n=0,\) I for \(n=0\) and \(\@\) is \(=,\) II for \(n=0\) and \(\@\) is \(|\), and III for \(n=0\) and \(\@\) is \(\to \to;\) also the particular case \(III_ n\) when s are normal closed forms (they contain neither variables nor rules). \(\@\) operations define a reduction relation which could be circular; the problem is solved by a fixed point construction; this approach enables the authors to show that the whole type 0 syntactic theory is suitable also to I and \(III_ n\) types without using a hierarchy of TRSs. The authors consider the confluence and termination problem for some known strategies: full substitution, leftmost reduction, parallel outermost reduction. They analyse the decidability of normal forms and give some criteria.