When & Where: 12:30pm, Friday, November 18, 2005, Room 200 AKW
Abstract:
Models of rewriting for the lambda calculus that allow sharing of structure are essential to the implementation of functional programming languages. The earliest and most widely used model of sharing characterises terms of the lambda calculus as directed acyclic graphs, as investigated in Christopher Wadsworth's 1971 PhD thesis, and most of the literature on term-graph rewriting follows this model.
A radically different form of sharing comes from the 1978 work on optimal reductions in the lambda calculus of Jean-Jacques Levy, which arose from his observation that the DAG model of sharing inevitably caused duplication of work, which led in turn to a realisation of a model of sharing in John Lamping's Partial Sharing Graphs of 1990. Partial sharing, the possibility of sharing less than complete subterms is essential to realising optimal reductions, but comes at a heavy price in terms of complexity: while the graph model itself is simple, it's relationship to the lambda calculus is opaque.
In my talk I will present an intermediate notion of sharing that I call parametric sharing that captures some of the partial sharing used in Lamping's model of optimal reductions but which maintains a straightforward relationship to the usual syntax of the lambda calculus, little more complex than Wadsworth's DAG model. I'll discuss the relationships between the three models of sharing and sketch the beginnings of a hierarchy of notions of sharings that hope to cast more light on optimal reductions.