Nominal Completion for Rewrite Systems with Binders
Talk by Maribel Fernandez. Joint work with Albert Rubio.
Venue: Salle de reunion, 10h30 Thursday 26 April 2012
Nominal rewriting generalises first-order rewriting by providing
support for the specification of binding operators, using the
nominal approach. In this talk, I will present a new ordering
that can be used to prove termination of nominal rewriting rules,
generalising the recursive path ordering to take into account
alpha equivalence. Using this ordering, we have designed a
Knuth-Bendix style completion procedure (to our knowledge,
this is the first completion procedure available for rewriting
systems with binders). An implementation can be found at
