A rationale for conditional equational programming.

*(English)*Zbl 0702.68034Summary: Conditional equations provide a paradigm of computation that combines the clean syntax and semantics of LISP-like functional programming with Prolog-like logic programming in a uniform manner. For functional programming, equations are used as rules for left-to-right rewriting; for logic programming, the same rules are used for conditional narrowing. Together, rewriting and narrowing provide increased expressive power. We discuss some aspects of the theory of conditional rewriting, and the reasons underlying certain choices in designing a language based on them. The most important correctness property a conditional rewriting program may possess is ground confluence; this ensures that at most one value can be computed from any given (variable-free) input term. We give criteria for confluence. Reasonable conditions for ensuring the completeness of narrowing as an operational mechanism for solving goals are provided; these results are then extended to handle rewriting with existentially quantified conditions and built-in predicates. Some termination issues are also considered, including the case of rewriting with higher-order terms.

##### MSC:

68N01 | General topics in the theory of software |

68N17 | Logic programming |

68Q42 | Grammars and rewriting systems |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

##### Keywords:

conditional equational programming; functional programming; logic programming; rewriting; narrowing; ground confluence
PDF
BibTeX
XML
Cite

\textit{N. Dershowitz} and \textit{M. Okada}, Theor. Comput. Sci. 75, No. 1--2, 111--138 (1990; Zbl 0702.68034)

Full Text:
DOI

##### References:

[1] | Bachmair, L.; Dershowitz, N.; Hsiang, J., Orderings for equational proofs, (), 346-357 |

[2] | Bellia, M.; Levi, G., The relation between logic and functional languages: a survey, J. logic programming, 3, 3, 217-236, (1986) · Zbl 0599.68014 |

[3] | Bergstra, J.A.; Klop, J.W., Conditional rewrite rules: confluency and termination, J. comput. system sci., 32, 323-362, (1986) · Zbl 0658.68031 |

[4] | Bertling, H.; Ganzinger, H., Completion-time optimization of rewrite-time goal solving, (), 45-58 |

[5] | Bosco, P.G.; Giovannetti, E.; Moiso, C., Refined strategies for semantic unification, (), 276-290 |

[6] | Breazu-Tannen, V.; Gallier, J., Polymorphic rewriting converses algebraic strong normalization and confluence, () · Zbl 0686.68022 |

[7] | Breazu-Tannen, V., Combining algebra and higher-order types, Edinburgh, Proc. 3rd IEEE symp. on logic in computer science, 82-90, (1988) |

[8] | Darlington, J.; Field, A.J.; Pull, H.; DeGroot, D.; Lindstrom, G., The unification of functional and logic languages, Logic programming, 37-70, (1986) |

[9] | () |

[10] | Deransart, P., An operational algebraic semantics of PROLOG programs, () · Zbl 0416.68077 |

[11] | Dershowitz, N., Computing with rewrite systems, (), Inform. and control, 64, 122-157, (1985), revised version appeared in · Zbl 0584.68020 |

[12] | Dershowitz, N.; Jouannaud, J.-P.; Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, (), Comm. ACM, 22, 8, 465-476, (1979) · Zbl 0431.68016 |

[13] | Dershowitz, N.; Okada, M., Proof-theoretic techniques and the theory of rewriting, Edinburgh, Scotland, Proc. 3rd IEEE symp. on logic in computer science, 104-111, (1988) |

[14] | Dershowitz, N.; Okada, M.; Sivakumar, G., Confluence of conditional rewrite systems, (), 31-44 · Zbl 0666.68094 |

[15] | Dershowitz, N.; Okada, M.; Sivakumar, G., Canonical conditional rewrite systems, (), 538-549, Argonne, IL |

[16] | Dershowitz, N.; Plaisted, D.A., Logic programming cum applicative programming, Boston, MA, Proc. IEEE symp. on logic programming, 54-66, (1985) |

[17] | Dershowitz, N.; Plaisted, D.A., Equational programming, (), 21-56 · Zbl 0722.68070 |

[18] | Dershowitz, N.; Sivakumar, G., Goal-directed equation solving, St. Paul, MN, Proc. 7th national conf. on artificial intelligence, 166-170, (1988) |

[19] | Fay, M., First-order unification in an equational theory, Austin, TX, Proc. 4th workshop on automated deduction, 161-167, (1979) |

[20] | Fribourg, L., Oriented equational clauses as a programming language, J. logic programming, 1, 179-210, (1984) · Zbl 0597.68034 |

[21] | Fribourg, L., SLOG: a logic programming language interpreter based on clausal superposition and rewriting, Boston, MA, Proc. IEEE symp. on logic programming, 172-184, (1985) |

[22] | Girard, J.Y., Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types., Proc. 2nd Scandinavian logic symp., 63-92, (1971) |

[23] | Goguen, J.A.; Meseguer, J., Equality, types, modules and (why not?) generics for logic programming, Logic programming, 1, 2, 179-210, (1984) · Zbl 0575.68091 |

[24] | Goguen, J.A.; Meseguer, J.; DeGroot, D.; Lindstrom, G., EQLOG: equality, types, and generic modules for logic programming, Logic programming, 295-363, (1986) |

