Rewriting Properties of Combinators for Intuitionistic Linear Logic

this paper we investigate the possibility of developing a (semi-)automatic rewriting tool for manipulating and reasoning about combinators for Intuitionistic Linear Logic. In particular, we develop a canonical (i.e. confluent and terminating) term rewriting system associated to a theory of categorical combinators for (rudimentary) Linear Logic. In order to do that, we make use of the Knuth-Bendix completion algorithm [3] to transform the equational theory for the combinators into an equivalent canonical rewrite system. This means that a set of categorical combinators for Linear Logic has first to be derived, and then the resulting system of combinators can be checked for rewriting properties using rewriting techniques. The process of deriving categorical combinators has been a relatively long one, with an interesting interaction between the more abstract side of the work (reported in [7]) and its mechanized version. We started with a first (theoretically correct) formulation of the combinators for each of the several fragments of the logic under consideration. As usual, the use of an automatic rewriting tool to derive and check properties such as local confluence, termination and canonicity of a system, has led us to "improve" the first axiomatic characterization of the categorical combinators, until an equivalent presentation was derived with the nice feature that rewriting techniques may be applied to it successfully. This process of transformation of the data provided by the theoretical considerations follows a definite pattern that is described in Section 2.3. Intuitionistic Linear Logic was introduced by Girard and Lafont in [4]. The basic assumption of Linear Logic is that one should be able to have a logical control of the resources available for a derivation. Th..