zbMATH — the first resource for mathematics

Conditional rewrite rules: Confluence and termination. (English) Zbl 0658.68031
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.
Reviewer: V.Calmatuianu

68Q65 Abstract data types; algebraic specification
68T99 Artificial intelligence
Full Text: DOI
[1] Barendregt, H.P., The lambda calculus, its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[2] Bergstra, J.A.; Tucker, J.V., A characterisation of computable data types by means of a finite, equational specification method, (), 76-90 · Zbl 0449.68003
[3] Berry, G.; Lévy, J.J., Minimal and optimal computations of recursive programs, J. assoc. comput. Mach., 26, 1, (1979)
[4] Chew, P., Unique normal forms in term rewriting systems with repeated variables, (), 7-18
[5] Curry, H.B.; Feys, R., ()
[6] Drosten, K., Toward executable specifications using conditional axioms, Report 83-01, (1983), T. U. Braunschweig · Zbl 0558.68019
[7] Ehrig, H.E.; Kreowski, H.-J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Parameterized data types in algebraic specification languages, ()
[8] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness and implementation of abstract data types, () · Zbl 0359.68018
[9] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, (), 30-45, rev. version
[10] Huet, G.; Lévy, J.J., Call by need computations in non-ambiguous linear term rewriting systems, ()
[11] Huet, G.; Oppen, D.C., Equations and rewrite rules: A survey, ()
[12] \scS. Kaplan, Conditional rewrite rules, Theor. Comput. Sci., in press. · Zbl 0577.03013
[13] Kaplan, S., Fair conditional term rewriting systems: unification, termination and confluence, () · Zbl 0585.68048
[14] Klop, J.W., Combinatory reduction systems, () · Zbl 0466.03006
[15] Lévy, J.J., Réductions correctes et optimales dans le lambda-calcul, ()
[16] O’Donnell, M., Computing in systems described by equations, () · Zbl 0421.68038
[17] O’Donnell, M., Equational logic as a programming language, (1985), MIT Press Cambridge, Mass · Zbl 0636.68004
[18] Pletat, U.; Engels, G.; Ehrich, H.-D.; Pletat, U.; Engels, G.; Ehrich, H.-D., Forschungsbericht 118/81, (), (1981), extended version
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.