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

[Miguel Mitrofanov]

Correction: I think that one can find an expression that causes name  
clashes anyway, I'm just not certain that there is one that would  
clash independent of whichever order you choose.

On 21 Jun 2009, at 21:12, Miguel Mitrofanov wrote:

> An answer would probably depend on the reductions order you've  
> chosen. Would that do?
>
> (\e -> e (\u -> e (\v -> u))) (\f -> \x -> f x) -- all variables  
> have different names, see?
>
> = (\f -> \x -> f x) (\u -> (\f -> \x -> f x) (\v -> u))
>
> = \x -> (\u -> (\f -> \x -> f x) (\v -> u)) x
>
> = \x -> (\f -> \x -> f x) (\v -> x)
>
> = \x -> \x -> (\v -> x) x -- Ouch!
>
> = \x -> \x -> x
>
> = \x -> id
>
>
> where the real answer is
>
>
> \x -> (\f -> \x -> f x) (\v -> x)
>
> = \x -> (\f -> \y -> f y) (\v -> x)
>
> = \x -> \y -> (\v -> x) y
>
> = \x -> \y -> x
>
> = \x -> const x
>
>
> On 21 Jun 2009, at 20:53, Andrew Coppin wrote:
>
>> OK, so I'm guessing there might be one or two (!) people around  
>> here who know something about the Lambda calculus.
>>
>> I've written a simple interpretter that takes any valid Lambda  
>> expression and performs as many beta reductions as possible. When  
>> the input is first received, all the variables are renamed to be  
>> unique.
>>
>> Question: Does this guarantee that the reduction sequence will  
>> never contain name collisions?
>>
>> I have a sinking feeling that it does not. However, I can find no  
>> counter-example as yet. If somebody here can provide either a proof  
>> or a counter-example, that would be helpful.
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe