I've been looking at various calculus with explicit substitutions for efficient implementation of normalisation of terms in the lambda calculus.
AFAICT there are basically two approaches: the λσ calculus of explicit substitutions, and the suspension calculus. All others I found suffer from the fact that they cannot compose substitutions, so they sometimes require several traversals of the terms.
Between the two, the suspension calculus seems much more amenable to an efficient implementation, but the λσ calculus seems more elegant and I find it a lot easier to have an intuition for what it means.
So, how can I implement the λσ calculus, in a way that is competitive (in terms of efficiency) with the suspension calculus?