HORPO with Computability Closure: A Reconstruction

DOI10.1007/978-3-540-75560-9_12MaRDI QIDQ3498461zbMATH OpenOpenAlexFDO

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

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Abstract: This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.

Recommendations

• The Computability Path Ordering: The End of a Quest
• The computability path ordering
• Certified Higher-Order Recursive Path Ordering
• A Higher-Order Iterative Path Ordering
• A Lambda-Free Higher-Order Recursive Path Order

Cites work

• Higher-Order Termination: From Kruskal to Computability
• Polymorphic higher-order recursive path orderings
• Termination of rewriting in the Calculus of Constructions

Cited in

(4)

• Computability Closure: Ten Years Later
• Coq formalization of the higher-order recursive path ordering
• Uncurrying for termination and complexity
• The Computability Path Ordering: The End of a Quest

This page was built for publication: HORPO with Computability Closure: A Reconstruction

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