Light Logics and Optimal Reduction

Not sure this isn't a tad too technical for the front page, but posting has been light, so...

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!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Limited scope

I've had a chance to read the paper: it is nice, but less ambitious than I had thought -- the authors only consider the class of EAL ("elementary affine logic") -typable terms.

It may be possible to extend the results to a systems that can type all lambda-calculus terms by adding appropriate fix-point combinators. This is, of course, hairy in the presence of restrictions on the structural rules, and the authors do not discuss how to close the expressiveness gap.