What is the status of / authority for the principle that an OMBIND does not
cause the variables to become bound in its first child? I thought it was
explicit in the standard, but now that I look for it, then the closest match
I find is the following two passages on page 12 of the standard:
... 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 nth argument
object. ...
... 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 Ω. ...
It sort-of follows from this, but rather indirectly. On the other hand I see
in Davenport & Kohlhase (Unifying Math Ontologies: A tale of two standards,
2009, p. 12) the passage
... the OpenMath2 dictum that the binding operator is not subject
to α-conversion by its own variables ...
which makes me trust my memory of the issue. Still, I don't quite see this
"dictum" spelt out in the standard. So where would one have picked it up?
Lars Hellström
[*] Actually, now that I reread this sentence, it occurs to me that it is
slightly wrong. It's not sufficient that z does not occur /free/, since some
v might occur free in a context where z is bound. Ah, the quagmire of
variable binding... :-)
_______________________________________________
Om mailing list
[email protected]
http://openmath.org/mailman/listinfo/om
