Nominal rewriting systems

Continuing the rewriting theme, here’s how to rewrite with binders using nominal techniques…

By Maribel Fernandez, Murdoch J. Gabbay and Ian Mackie, from PPDP 2004, available from Murdoch J. Gabbay’s website:

In this paper we present a generalization of first-order rewriting that 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 alpha-conversion and has good properties. This is achieved by adapting the powerful techniques for programming with binders developed by Pitts et al. in the FreshML project to the rewriting framework We extend the syntax of first-order terms with simple constructs to represent binding operations. Terms involving binders can be matched against terms naming bound variables explicitly. Nominal rewriting can be seen as higher-order rewriting with first-order syntax. We show that standard, first-order, rewriting is a particular case of nominal rewriting, and we also show that very expressive higher-order systems such as Klop’s Combinatory Reduction Systems can be easily defined as nominal rewriting. Finally we study confluence and termination properties of nominal rewriting. Keywords: variable binding, alpha-conversion, first and higher-order rewriting.

0 Responses to “Nominal rewriting systems”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: