Clarifying and partially fixing alpha-conversion and bound variables in OM2

[kohlhase]

This pull request contains the fixes for #30 and #40. As this is a complex topic, this will require multiple commits.

It is still under development, so do not merge it yet, but possibly give early feedback as the commits flow in.

[kohlhase]

I have updated this PR to the trunk and think it is ready to go. @davidcarlisle could you please have a look and merge if you like it?

[kohlhase]

BTW, the change is so large, since I had to (manually) format the MathML to make sense of it while editing.

[florian-rabe]

I'm commenting on #53:

Using my definitions in #64, #53 can be resolved easily. However, as described in #64, we have to choose between two options. Depending on the choice, the resolution to #53 varies:

• sequential binding: Duplicate variables are not a problem anymore because their semantics is clearly specified. They are usually pointless but should be allowed. The remark "Repeated occurrences of the same variable in a binding operator ..." in the standard should be revised to clarify that it is just an example of a consequence of the definition of binding and alpha-conversion. It could read "... are allowed but rarely useful: By applying alpha-conversion, we see that binding(B,x,y,x,O) (where all variable bindings are unattributed) is equivalent to binding(B,x',y,x,O) for a fresh variable x'. Duplicate bindings are only useful in the presence of attributed variable bindings. For example, in binding(B,x,attribution(y, k1, V1), attribution(x,k2,V2),O), the first binding of x still binds references to x in V1 and V2. This is typically avoided in human-written content but may occasionally come up in machine-generated content."
• parallel binding: Duplicate variables should be forbidden.

[florian-rabe]

Michael asked about variants of parallel binding that do not forbid duplicate variables. Here's one option:

In a binding object, essentially all variable bindings govern each other. The precise definition is more technical because it has to cover the case where the same variable name is bound multiple times in the same binding object: In a binding object with variable bindings b_1, ..., b_n, the variable reference bi governs the list of variable bindings that results from cutting off b{i+1}, ..., b_n, b_1, ..., b_i after the first binding with the same name as b_i.

This somewhat convoluted definition has the effect that the following examples work:

• singly or mutually recursive bindings without duplicates variable names, e.g., let x=f(y), y=g(x) in O
• sequential bindings with shadowing semantics for duplicate variable names, e.g., let x = 1, x=x+1 in x (which evaluates to 2)

However, it has the serious drawback that it does not work if the same variable name is used in nested binding objects, e.g., in let x = 1 in let x = x+1 in x the second binding of x would falsely be interpreted as a recursion.