Skip to main content

Optimal Sharing Graphs for Substructural Higher-order Rewriting Systems

Smith, Connor Lane (2017) Optimal Sharing Graphs for Substructural Higher-order Rewriting Systems. Doctor of Philosophy (PhD) thesis, University of Kent,. (KAR id:63884)

Language: English
Download (832kB) Preview
[thumbnail of 249thesis.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


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.

Item Type: Thesis (Doctor of Philosophy (PhD))
Thesis advisor: Kahrs, Stefan
Thesis advisor: Thompson, Simon
Thesis advisor: Owens, Scott
Uncontrolled keywords: optimality, sharing graphs, substructural types, linear logic, higher-order rewriting, term rewriting, lambda calculus
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: System Moodle
Depositing User: System Moodle
Date Deposited: 06 Oct 2017 13:54 UTC
Last Modified: 16 Feb 2021 13:49 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):