Specify binding of variables

[florian-rabe]

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.

[florian-rabe]

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

[florian-rabe]

@kohlhase Your text in #50 seems to describe a third option: parallel binding except bindings do not govern themselves. I think that is objectively worse than my version of parallel binding. For example, it would allow mutual but not single recursion.

[florian-rabe]

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

[JamesHDavenport]

While I appreciate the importance of the issue, is it possible to have a worked example of the difference> I am not sure our colleagues will understand the question without one: I don’t really. James

From: Florian Rabe [mailto:notifications@github.com] Sent: 09 October 2017 15:48 To: OpenMath/OMSTD OMSTD@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: Re: [OpenMath/OMSTD] Specify binding of variables (#64)

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 closest variable binding for the same name that governs B. A variable reference that that is not bound by any variable binding is called a free variable.

However, there is now a fundamental question (as mentioned by @kohlhasehttps://github.com/kohlhase on #30https://github.com/OpenMath/OMSTD/issues/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.)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/OpenMath/OMSTD/issues/64#issuecomment-335180854, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGvamcZcFC_PCG9dp_jwl5_gqXzRqweqks5sqjIRgaJpZM4PykHA.

[kohlhase]

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.

[kohlhase]

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.

[kohlhase]

We have done that. It is part of #50