具有可计算性闭包的HORPO：一种重构方法
HORPO with Computability Closure : A Reconstruction
摘要：
本文给出了高阶递归路径序的一个新的、可判定的定义，其中只在需要时进行类型比较，从而消除了对可计算性闭包的需要，并且显式地处理了约束变量，使得处理任意严格正归纳类型的递归成为可能.
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
