[Haskell-cafe] Slightly off-topic: Lambda calculus
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
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
> 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
More information about the Haskell-Cafe