Optimal Sharing Graphs for Substructural Higher-order Rewriting Systems

The notion of optimal reduction was introduced by Lévy (1980) in the context of the untyped ?-calculus, based on the concept of families of reducible expressions. It took more than a decade for an algorithm achieving this optimal reduction to be discovered, introduced by Lamping (1990) and then refined by Gonthier, Abadi & Lévy (1992). The existence of an analogous algorithm for higher-order term rewriting systems was later theorised by Van Oostrom (1996), but has of yet been unrealised.

We provide such an algorithm by defining a class of higher-order rewriting systems having Intuitionistic Linear Logic (Benton, Bierman, de Paiva & Hyland 1992) as a substitution calculus, in the sense of Van Oostrom (1994), and introduce a method of translating terms and rules into equivalent Lamping-Gonthier sharing graphs. Our system thus offers a generalisation of the mechanism for optimal reduction from second- to higher-order term rewriting systems. Moreover, in the case of match-sequential systems, we provide a specific reduction strategy, as we are able to effectively identify needed redexes.

Finally, we explore briefly the subtleties and complexities of applying the technique to various other term rewriting system, such as those with alternative substructural or polymorphic type systems, those with generalised patterns on the left-hand side, and those with rationally infinite terms. All these systems are built upon the same fundamental translation of ?-terms to sharing graphs.