HORPO with Computability Closure : A Reconstruction
Fr\'ed\'eric Blanqui (INRIA Lorraine - LORIA), Jean-Pierre Jouannaud, (LIX), Albert Rubio

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Computability, Logic, AI Algorithms · Model-Driven Software Engineering Techniques
