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

📧 Request an update