A Total AC-Compatible Reduct ion Ordering on Higher-Order Terms
l'ia, Waluld · 2006
Automated methods of proving termination of rewrite systmns a.rc used in many theorem provers and specitication development systcins. Most of these inethods arc based on finding a suitable reduction ordering, i.e., a well-founded partial order which is stable untler context and substitution. The most popular reduction ordering in first-order rewriting is RPO recursive path oTdcring. Its principle is to generate recursively an ordering on terms fi'om a given ordering on function symbols called precedence. The recursive definition of RPO allows to apply and to implement it easily. Higher-order rewrite rules are used in the programming languages, like ML, Elf, or theorem prow::rs, like Isabelle. Unfortunately, there are only few methods for proving termination of higher-order systems. In the case of first-order pat tern matching it is known that a higher-order rewrite system has terlnina.tion property when its rules billow a generalised form of a prilnitive recursive schema of higher type (see [5, 4]). in the general case of higher-order pat tern matching one can use A-RPO proposed by Jouannaud and II,ubio [6]. A-R,PO is a higher-order reduction ordering) i.e., a well-fi)unded ordering stable under ground contexts and substitutions and moreover compatible with the underlying typed A-calculus. Since we arc interested in higher-order pattern matching, compatibility with typed A-calculus means compatibility with /3~-conversions. This is easily achieved by defining )~-RPO on canonical representatives terms in/~-normal r/-long form. Compared to RPO, A-RPO needs not only a precedence on function symbols but also a precedence on types. Terms are compared first by type, then by top symbol, finally the comparison proceeds