[25] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. assoc. computing Mach., 27, 4, 797-821, (1980) · Zbl 0458.68007 |

[26] | Huet, G.; Oppen, D.C., Equations and rewrite rules: a survey, (), 349-405 |

[27] | Hullot, J.-M., Canonical forms and unification, (), 318-334 |

[28] | Jayaraman, B.; Silberman, F.S.K., Equations, sets, and reduction semantics for functional and logic programming, Cambridge, MA, Proc. ACM conf. on LISP and functional programming, 320-331, (1986) |

[29] | Josephson, N.A.; Dershowitz, N., An implementation of narrowing, J. logic programming, 6, 1,2, 57-77, (1989) · Zbl 0668.68112 |

[30] | Jouannaud, J.-P.; Waldmann, B., Reductive conditional term rewriting systems, () |

[31] | J.-P. Jouannaud and M. Okada, Rewriting with higher order terms, in preparation. |

[32] | Kahn, K.M., Uniform—A language based upon unification which unifies much of lisp, prolog and act 1, Vancouver, B.C., Proc. 7th internat. joint conf. on artificial intelligence, 933-939, (1981) |

[33] | Kanamori, T., Computation by meta-unification with constructors, () |

[34] | Kaplan, S., Simplifying conditional term rewriting systems: unification, termination and confluence, J. symbolic comput., 4, 3, 295-334, (1987) · Zbl 0641.68046 |

[35] | Klop, J.W., Combinatory reduction systems, () · Zbl 0466.03006 |

[36] | Knuth, D.E.; Bendix, P.B., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902 |

[37] | Komorowski, H.J., QLOG—the programming environment for PROLOG in LISP, (), 315-322 |

[38] | Lindstrom, G., Functional programming and the logic variable, Proc. 12th ACM symp. on principles of programming languages, 266-280, (1985), New Orleans, LA |

[39] | Malachi, Y.; Manna, Z.; Waldinger, R.J., TABLOG: the deductive tableau programming language, Austin,TX, Proc. ACM symp. on LISP and functional programming, 323-330, (1984) |

[40] | Martin-Löf, P., Haupsatz for the theory of species, Proc. 2nd Scandinavian logic symp., 217-233, (1971) |

[41] | Martelli, A.; Moiso, C.; Rossi, G.F., An algorithm for unification in equational theories, Salt Lake City, UT, Proc. IEEE symp. on logic programming, 180-186, (1986) |

[42] | O’Donnell, M.J., Computing in systems described by equations, () · Zbl 0421.68038 |

[43] | Okada, M., Strong normalizability for the combined system of the pure typed λ-calculus and an arbitrary convergent term rewrite system, Proc. internat. symp. on symbolic and algebraic computation, (1989) |

[44] | Okada, M.; Gregono, P., Practical application of conditional term rewriting systems, Proc. IX conf. of the Chilean computer science society/XV Latin American conf. on informatics, (1989) |

[45] | Okada, M.; Grogono, P., New results in term rewriting theory, Proc. of the internat. conf. on symbolic and logic computation, (1989) |

[46] | Okada, M., Note on a proof of the extended kirby-Paris game for labeled finite trees, European J. combin., 9, 249-253, (1988) · Zbl 0657.05020 |

[47] | Okada, M., Introduction to proof theory for computer science, (1988), Laboratoire de Recherche Informatique, Universite de Paris-Sud Orsay, France, Unpublished lecture notes |

[48] | Okada, M., Proof-theoretic ordinals and ordering structures in term rewriting theory, () |

[49] | Okada, M., A logical analysis for the theory of conditional rewriting, (), 179-196, Orsay, France |

[50] | Plaisted, D.A., Semantic confluence tests and completion methods, Inform. and control, 65, 2/3, 182-215, (1985) · Zbl 0598.68058 |

[51] | Prawitz, D., Ideas and results in proof theory, Proc. 2nd Scandinavian logic symp., 235-307, (1971) |

[52] | Reddy, U.S., Narrowing as the operational semantics of functional languages, Boston, MA, Proc. IEEE symp. logic programming, 138-151, (1985) |

[53] | Robinson, J.A., Beyond LOGLISP—combining functional and relational programming in a reduction setting, (), 1-20 · Zbl 0770.68040 |

[54] | Sato, M.; Sakurai, T., QUTE: a functional language based on unification, Tokyo, Japan, Proc. internat. conf. on fifth generation computer systems, 157-165, (1984) |

[55] | Slagle, J.R., Automated theorem-proving for theories with simplifiers, commutativity, and associativity, J. assoc. comput. Mach., 21, 4, 622-642, (1974) · Zbl 0296.68092 |

[56] | Smolka, G.; DeGroot, D.; Lindstrom, G., FRESH: a higher-order language with unification and multiple results, Logic programming, 469-524, (1986) |

[57] | Tait, W.W., Intensional interpretation of functionals of finite type, J. symbolic logic, 32, 198-212, (1967) · Zbl 0174.01202 |

[58] | Tamaki, H., Semantics of a logic programming language with a reducibility predicate, Atlantic City, NJ, Proc. IEEE symp. on logic programming, 259-264, (1984) |

[59] | Zhang, H.; Rémy, J.-L., Contextual rewriting, (), 46-62 |

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.