HORPO with Computability Closure: A Reconstruction

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

• Type: Conference
• Year: 2007
• Where: LPAR
• Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
• Keywords: Artificial Intelligence, Computability Closure, Decidable Definition, LPAR 2007, Positive Inductive Types