[om] Re: OpenMath 2 draft 6c available

Andreas Strotmann Strotmann at rrz.uni-koeln.de
Mon May 17 19:29:13 CEST 2004

Since the corrections that I proposed in November still have not made it
into this draft, here is the proposal again, but in a concrete proposal
for a slight rewording of the document:

A) change the following two paragraphs in 3.1.4 slightly:

> A symbol cannot have more than one role and cannot be used to construct a compound OpenMath
> object in a way which requires a different role (using the definition of construct given earlier in this
> section). This means that one cannot use a symbol which binds some variables to construct, say,
> an application object. However it does not prevent the use of that symbol as an argument in an
> application object (where by argument we mean a child with index greater than 1).

"A symbol cannot have more than one role, and is usually only used to
construct a compound object of the kind specified by its role (using the
definition of "construct" given earlier in this section) rather than
other kinds of objects. As an example, this means that one should
usually use a symbol that binds some variables to construct a binding
object rather than, say, an application object. However it does not
prevent the use of that symbol as an argument in an application object
(where by argument we mean a child with index greater than 1).

"Note that this does not categorically prevent the use of any OpenMath
symbol, regardless of its role, to construct any kind of other OpenMath
object, be it application, attribution, binding, or error object;
however, OpenMath at this point does not specify the meaning of OpenMath
objects constructed using symbols that have a role that does not match
the OpenMath object they are used to construct.

> If no role is indicated then the symbol can be used anywhere. Note that
this is not the same as
> saying that the symbol’s role is constant.

"If no role is indicated then the symbol can be used anywhere, with no
caveat attached. Note that this is not the same as saying that the
symbol’s role is constant."

B) in Appendix C, add the following after the first paragraph ending in:

> Similarly it is possible to use the role
> information contained in the CD to restrict which symbols can be the first child of an OMBIND or the
> odd-numbered children of an OMATP.

"However, this use of the role information is not recommended since no
absolute restrictions are defined in this documenton on where these
symbols may appear."

((One may also add "in principle" to "it is possible".))

C) in appendix F1, first bullet, make the following slight changes:

> OpenMath symbols have an optional role qualifier which restricts the place where they may
> occur within compound objects.

"OpenMath symbols have an optional role qualifier which represents a
recommendation for the place where they may occur within compound objects."

> In the XML encoding it may be used to provide
> a more restricted schema leading to tighter validation.

"In the XML encoding it may be used to provide
a more restricted schema leading to tighter validation, but this use is
not recommended in general."

-------

Rationale: I have given ample samples over the last two years' worth of
OpenMath meetings that show where, at the very least, symbols with
"binder" roles and those with "apply" roles may reasonably appear as
"heads" of both application and binding objects.  Indeed, an entire
chapter of my dissertation argues that allowing this is actually
*necessary* if one wants to define a reasonably complete semantics or
type system for OpenMath eventually; a sample such type system is given
in the same chapter to make the point, and a brief version of that
chapter has just been submitted to MKM'04.

I would find it unreasonable to simply ignore research that clearly
argues that the original versions of the above text passages are *wrong*
in an important way, given that they can be fixed as easily as shown here.

I realize that there is a minor inconvenience that is re-introduced by
the changes proposed here, in that binder symbols, for example, may not
be relied upon one hundred percent to only appear as syntactic binders
(or arguments).  However, as I said, I have previously provided ample
evidence both in the OpenMath and in the MathML community that this is
the way life actually is like out there in the real world of
mathematics, and applications that cannot handle this extra complication
are still free to use the techniques mentioned in both the original and
in the corrected versions of these text passages and use syntactic
restrictions for this purpose -- just like applications I have seen that
cannot handle "\pi * x = 2 * \pi" as a linear equation because they
insist that those have to have the form of a sum of products of a number
and a variable on the left side of the equation, with a number on the
right side of the equation.

-- Andreas

--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems