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