Access Restriction

Author Jouannaud, Jean-Pierre ♦ Rubio, Albert
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2007
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Automated termination prover tool ♦ Gödel's polymorphic recursor ♦ Higher-order rewriting ♦ Termination orderings ♦ Typed lambda calculus
Abstract 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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2007-03-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 54
Issue Number 1
Page Count 48
Starting Page 1
Ending Page 48

Open content in new tab

   Open content in new tab
Source: ACM Digital Library