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.
https://hal.inria.fr/inria-00168304 Contributor : Frédéric BlanquiConnect in order to contact the contributor Submitted on : Monday, August 27, 2007 - 12:21:26 PM Last modification on : Friday, February 4, 2022 - 3:30:27 AM Long-term archiving on: : Friday, April 9, 2010 - 1:10:38 AM
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. HORPO with Computability Closure : A Reconstruction. 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Oct 2007, Yerevan, Armenia. ⟨inria-00168304⟩