clarify (and possibly fix) duplicate variables.

[kohlhase]

Excerpted from #30 (and ultimately from OpenMath/OM3#1): Florian Rabe reports:

2. The case of duplicate variables is unclear, too. What happens if a variable occurs twice, but with different attributions? And what happens to binding(b, x, attribution(y, k -> x), x, C)?

I think duplicate bound variable should be forbidden. They are intended to be pointless anyway.

[kohlhase]

I think duplicate bound variable should be forbidden. They are intended to be pointless anyway.

I would love to do that, but I am not sure that we can do this in a revision like R1, since it would make some valid OM invalid. I can imagine to say that duplicated variables are "strongly discouraged, since they are intended to be pointless", and then say what they would mean via alpha-renaming (if we can puzzle out Florian's examples).

[kohlhase]

Assigning to David, James, and myself to give this exposure.

[kohlhase]

For convenience, here is the relevant passage from OM2

Repeated occurrences of the same variable in a binding operator are allowed. An OpenMath application should treat a binding with multiple occurrences of the same variable as equivalent to the binding in which all but the last occurrence of each variable is replaced by a new variable which does not occur free in the body of the binding. binding (lambda, v , v ,application (times,v ,v) ) is semantically equivalent to: binding (lambda , v' , v ,application (times,v ,v) ) so that the resulting function is actually a constant in its first argument (v' does not occur free In the body application (times,v ,v) )).

[kohlhase]

This has a left-to-right procedural semantics, which is extremely ugly, but possible. I think this can be updated to include attributed variables. The idea is that

binding(B,u,x:a,v,x,w,C) where u,v,w are (possibly empty) sequences of bound variables, where u and v do not have head x, and a is the attribute sequence of the attributed variable x.

is repaced by binding (B,u',x':a',v',x,w,C), where -- and now we have three possibilities --

1. u', a', and v' are obtained from u, a, and v by replacing x by x',
2. v'=v and u' and a' are obtained from u and a by replacing x by x',
3. u'=u, v'=v, and a' is obtained from a by replacing x by x, or
4. u'=u, v'=v, and a'=a. I am not sure which one is best, I think we are essentially free to choose. Probably I would go for 2. as this is most in keeping with the left-to-right spirit of this disambiguation rule.

All in all I find this soooo ugly that I would much rather forbid duplicate variables (in one binding; the across-binding case is unproblematic by alpha-conversion).

[kohlhase]

If I do not hear from anyone until Sunday, I will implement 2. in #50 and consider the PR completed and ready for feedback on monday.

[JamesHDavenport]

Apologies – I don’t understand what 2. Is – I don’t see choices in #50.

From: Michael Kohlhase [mailto:notifications@github.com] Sent: 06 October 2017 15:17 To: OpenMath/OMSTD OMSTD@noreply.github.com Cc: James Davenport J.H.Davenport@bath.ac.uk; Assign assign@noreply.github.com Subject: Re: [OpenMath/OMSTD] clarify (and possibly fix) duplicate variables. (#53)

If I do not hear from anyone until Sunday, I will implement 2. in #50https://github.com/OpenMath/OMSTD/pull/50 and consider the PR completed and ready for feedback on monday.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/OpenMath/OMSTD/issues/53#issuecomment-334767903, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGvamVTE9kB8Sk767ewTOT1r94OSVPcEks5spjZmgaJpZM4PukTQ.

[kohlhase]

Apologies – I don’t understand what 2. Is – I don’t see choices in #50.

2. is item 2. in binding(B,u,x:a,v,x,w,C) where u,v,w are (possibly empty) sequences of bound variables, where u and v do not have head x, and a is the attribute sequence of the attributed variable x is repaced by binding (B,u',x':a',v',x,w,C), where -- and now we have three possibilities --

3. u', a', and v' are obtained from u, a, and v by replacing x by x',

4. v'=v and u' and a' are obtained from u and a by replacing x by x',

5. u'=u, v'=v, and a' is obtained from a by replacing x by x, or

6. u'=u, v'=v, and a'=a. I am not sure which one is best, I think we are essentially free to choose. Probably I would go for 2. as this is most in keeping with the left-to-right spirit of this disambiguation rule.

And you are right, I had not extended #50 with the respective specification (sorry forgot). But while I wrote it up, I changed my mind, and specified 3.

As I said, the choice is somewhat arbitrary, but should be made. In any case, it only applies to very obscure cases; and with the (proposed) deprecation we should not be getting new ones.

[kohlhase]

OK, closing this, all discussion should move to #50