Nominal rewriting systems

We present a generalisation of ?rst-order rewriting which al- lows us to deal with terms involving binding operations in an elegant and practical way. We use a nominal approach to binding, in which bound entities are explicitly named (rather than using a nameless syntax such as de Bruijn indices), yet we get a rewriting formalism which respects ?-conversion and can be directly implemented. This is achieved by adapt- ing to the rewriting framework the powerful techniques de- veloped by Pitts et al. in the FreshML project. Nominal rewriting can be seen as higher-order rewriting with a ?rst-order syntax and built-in ?-conversion. We show that standard (?rst-order) rewriting is a particular case of nominal rewriting, and that very expressive higher-order systems such as Klop's Combinatory Reduction Systems can be easily de?ned as nominal rewriting systems. Finally we study confluence properties of nominal rewriting