Abstract Powerful confluence criteria for higher-order rewriting exist for left-linear systems, even in the presence of critical pairs and non-termination. On the other hand, confluence criteria that allow for mixing non-termination and non-left-linearity are either extremely limited or hardly usable in practice. In this paper, we study confluence criteria which explore sort information to make proving higher-order confluence possible, even in the presence of non-termination and non-left-linearity. We give many interesting examples of systems covered by our results, including a (confluent) variant of Klop’s counterexample, and a calculus issuing from a dependent type theory with cumulative universes.

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules.

Abstract User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

We develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. We show that confluence is preserved for a large subset of terms that contains all pure lambda terms. Our results are applied to famous Klop’s examples of non-confluent behaviours in presence of convergent rewrite rules and to fragments of various encodings, in a dependent type theory with rewrite rules, of the Calculus of Constructions with polymorphic universes.

We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus. We justify here CoqMT’s type-checking algorithm by showing strong normalization as well as the Church-Rosser property of β-reductions augmented with CoqMT’s weak and strong T -elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.

We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church’s simply typed λ-calculus and, on the other hand, any use of eta, as a reduction, as an expansion, or as an equation. The user’s rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.

We study a complex type theory, a Calculus of Inductive Constructions with a predicative hierarchy of universes and a first-order theory T built in its conversion relation. The theory T is specified abstractly, by a set of constructors, a set of defined symbols, axioms expressing that constructors are free and defined symbols completely defined, and a generic elimination principle relying on crucial properties of first-order structures satisfying the axioms. We first show that CoqMTU enjoys all basic meta-theoretical properties of such calculi, confluence, subject reduction and strong normalization when restricted to weak-elimination, implying the decidability of type-checking in this case as well as consistency. The case of strong elimination is left open.

This article extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. These relations can be generated from two given well-founded orderings, on the function symbols and on the type constructors. The obtained orderings on terms are well founded, monotonic, stable under substitution and include β-reductions. They can be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules using first-order pattern matching. For example, the polymorphic version of Gödel's recursor for the natural numbers is easily oriented. And indeed, our ordering is polymorphic, in the sense that a single comparison allows to prove the termination property of all monomorphic instances of a polymorphic rewrite rule. Many nontrivial examples are given that exemplify the expressive power of these orderings. All have been checked by our implementation. This article is an extended and improved version of Jouannaud and Rubio [1999]. Polymorphic algebras have been made more expressive than in our previous framework. The intuitive notion of a polymorphic higher-order ordering has now been made precise. The higher-order recursive path ordering itself has been made much more powerful by replacing the congruence on types used there by an ordering on types satisfying some abstract properties. Besides, using a restriction of Dershowitz's recursive path ordering for comparing types, we can integrate both orderings into a single one operating uniformly on both terms and types.

This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. The obtained ordering is well-founded, compatible with p-reductions and with polymorphic typing, monotonic with respect to the function symbols, and stable under substitution. It can therefore be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules. For example, the polymorphic version of Godel's recursor for the natural numbers is easily oriented. And indeed, our ordering is polymorphic, in the sense that a single comparison allows to prove the termination property of all monomorphic instances of a polymorphic rewrite rule. Several other non-trivial examples are given which exemplify the expressive power of the ordering.

This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn Clauses built up from the equality and finitely many unary membership predicates. In contrast with other works in the area, constructors are not assumed to be free. Techniques originating from tree automata are used to describe ground constructor terms in normal form, on which the induction proofs are built up. Validity of (free) constructor clauses is checked by on original technique relying on the recent discovery of a complete axiomatisation of finite trees and their rational subsets. Validity of clauses with defined symbols or non-free constructor terms is reduced to the latter case by appropriate inference rules using a notion of ground reducibility for these symbols. We show how to check this property by generating proof obligations which can be passed over to the inductive prover.

Results for syntactic theories are generalized to shallow theories. The main technique used is the computation by ordered completion techniques of conservative extensions of the starting shallow presentation which are, respectively, ground convergent, syntactic, and cycle-syntactic. In all cases, the property that variables occur at depth at most one appears to be crucial. shallow theories thus emerge as a fundamental nontrivial, union-closed subclass of equational theories for which all important questions are decidable.>

The combination of polymorphically typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allow higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions if provided by the definition of the map function for lists.>

A complete unification algorithm is presented for the combination of two arbitrary equational theories E in T(F,X) and E/sup 1/ in T(F',X), where F and F' denote two disjoint sets of function symbols. The method adapts to unification of infinite trees. It is applied to two well-known open problems, when E is the theory of Boolean rings or the theory of Abelian groups, and E is the free theory. The interest to Boolean rings originates in VSLI verification.>

Abstract Church-Rosser properties are first presented, depending on an arbitrary relation R, an equivalence relation E and a reduction relation $R^E $ used to compute normal forms of R modulo E. Terminating rewriting systems operating on equational congruence classes of terms of a free algebra are then considered. In this framework, the Church–Rosser property is proved decidable for a very general reduction relation which may take into account the left-linearity of rules for efficiency reasons, under the only assumption of existence of a complete and finite unification algorithm for the underlying equational theory, whose congruence classes are assumed to be finite. This extends previous results by Lankford and Ballantyne, Peterson and Stickel, Huet, Jouannaud. A general completion procedure for mixed sets of rules and equations is then presented that generalizes and improves Peterson and Stickel’s one. In addition to computing a Church–Rosser set of rules when it terminates, it yields a semi-decision procedure for testing equality when it runs forever. Finally a post-processor is described that yields a Church–Rosser set of inter-reduced rules. All proofs, including the correctness proof of our completion algorithm, are based on the powerful proof technique of multiset induction.

Article Principles of OBJ2 Share on Authors: Kokichi Futatsugi Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, Japan Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, JapanView Profile , Joseph A. Goguen SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford University SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversityView Profile , Jean-Pierre Jouannaud CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, France CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, FranceView Profile , José Meseguer SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford Universit SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversitView Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985 Pages 52–66https://doi.org/10.1145/318593.318610Online:01 January 1985Publication History 308citation447DownloadsMetricsTotal Citations308Total Downloads447Last 12 Months14Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Article Completion of a set of rules modulo a set of equations Share on Authors: Jean-Pierre Jouannaud CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile , Helene Kirchner CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 83–92https://doi.org/10.1145/800017.800519Online:15 January 1984Publication History 41citation373DownloadsMetricsTotal Citations41Total Downloads373Last 12 Months8Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access