Specify binding of variables
Closed this issue · 7 comments
I think issue #30 and #53 are symptoms of a different problem: We have to specify which bound variable an OMV object refers to.
If this is specified, the sections on alpha-conversion and duplicate variables basically write themselves.
Even if we, hypothetically, omit them entirely, people would be able to infer the intended meaning.
We should add in 2.1.3 (iv):
"The (possibly attributed) variables are called variable bindings.
Any other variable object is called a variable reference.
Then we should define in 2.2:
A variable reference R is bound by the variable binding B if R is the closest variable binding for the same name that governs B.
A variable reference that is not bound by any variable binding is called a free variable.
However, there is now a fundamental question (as mentioned by @kohlhase on #30) because we have two options to define govern in 2.2 (subsection on binding objects):
- sequential binding: Each variable binding governs all subsequent arguments of the binding object.
- parallel binding: Each variable binding governs all arguments of the binding object except for the binder.
I prefer sequential binding.
Interpolating the standard, I also believe sequential binding is what the authors had in mind.
But it is worth investigating whether anybody has used or wants to use parallel binding.
(I don't - MMT has always implemented sequential binding.)
The only use case of parallel binding I'm aware so far of is a recursive let binder.
Are there other examples?
If an arbitrary number of children is allowed after the variable bindings in a sequential binding object (which I think is a good idea anyway), recursive let could alternatively be handled by putting the definitions behind the bindings, e.g., binding(let, f: f_type, g:g_type, f_def(f,g), g_def(f,g), O).
I prefer sequential binding.
Interpolating the standard, I also believe sequential binding is what the authors had in mind.
@florian-rabe, I have implemented your suggestions of definitions in 2.1.3 and 2.2. and am changing to sequential binding. I am (now) convinced by your argument
If an arbitrary number of children is allowed after the variable bindings in a sequential binding object (which I think is a good idea anyway), recursive let could alternatively be handled by putting the definitions behind the bindings, e.g., binding(let, f: f_type, g:g_type, f_def(f,g), g_def(f,g), O).
This is probably how we should handle recursive let.
I have integrated another set of changes suggested by @florian-rabe. In particular, we discussed that the proposed deprecation of duplicate variables is overblown in the light that alpha-conversion is well-defined. We settled for "discouraged".
Also, we have settled for a rather conventional sequential reading of bound variables, which does not cover the recursive let example and leave covering that to the future (with a multi-body-binder exetnsion of OM).
Florian will make another reading through the changes and then I think that #50 is ready to go (and much less controversial, than intermediate versions).
It would be great, if we could adopt this soon, so that we can make progress towards OM2r2.