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

[Miguel Mitrofanov]

Probably the easiest way to fix this was already proposed by Deniz  
Dogan: de Bruijn indices.

On 21 Jun 2009, at 21:57, Andrew Coppin 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...)
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe