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

Miguel Mitrofanov miguelimo38 at yandex.ru
Sun Jun 21 13:12:18 EDT 2009

```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

\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.
>
> _______________________________________________