[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



More information about the Om mailing list