Nominal rewriting systems

9 years 2 months ago
Nominal rewriting systems
We present a generalisation of first-order rewriting which allows 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 adapting to the rewriting framework the powerful techniques developed by Pitts et al. in the FreshML project. Nominal rewriting can be seen as higher-order rewriting with a first-order syntax and built-in α-conversion. We show that standard (first-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 defined as nominal rewriting systems. Finally we study confluence properties of nominal rewriting. Categories and Subject Descriptors F.4.1 [Mathematical Logic and F...
Maribel Fernández, Murdoch Gabbay, Ian Mack
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where PPDP
Authors Maribel Fernández, Murdoch Gabbay, Ian Mackie
Comments (0)