HORPO with Computability Closure: A Reconstruction

DOI10.1007/978-3-540-75560-9_12zbMATH Open1137.03307arXiv0708.3582OpenAlexW1896024878MaRDI QIDQ3498461FDOQ3498461

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)

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

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

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)