AlphaConversion parameter renaming feature is broken

[hexwell]

I was working on adding lazy evaluation to Nameless and I came across this:

$ python2 nameless

nameless!
Type 'quit' to exit.
> (λa.λb.a λb.b)
(λa.λb.a λb.b)
λb.λb.b

Looks like the parameter name conflict is not detected

[hexwell]

This seems to boil down to a variable identity issue:

The problem is due to absence of parameter name conflicts checks against bound variables of the replacement in AlphaConversion of Abstraction.

It could be solved by expanding the set of unavailable names using the BoundVariables visitor, but in it, bound variables of an application are defined as so:

BV((e1 e2)) = BV(e1) ⋃ BV(e2)

This raises another problem, if any variable of e1 has the same name of a variable of e2 they are incorrectly treated as the same variable by AlphaConversion of Variable, and thus both substituted with the same replacement.

[hexwell]

I'm writing this for the record and for future reference after having fixed the issue.

There are two issues at play here:

The first one is mentioned in the title and it's about the parameter rename feature.
It is the easier of the two to understand, and it is the one fixed by my PR.

I proposed a partial solution to this in my previous comment:

Extending the set of unavailable names in AlphaConversion of Abstraction using the BoundVariables visitor on the replacement.

However this is not sufficient, because there is a chance that the new name chosen for the parameter conflicts with the name of the parameter of an outer abstraction.

To solve this, a set of unavailable names was added as an attribute to the AlphaConversion class, and it was used to further extend the set of unavailable names.

When a rename occurs, before recursing down the tree, the chosen new name is added to the set, so that it is marked unavailable for all further nested expressions.

What happened before is that, if by chance a new name that clashed with the name of the parameter of an outer abstraction was chosen, the resulting expression had two or more nested abstractions with the same parameter names.

This leads to the the second issue, the one I referred to previously as "a variable identity issue", that I described here:

if any variable of e1 has the same name of a variable of e2 they are incorrectly treated as the same variable by AlphaConversion of Variable

It turned out that the issue was about distinguishing between parameter declaration and variable use rather than about variable identity (variable identity being: distinguishing between a) different variables, bound by distinct abstractions, but having the same name, and b) occurrences of the same variable bound by the same abstraction. I'm interpreting my own writing a bit here, I might have been on the wrong path, or I might have been on the right track and have used slightly misleading language).

What this means practically is that if an expression has two or more nested abstractions having parameters with the same name (homonymous), AlphaConversion of Variable replaces both the parameter declaration and the occurrences, resulting in a rather confusing, illegal and ultimately wrong expression.

e.g.

> (λa.λa.x λb.b)
(λa.λa.x λb.b)
λλb.b.x

This second issue is actually still present and was not fixed.

I reckon that the escape route of declaring such inputs (nested abstractions with homonymous parameters (shadowing)) outside of the domain of the interpreter / illegal, and therefore undefined / producing undefined behavior can be used to avoid fixing it.

If the input is valid, I believe that with my fix the interpreter won't generate such incorrect expressions by itself anymore.