The computability path ordering

DOI10.2168/LMCS-11(4:3)2015MaRDI QIDQ3196359zbMATH OpenFDO

Authors Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1506.03943

zbMATH Keywords

reducibilitylambda-calculusrewritingterminationinductive typespath order

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Abstract: This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in the com-putability closure. The well-foundedness proof shows that core CPO captures the essence of computability arguments 'a la Tait and Girard, therefore explaining its name. We further show that no further type check can be eliminated from its recursive calls without loosing well-foundedness, but for one for which we found no counterexample yet. Two extensions of core CPO are then introduced which allow one to consider: the first, higher-order inductive types; the second, a precedence in which some function symbols are smaller than application and abstraction.

Recommendations

• The Computability Path Ordering: The End of a Quest
• scientific article; zbMATH DE number 1405624
• On the complexity of recursive path orderings
• scientific article; zbMATH DE number 1303201
• Ordinal computability
• A complete characterization of the ordering of path-complete methods
• On recursive path ordering
• Order-computable sets
• The first-order theory of lexicographic path orderings is undecidable
• Computably enumerable partial orders

Cited in

(15)

• Higher-Order Termination: From Kruskal to Computability
• Superposition with lambdas
• The Computability Path Ordering: The End of a Quest
• Computability Closure: Ten Years Later
• Coq formalization of the higher-order recursive path ordering
• Size-based termination of higher-order rewriting
• Superposition with lambdas
• HORPO with Computability Closure: A Reconstruction
• Superposition for higher-order logic
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• The computability path order for beta-eta-normal higher-order rewriting
• A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
• Certified Higher-Order Recursive Path Ordering
• A Lambda-Free Higher-Order Recursive Path Order

Describes a project that uses

Uses Software

• Automath

This page was built for publication: The computability path ordering

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196359)