HORPO with Computability Closure : A Reconstruction
Logic in Computer Science
2007-08-28 v1
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.
Keywords
Cite
@article{arxiv.0708.3582,
title = {HORPO with Computability Closure : A Reconstruction},
author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Albert Rubio},
journal= {arXiv preprint arXiv:0708.3582},
year = {2007}
}