[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jean-Pierre Jouannaud
Date: December 1991
Summary: Investigate confluence and termination of combinations of typed lambda-calculi with term rewriting systems.
Combinations of typed λ-calculi with term-rewriting systems have been studied extensively in the past few years [Bar90][BTG89][DO90][Dou91]. The strongest termination result allows first-order rules as well as higher-order rules defined by a generalization of primitive recursion. Suppose all rules for functional constant F follow the schema:
F(l[X],Ȳ)→ v[F(r_{1}[X],Ȳ) ,...,F(r_{m}[X],Ȳ),Ȳ)] |
where the (not necessarily disjoint) variables in X and Ȳ are of arbitrary order, each of l,r_{1},...,r_{m} is in T( F,{X}), v[z,Ȳ] is in T( F,{Ȳ,z}), for new variables z of appropriate types, and r_{1},…,r_{m} are each less than l in the multiset extension of the strict subterm ordering. If T(F,X) is the term-algebra which includes only previously defined functional constants—forbidding the use of mutually recursive functional constants—termination is ensured [JO91]. Does termination also hold when there are mutually recursive definitions? Does this also hold when the subterm assumption is unfulfilled? (In [JO91] an alternative schema is proposed, with the subterm assumption weakened at the price of having only first-order variables in X.) Questions of confluence of combinations of typed λ-calculi and higher-order systems also merit investigation. These results have been extended to combinations with more expressive type systems [BF93b][BF93a].
An extension to the Calculus of Constructions has been reported in [BFG94]. One can also allow the use of lexicographic and other “statuses” for the higher-order constants when comparing the subterms of F in left and right hand sides [Jouannaud and Okada, unpublished]. Finally, this can also be done when the rewrite rules follow from the induction schema in the initial algebra of the constructors [Wer94].
Important improvements of the previous works have been achieved in [Bla03] and [WC03].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |