[Haskell-cafe] Slightly off-topic: Lambda calculus

[Andrew Coppin]

Andrew Coppin wrote:
> Ladies and gentlemen, we have a counter-example!
>
>  (\x1 -> x1 x1) (\y2 -> \z3 -> y2 z3)
>  (\y2 -> \z3 -> y2 z3) (\y2 -> \z3 -> y2 z3)
>  \z3 -> (\y2 -> \z3 -> y2 z3) z3
>  \z3 -> \z3 -> z3 z3
>
> Now the operative question becomes... how in the name of God to I fix 
> this?
>
> (The obvious approach would be to rerun the renamer; but would 
> discarding the variable indicies introduce even more ambiguity? Hmm...)

I knew alpha conversions were trixy little things! ;-)

Well anyway, the obvious thing to do is after each reduction, strip off 
all the variable indicies and rerun the labeller to assign new indicies. 
But does this solution work properly in general?

The labeller is carefully crafted to respect scoping, so that for 
example "\x -> x (\x -> x) x" becomes "\x1 -> x1 (\x2 -> x2) x1". But 
still, the final expression above is nicely labelled, yet wrong. How 
does this happen?

Well, variable indicies are supposed to be unique. But in line 2 we see 
a bunch of them get duplicated. At this point, if you strip all the 
indicies and recompute them, you get

  (\y1 -> \z2 -> y1 z2) (\y3 -> \z4 -> y3 z4)

There are now no spurious duplicates, and the reduction should proceed 
through the remaining steps without incident.

So rerunning the labeller works *for this example*. But does it work in 
general?

As an alternative, I could completely reprogram my entire application to 
use de Bruijn indices. Hmm...