[Haskell-cafe] Slightly off-topic: Lambda calculus
thomas.dubuisson at gmail.com
Sun Jun 21 21:04:25 EDT 2009
Just as ancillary information: ∃ a calculator on Hackage called
"LambdaCalculator". Its rather short (loc wise) and fun to play with.
On Sun, Jun 21, 2009 at 10:57 AM, Andrew
Coppin<andrewcoppin at btinternet.com> wrote:
> Lauri Alanko wrote:
>> 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.
> Ladies and gentlemen, we have a counter-example!
> (\x1 -> x1 x1) (\y2 -> \z3 -> y2 z3)
> (\y2 -> \z3 -> y2 z3) (\y2 -> \z3 -> y2 z3)
> \z3 -> (\y2 -> \z3 -> y2 z3) z3
> \z3 -> \z3 -> z3 z3
> This *should* of course be
> \z3 -> \z4 -> z3 z4
> which is a different function.
> Now the operative question becomes... how in the name of God to I fix this?
> (The obvious approach would be to rerun the renamer; but would discarding
> the variable indicies introduce even more ambiguity? Hmm...)
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe