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

Thomas DuBuisson thomas.dubuisson at gmail.com
Sun Jun 21 21:04:25 EDT 2009

```All,
Just as ancillary information: ∃ a calculator on Hackage called
"LambdaCalculator".  Its rather short (loc wise) and fun to play with.

Thomas

On Sun, Jun 21, 2009 at 10:57 AM, Andrew
Coppin<andrewcoppin at btinternet.com> wrote:
> Lauri Alanko wrote:
>>
>> With "name collisions" I'm assuming you mean inadvertent variable
>> capture. The answer depends on your evaluation strategy. If you never
>> reduce inside a lambda (e.g. call-by-name or call-by-value), then you
>> will always be substituting a closed term in place of a variable, and
>> nothing in a closed term can get captured.
>>
>> However, if by "as many reductions as possible" you mean "to normal
>> form", then you also need to reduce inside lambdas. Then the story is
>> different. Consider the following sequence of beta reductions:
>>
>> (\x. x x) (\y. \z. y z)
>> -> (\y. \z. y z) (\y. \z. y z)
>> -> \z. (\y. \z. y z) z
>> -> \z. \z'. z z'
>>
>> Notice that in the original form, all variable names were unique, but
>> then the variable "z" got duplicated, and the last reduction happened
>> _inside_ the "\z." expression, which required renaming of the inner
>> "z" in order to avoid variable capture and the erroneous result of
>> "\z. \z. z z".
>>
>> Hope this helps.
>>
>
> 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
>
> This *should* of course be
>
>  \z3 -> \z4 -> z3 z4
>
> which is a different function.
>
> 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...)
>
> _______________________________________________