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

[Lauri Alanko]

On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin wrote:
> 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?

With "name collisions" I'm assuming you mean inadvertent variable
capture. The answer depends on your evaluation strategy. If you never
reduce inside a lambda (e.g. call-by-name or call-by-value), then you
will always be substituting a closed term in place of a variable, and
nothing in a closed term can get captured.

However, if by "as many reductions as possible" you mean "to normal
form", then you also need to reduce inside lambdas. Then the story is
different. Consider the following sequence of beta reductions:

(\x. x x) (\y. \z. y z)
-> (\y. \z. y z) (\y. \z. y z)
-> \z. (\y. \z. y z) z
-> \z. \z'. z z'

Notice that in the original form, all variable names were unique, but
then the variable "z" got duplicated, and the last reduction happened
_inside_ the "\z." expression, which required renaming of the inner
"z" in order to avoid variable capture and the erroneous result of
"\z. \z. z z".

Hope this helps.


Lauri