Archive for the 'Term rewriting' Category

Closed nominal rewriting and efficiently computable nominal algebra equality

By Maribel Fernandez and Murdoch J. Gabbay, from LFMTP 2010, available from Murdoch J. Gabbay’s website:

We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of lambda-calculus and first-order logic.

Advertisements

Efficient lambda-evaluation with interaction nets

I was informed of this paper on a trip to the University of Sussex just before Christmas.  Unfortunately, it’s taken me a while to get around to reading it, and therefore posting it to the blog.  The paper’s of interest not only to those who are interested in name binding, where interaction nets appear to provide a graphical representation of lambda-terms (and much more), but also those interested in implementing rewrite systems, wherein interaction nets facilitate a very efficient implementation.

By Ian Mackie, from RTA 2004, available from SpringerLink:

This paper presents an efficient implementation of the lambda-calculus using the graph rewriting formalism of interaction nets. Building upon a series of previous works, we obtain one of the most efficient implementations of this kind to date: out performing existing interaction net implementations, as well as other approaches. We conclude the paper with extensive testing to demonstrate the capabilities of this evaluator.

CINNI: A generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi

By Mark Oliver Stehr, from WRLA 2000, available from Mark Oliver Stehr’s website:

We approach the general problem of representing higher-order languages, that are usually equipped with special variable binding constructs, in a less specialized first-order framework such as membership equational logic and the corresponding version of rewriting logic. The solution we propose is based on CINNI, a new calculus of explicit substitutions that makes use of a term representation that contains both the standard named notation and de Bruijn’s indexed notation as special subcases. The calculus is parametric in the syntax of the object language, which allows us to apply it to different object languages such as λ-calculus, Abadi and Cardelli’s object calculus (ς-calculus) and Milner’s calculus of communicating mobile processes (π-calculus). As a practical result we obtain executable formal representations of these object languages in Maude with a representational distance close to zero.

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.

Term rewriting with variable binders: an initial algebra approach

By Makoto Hamana, from PPDP 2003, available from Makoto Haman’s website:

We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner; firstly we present the term language, then formulate equational logic, and finally define rewrite systems by two styles: rewrite logic and pattern matching styles. The novelty of this development is that we follow an initial algebra approach in an extended notion of Σ-algebras in various functor categories. These are based on Fiore-Plotkin Turi’s presheaf semantics of variable binding and Lüth-Ghani’s monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs are initial algebras in suitable categories. Finally, we discuss our design choice of BTRSs from a semantic perspective.