A BRICS Mini-Course
February 24-26, 1999
Stefano Guerrini, email@example.com
Department of Computer Science, Queen Mary and Westfield College, London, United Kingdom
Lambda-calculus optimal reductions were defined in Levy's dissertation in 78. Levy's optimal reductions rest on a beautiful abstraction of the intuitive concept of `sharable redex'. This abstraction led Levy to find a lower-bound for the cost of the reduction of a lambda-term T by any conceivable reduction machine capable to reduce, in a single step, all the sharable redexes in T. Unfortunately, Levy did not give any actual machine satisfying that optimality requirement. A brilliant solution for the problem was proposed by Lamping more than 10 years later by means of the so-called sharing graph reductions. Lamping's sharing graph technique was successively improved by several researchers (the list includes Gonthier, Asperti, Laneve, Danos, Regnier, etc.) that discovered surprising connections with Linear Logic and Geometry of Interaction. Finally, Asperti and Mairson proved that there is no chance to get an optimal reduction machine, at least in the tight sense defined by Levy, for this would contradict the time hierarchy theorem. Nevertheless, this does not decrease the relevance of optimal reductions and of sharing graphs. It only shows that the computational complexity of lambda-calculus cannot be captured by counting beta-rules only, neither by extending beta-rule to a rule reducing in parallel all the sharable redexes in a term.
In this mini-course, we want to focus on the main ideas behind optimal reductions and sharing reductions. For the amount and the complexity of the results that we want to analyze, there will be no time for a lot of details. The main aim is at justifying why optimal reductions and sharing graphs are milestones in the quest for understanding the computational complexity of beta-reduction, and in which sense Asperti-Mairson result opens new and interesting problems in the field.