HORPO with Computability Closure : A Reconstruction

TL;DR

This paper introduces a new decidable version of the higher-order recursive path ordering that simplifies type comparisons and explicitly manages bound variables, enabling recursors for all strictly positive inductive types.

Contribution

It presents a reconstruction of HORPO that removes the computability closure and explicitly handles bound variables, broadening its applicability.

Findings

Decidable higher-order recursive path ordering without computability closure

Handles recursors for arbitrary strictly positive inductive types

Type comparisons are made only when necessary

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.