Rewriting Formalisms With Binding Support

: Comparing Combinatory Reduction Systems and Nominal Rewrite Systems with Atom Substitution

Abstract

In this thesis, two extensions of term rewriting systems with binding support are compared: Nominal Rewrite Systems defined by Fernández, Gabbay and Mackie (Fernández and Gab- bay, 2007; Fernández et al., 2004) and Combinatory Reduction Systems, a well-established higher-order rewriting formalism introduced by Klop (Klop, 1980; Klop et al., 1993).
Higher-order term rewriting is a collective name for a large number of different formal- isms combining term rewriting systems and the l -calculus, a formal system for expressing functional computation which provides to term rewriting systems a notion of binding and substitution as primitive. Nominal rewriting allows a first-order approach to binding where variables, both free and abstracted, can be directly manipulated and a-equality is formally axiomatised in the logic by means of a swapping operation and a freshness relation. Despite the differences in their underlying semantic foundations, nominal and higher-order rewriting formalisms are closely related to each other. The relationship between Combinatory Reduc- tion Systems and other higher-order rewriting formalisms has already been well documented (see for instance (Bertolissi et al., 2006; Kop, 2012; van Oostrom and van Raamsdonk, 1994; van Raamsdonk, 1999)). In (Fernández et al., 2004), Fernández, Gabbay and Mackie presented an encoding of Combinatory Reduction Systems into Nominal Rewrite Systems showing the rewrite relation to be preserved when adding to the encoded system a set of rules simulating higher-order substitution from the l-calculus. This immediately poses two areas of study that are addressed in this thesis, the simulation of nominal rewriting in Combinatory Reduction Systems and an extension of Nominal Rewrite Systems where higher-order substitution for nominal terms is provided as primitive. As a result, the naturality of the encoded Combinatory Reduction System in nominal rewriting is improved in the sense that the rewrite relation is not only preserved but also reflected.
This thesis aims to unify both rewriting communities by providing a concrete correspond- ence between Combinatory Reduction Systems and the nominal rewriting framework. There is a theoretical interest in showing such correspondence because the expressive power of nominal and higher-order rewriting is put in evidence.
Techniques to prove confluence and termination of higher-order rewriting systems were studied in (Hamana, 2010; Klop et al., 1993; Mayr and Nipkow, 1998) amongst others.
However, the syntax and type restrictions imposed on rewrite rules in these systems have prevented the design of completion procedures for higher-order rewrite systems (Nipkow and Prehofer, 1998). Nominal terms enjoy many useful properties, for instance, unification modulo a-equivalence is decidable and unitary (Urban et al., 2004) and nominal matching is linear (Calvès and Fernández, 2008a). Nominal rewriting can be implemented efficiently if we use closed rules, roughly speaking, closed rules do not contain unabstracted atoms and preserve the binding status of atoms during reduction - a natural restriction which is also imposed on Combinatory Reduction Systems by definition as well as other well- known higher-order formalisms (e.g. HRSs (Nipkow, 1991) and ERSs (Glauert et al., 2005; Khasidashvili, 1990)). Additionally, a completion algorithm for Nominal Rewrite Systems has been designed by Fernández and Rubio in (Fernández and Rubio, 2012). Therefore a practical interest arises, that of the possibility of transferring results between nominal rewriting and higher-order term rewriting by reason of the existing translations between Combinatory Reduction Systems and other higher-order rewriting formalisms. In particular, techniques and properties of the rewriting relation such as termination can be exported from nominal rewriting to Combinatory Reduction Systems.
This thesis first defines a pair of translation functions from Combinatory Reduction Systems to Nominal Rewrite systems and vice versa where the rewrite relation is preserved and (almost) reflected. The translation from Combinatory Reduction Systems to Nominal Rewrite systems is based on the translation given in (Fernández et al., 2004) where some issues have been corrected from the original translation as well as improving the naturality of the encoding by using closed rewriting, a formal treatment of the Barendregt variable convention in rule induction. An extension of nominal terms is then studied, where capture- avoiding substitution of atoms by terms is implemented in the syntax. Properties of the extended theory and an algorithmic representation of a-equality are then derived, providing a framework in which the notion of unification of extended nominal terms is defined, along with a proof of undecidability constructed by implementing an effective method to reduce Hilbert’s tenth problem to unification of nominal terms extended with atom substitution. Two matching algorithms are then specified, a general one that finds the set of all possible correct solutions and only correct solutions to any (unifiable) matching problem by imposing a syntactic restriction on the matching algorithm to avoid instantiation of variables on one side of the matching constraint, and a unitary simple-matching algorithm which enjoys the property of unique most general solutions for the class of simple matching constraints. Both matching algorithms are then applied to the extension of Nominal Rewrite Systems we describe, providing an operational definition of closedness for extended nominal terms and, in the case of the simple-matching algorithm, finding a match during the rewriting process.
Finally, we use the framework of extended nominal rewriting to provide a one-step reduction preserving translation from Combinatory Reduction Systems to standard extended Nominal Rewrite Systems as well as a reduction-preserving translation from the class of standard extended Nominal Rewrite Systems to Nominal Rewrite Systems.

Date of Award	2017
Original language	English
Awarding Institution	King's College London
Supervisor	Maribel Fernandez (Supervisor) & Christian Urban (Supervisor)