Fernández, Maribel, Gabbay, Murdoch and Mackie, Ian (2004) Nominal rewriting systems. In: Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming.
Full text not available from this repository.Abstract
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
Item Type: | Conference or Workshop Item (Paper) |
---|---|
Schools and Departments: | School of Engineering and Informatics > Informatics |
Depositing User: | Ian Mackie |
Date Deposited: | 06 Feb 2012 20:42 |
Last Modified: | 13 Apr 2012 08:16 |
URI: | http://sro.sussex.ac.uk/id/eprint/27579 |