A Completion Procedure for Equational Rewriting Systems with Binders
摘要
Completion of first-order rewriting has been extensively studied; however, challenges remain in languages that include binders – addressing them is crucial to enable theorem proving applications. In practice, the \(\alpha \) -equivalence generated by the binders has to be combined with an \(\mathcal {E}\) -equivalence generated by equational axioms. The extension of first-order rewriting to work modulo both \(\alpha \) -equivalence and equational axioms \(\mathcal {E}\) is not straightforward: particular care is needed when dealing with freshness constraints and renamings, since these can interact with \(\mathcal {E}\) . In this paper, we define equational nominal rewrite systems (ENRSs) and present a critical pair theorem and a generalised notion of closedness. In addition, we design a completion procedure for closed ENRSs, based on a generalisation of the recursive path ordering, using a novel notion of irrelevance of freshness contexts.