Lambda the Ultimate

Baillot, Coppola & Del Lago have an arXived preprint, "Light Logics and Optimal Reduction: Completeness and Complexity:

Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL, resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proof-nets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, resp.) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics).

We've 'known' that Lamping's algorithm implements Levy-optimality since Lamping 'proved' it in 1989, but unfortunately his argument has holes, and it has proven hard to fix them, this despite there being a fairly accessible geometric intuition supporting soundness & completeness. Harry Mairson has done worthy missionary work advertising the importance of this gap and working towards filling it. I haven't yet worked my way through this proof, but it looks like it belongs to a very attractive class of argument; namely those that attempt to forge a Curry-Howard-like correspondence between Lamping graphs and proof nets of weakened linear logics. Recommended reading for LtUers who enjoy a challenge!