The computability path ordering

DOI10.2168/LMCS-11(4:3)2015zbMATH Open1448.68253arXiv1506.03943MaRDI QIDQ3196359FDOQ3196359

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)

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.

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

Recommendations

• The Computability Path Ordering: The End of a Quest
• Publication:4938603
• 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

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)

Cited In (14)

• 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
• Title not available (Why is that?)
• 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

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)