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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
