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

[Miguel Mitrofanov]

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