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

Andrew Coppin andrewcoppin at btinternet.com
Sun Jun 21 14:24:52 EDT 2009

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 

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

More information about the Haskell-Cafe mailing list