Definition of alpha conversion underspecified

[kohlhase]

see https://github.com/OpenMath/OM3/issues/1

Florian Rabe reports:

"This object binding (B , v , C ) can be replaced in Ω by binding (B , z , C') where z is a variable not occurring free in C and C' is obtained from C by replacing each free (i.e., not bound by any intermediate binding construct) occurrence of v by z."

1. It is left out what happens if there are variables with attributions. It is reasonable to allow even mutually recursive attributions:

binding(let, attribution(v_1,value -> t_1), attribution(v_2,value -> t_2), C) i.e., let v_1 := t_1 and v_2 := t_2 in C

where t_1 and t_2 may contain v_1 and v_2.

Therefore, alpha conversion must rename variables not only in the scope, but also in all bound variables themselves.

[kohlhase]

This is related to #40 and should be fixed together. Assigning myself to this.

[kohlhase]

For convenience, this is what the OM2R1 standard says about bindings objects

objects are constructed from an OpenMath object, and from a sequence of zero or more variables followed by another OpenMath object. The first OpenMath object is the “binder” object. Arguments 2 to n - 1 are always variables to be bound in the “body” which is the n th (last) argument object. It is allowed to have no bound variables, but the binder object and the body should be present. Binding can be used to express functions or logical statements. The function λ x . x + 2 , in which the variable x is bound by λ , corresponds to a binding object having as binder the OpenMath symbol lambda: binding ( lambda , x , application ( plus , x , 2 ) ) .

Phrasebooks are allowed to use α conversion in order to avoid clashes of variable names. Suppose an object Ω contains an occurrence of the object binding ( B , v , C ) . This object binding ( B , v , C ) can be replaced in Ω by binding ( B , z , C' ) where z is a variable not occurring free in C and C' is obtained from C by replacing each free (i.e., not bound by any intermediate binding construct) occurrence of v by z . This operation preserves the semantics of the object Ω . In the above example, a phrasebook is thus allowed to transform the object to, e.g. binding ( lambda , z , application ( plus , z , 2 ) ) .

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]

I am starting a branch alpha-conversion to address the issues we can in a revision, will push when we have deltas.

[kohlhase]

It is left out what happens if there are variables with attributions. It is reasonable to allow even mutually recursive attributions:

I think that we can fix this by explicitly mentioning attributions in the definition of "bound" and alpha-renaming. I would say that this is just a clarification, since anything else would be unreasonable especially in the presence of semantic attributions which model types, a use case of attributions that is explicitly mentioned on OM2.

[kohlhase]

Fixes will be flowing into pull request #50

[JamesHDavenport]

I agree that it’s underspecified. It’s not clear to me what the ‘right’ semantics are. I’d probably be happy with this as an editors’ revision, though it sounds as if it’s on the big end of the scale. James

From: Michael Kohlhase [mailto:notifications@github.com] Sent: 04 October 2017 08:01 To: OpenMath/OMSTD OMSTD@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: Re: [OpenMath/OMSTD] Definition of alpha conversion underspecified (#30)

It is left out what happens if there are variables with attributions. It is reasonable to allow even mutually recursive attributions:

I think that we can fix this by explicitly mentioning attributions in the definition of "bound" and alpha-renaming. I would say that this is just a clarification, since anything else would be unreasonable especially in the presence of semantic attributions which model types, a use case of attributions that is explicitly mentioned on OM2.

— 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/30#issuecomment-334066844, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGvamZ-Pzm_UY5Fta5iXWWF8cCqQpYS-ks5soy0bgaJpZM4Pqre8.

[kohlhase]

It’s not clear to me what the ‘right’ semantics are.

I have a relatively clear idea by now, but I still have to formulate it.

I’d probably be happy with this as an editors’ revision, though it sounds as if it’s on the big end of the scale.

I think we will have to jointly explore what the borderline between "clarification" and "change" is and stay on this side of it. I.e. do what we can do in R2 and relegate anything disruptive to the futuer.

And I guess the only way of doing that is by making the changes on the branch and seeing whether we feel comfortable with that.

[kohlhase]

I think I have nailed down the semantics of alpha-conversion in the presence of attributed variables. It became quite a lot more complicated. This warrants careful re-reading to make sure that I have not introduced errors. I will get Florian Rabe to look this over too.

[kohlhase]

I have extracted the case of duplicated variables to #53 to keep (related but different) matters separated.

[kohlhase]

A note of warning is in order here. The version of alpha-conversion I have specified in #50 treats all the bound variables of a binding operation as parallel to be able to cover Florian's example

let v_1 := t_1 and v_2 := t_2 in C

from above. In lambda-calculi this is not the prevalent intution; there we treat bound variables as sequential and usually take the following for tranted

lambda x,y C = lambda x (lambda y C)

In particular, if we have a typed variant like lambda x:t,y:s C we usually allow x to appear in s, but not y in t.

Florian's let example often (and very naturally) occurs in advanced programming languages where one wants to allow mutually recursive functions. And I think that we want to allow specifying these in OpenMath (which is why I chose this).

As the bound variable sequence is ordered (even if variable occurrence restrictions are not subjet to this ordering) there is nothing that prevents us to specifying a variable occurrence restriction and the FMP with lambda x,y C = lambda x (lambda y C) in CDs for lambda-calculi like LF.

We may want to discuss this somewhere, maybe in the FAQ as well (I do not think we should burden the standard with these examples).

[florian-rabe]

Using my comments at #64, this can now be easily described by saying that every variable reference bound by the renamed variable binding is renamed accordingly.

[kohlhase]

I have integrated all the comments into #50, which has been cross-checked by Florian, this only needs to be merged. If I do not hear from other editors by Wednesday night I will merge the PR.