Six years ago, I taught a class called “Lambda Calculus and Applications” at U. Iowa. When I was preparing the course, I was thinking that I would try not to sweep the issue of renaming variables under the rug, which is what is universally done by everyone, except:
- people trying to formalize a language with bound variables in a theorem prover, and then they use de Bruijn indices (unless they have the happiness to have higher-order abstract syntax available to them, and then they definitely use that).
- the tiny group of interesting people who actually want to reason about alpha equivalence itself.
Three years ago, I taught the class again. I didn’t quite remember how things went the first time. It had been covid time, I had three children I was mostly caring for. I did have a nagging memory there was some snag…
I talked about beta-reduction. I talked about alpha-equivalence.
And then I started the proof of confluence of…
Something involving beta-reduction and alpha-equivalence?
And then you know what? I remembered that the class eight years ago had run right off the rails in a fireball as I floundered trying to prove confluence with explicit alpha-equivalence. With renewed energy, I tried it again in the class of six years ago. The fireball was bigger this time, because I drove the alpha train with more determination.
I had to set the problem aside for a bit, but I returned to it last year, with a focus on the theorem I ran into which broke the whole program: confluence with explicit alpha-equivalence. Well, we “know” how to do that, because Church and Rosser proved it already. But their proof is not so easy to follow, and the modern way to do the proof, namely the Tait-Martin-Loef method (possibly as improved by Takahashi), hasn’t been extended to explicit alpha-equivalence, to my knowledge. So I set out to do this.
And had a miserable time of it, again. I gave up for another year. The issue was in considering all combinations of alpha-steps and beta-steps from a starting term. It just became intractable.
This summer, feeling pretty positive I guess, I returned to the problem. And I am happy to report that this time, there was progress! (There is a moral to the story of research misery here…!)
The Tait-Martin-Loef proof of confluence relies on a notion of parallel reduction. We can reduce any of the redexes in a term, and their residuals, in one parallel step. The reductions all must be capture-avoiding, of course, which we must state explicitly with named variables. But we cannot reduce any redexes that get created. The proof of confluence follows easily from the central theorem about parallel reduction, that it has the diamond property: if a term t parallel reduces to terms s1 and s2, then those terms parallel reduce to a common term t’. In fact, Takahashi showed that s1 and s2 will both reduce to a term t* computed from t by contracting all the redexes in t. So we have the so-called triangle property: if t parallel reduces to s, then s parallel reduces to t*. (As a corollary, t parallel reduces to t*, since t parallel reduces to itself.)
Now, how to incorporate alpha-equivalence? I am having good success by making alpha-steps part of parallel reduction. So to parallel reduce s to t, you can contract redexes in s or their residuals, and you can also rename bound variables (in a capture-avoiding way) of lambda-terms that are not part of contracted redexes.
To extend Takahashi’s approach, I am using a function acanon, which puts terms t into alpha-canonical form, by computing fresh names (in a canonical way) for the bound variables in t. Canonicity arises because we compute fresh names deterministically from the set of current possibly free variables of the term.
I am happy to report that with this approach, I have completed a proof of a version of a well-known theorem in lambda-calculus with explicit alpha. The theorem says that if variables in a term t are suitably distinct, then t parallel reduces to t* without any alpha-steps. I formulate this as follows: given any term t, the alpha-canonization a of t can be parallel-reduced to a*. This implies that no capture takes place when computing a*, because if it did, a would not be able to parallel-reduce to a*, as parallel-reduction (as I define it) forbids capture.
The repo for my development is here.
My next target is to prove a suitable form of the triangle property: if t parallel-reduces to s, then s parallel-reduces to (acanon t)*. Initial exploration suggests that this will have to be formulated in a somewhat more general way, to account for alpha.
in 
with the offer of a billion dollars, and 
(which is implicit in 
, as this is really just 
) with a wish. The latter makes sense because if you have a proof of 
QA9 