Correction: I think that one can find an expression that causes name clashes anyway, I'm just not certain that there is one that would clash independent of whichever order you choose. On 21 Jun 2009, at 21:12, Miguel Mitrofanov wrote:

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

Wow. Now you've showed it to me, it seems pretty obvious. That's what I like about math. On 21 Jun 2009, at 21:56, Bertram Felgenhauer wrote:

Miguel Mitrofanov wrote:

...

Correction: I think that one can find an expression that causes name clashes anyway, I'm just not certain that there is one that would clash independent of whichever order you choose.

Yes there is.

Consider

(\f g -> f (f (f (f (f (f g)))))) (\l a b -> l (b a)) (\x -> x)

which has 6 variables in total. This reduces to the normal form

\a b c d e f g -> g (f (e (d (c (b a)))))

which requires 7 variables. So without alpha-conversion at least one of the original 6 variables will clash with itself.

Bertram _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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...)

Andrew Coppin wrote:

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

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...)

I knew alpha conversions were trixy little things! ;-) Well anyway, the obvious thing to do is after each reduction, strip off all the variable indicies and rerun the labeller to assign new indicies. But does this solution work properly in general? The labeller is carefully crafted to respect scoping, so that for example "\x -> x (\x -> x) x" becomes "\x1 -> x1 (\x2 -> x2) x1". But still, the final expression above is nicely labelled, yet wrong. How does this happen? Well, variable indicies are supposed to be unique. But in line 2 we see a bunch of them get duplicated. At this point, if you strip all the indicies and recompute them, you get (\y1 -> \z2 -> y1 z2) (\y3 -> \z4 -> y3 z4) There are now no spurious duplicates, and the reduction should proceed through the remaining steps without incident. So rerunning the labeller works *for this example*. But does it work in general? As an alternative, I could completely reprogram my entire application to use de Bruijn indices. Hmm...

On Sun, Jun 21, 2009 at 07:48:30PM +0100, Andrew Coppin wrote:

Andrew Coppin wrote:

...

Well anyway, the obvious thing to do is after each reduction, strip off all the variable indicies and rerun the labeller to assign new indicies. But does this solution work properly in general?

No.

Supposing some Lambda expression eventually reduces to, say,

\x1 -> \x2 -> x1 x2

Now strip off all the indicies:

\x -> \x -> x x

...and recompute them...

\x1 -> \x2 -> x2 x2

FAIL.

To make it worth properly, I would have to (at least) make the renamer respect any indicies which are already present. It's nontrivial, but doable. Of course, the £1,643,264 question is... would it work even then?

I reiterate the pointers to reading material that I gave earlier. A lot of really smart people have spent a lot of time thinking about this already; it's likely not worth any more of your time to try figuring it out yourself. (It's definitely worth some initial time struggling with it, so that you can properly appreciate the solutions---but it sounds like you've already done that!) Briefly, the key operation is substitution---*while* doing a substitution you have to somehow check that names aren't clashing, and possibly rename some things if necessary (or if using de Bruijn indices, you may need to shift some indices around while doing substitution). If you wait until *after* doing a substitution to fix up the names, it's too late. But don't take my word for it, go read about it somewhere. =) -Brent