# [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
general?

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

```