[om] problem with "role" proposal for OM2
Strotmann at rrz.uni-koeln.de
Wed Nov 19 15:04:57 CET 2003
during my presentations at the Bremen OM workshop I voiced a concern
with an aspect of the "role" concept introduced in the current draft for
OM 2.0. While this problem was discussed there, no agreement as to its
resolution was reached except, perhaps, to invitate me to start a
discussion on this matter in this, wider, forum.
Let me start off by saying that, in principle, I really like the idea of
introducing a "role" concept along the lines proposed in that draft. My
problem is with the practice that has been proposed to go with it.
What I like about the proposal is that it makes it easy to say, in a CD,
"symbol xyz is a binder/attribute/error... symbol". Strangely, perhaps,
there was no proposal to make it easy to say "xyz is a constant/operator
symbol" as well, but that would be a mere editorial problem to fix.
What I do not like about the current proposal is the *interpretation* it
proposes for the statement "xyz is a binder symbol", for example. The
proposal states that a particularly good thing about the new "role"
concept is that it can be interpreted to mean that the binder symbol xyz
in our example *must* no longer appear anywhere in an OM object *except*
as a binder (i.e. the head of a Binding object); an attribute symbol as
the name of an attribution; etc. This would facilitate the writing of
more restrictive modular XML grammars auto-generated from a CD that
would actually go and enforce such syntactic restrictions, the argument
This purely syntactic interpretation of the "role" of a symbol, I
argued, is a Bad Idea (TM).
Here are a few technical problems we would incur:
-- it means we cannot fix the oversight of leaving out "constant" or
"function" roles because we *know* they are not syntactically restricted
to appearing in one particular syntactic position.
-- it means we cannot possibly have a valid OM Object-encoding of any
CD that contains any of those role specs. The Meta CD thus becomes
mostly useless. I'll leave the trivial "proof" as an exercise to the
reader... In brief, any kind of conversation via OpenMath concerning
meta-reasoning about OM objects that involve symbols with roles becomes
-- compatibility with MathML 2.0 becomes a more serious issue, since
revision 2 of that standard does provide for both the functional and the
binder interpretation at least of the binder symbols in the MathML CD
group. (As a reminder, this equivalence roughly corresponds to saying
that Binding(b,x,y,z,e) is semantically equivalent to
Apply(b,Lambda(x,y,z,e)), with an extra bit of complication, easily
taken care of, because OM, unlike MML, does not have a Lambda
constructor but only a lambda binder in some CD).
-- Whole areas of mathematical literature become rather awkward to
represent in OM, namely those that routinely use what I have recently
learned is known as Higher-Order Syntax for quantifier expressions
(using Apply(forall,Lambda(x,P(x))) instead of the more common
Binding(forall,x,P(x)). It may be hard to fathom, but they actually
quantify over quantifiers in such fields of mathematics!
-- As an example, stating rather obvious equalities that have been used
as examples in several of my OM Workshop presentations, such as
existsUniquely := lambda(P, --see my slides for the full expression--)
, becomes difficult because you suddenly need to decide whether to admit
that existsUniquely should normally be used as a quantifier and thus a
binder symbol, and make this defining equation in its FMP section
illegal syntactically, or whether to leave out the crucial information
that it is a binder symbol just so that some group of mathematicians can
However, my main objection is of a philosophical nature that goes to the
core of what OpenMath is meant to be. I believe strongly that OpenMath
is meant to be a way to "say what you mean" when it comes to
mathematical concepts. Thus, an OM object is not just a piece of
syntax, but has a more or less tightly defined semantics associated with
it. Granted, that semantics has been somewhat vague when it came to
binding objects, for example, but at workshops during the last two years
or so (and in my dissertation) I have shown that the simple equivalence
of the functional and the binding use of binders provides an excellent
candidate for a standard semantic interpretation of OM objects -- with
(in fact) several cases (integration, summation, etc.) that rely on this
interpretation readily available already in the current core set of
This approach is exactly equivalent to the one that realizes that
operator symbols may be arguments, too: binders can be used as
operators, too, and as operators, they can appear as arguments, too. In
meta-reasoning about OM objects, *any* OM symbol may be an argument,
including those that usually mark attributions, say.
Unfortunately, the narrow syntactic interpretation of the "role" of a
binder symbol (or any other of those roles) invalidates this approach.
It refuses to recognize that some transformations of OM objects are
semantic-equivalence preserving, and that some of these are necessarily
such that the symbols involved change their syntactic roles without
changing their semantic roles. (f o g)(x) is the same as f(g(x)), and
just because f and g appear in different *syntactic* roles in both
expressions doesn't mean that their *semantic* role is not that of a
function in all cases.
My proposal is therefore very simple: in the descriptions of all
"role"s, change anything that says "a symbol with role R *may only*
appear..." to "a symbol with role R *usually* appears...". The
definition of a standardized "categorial" type system for OpenMath as
proposed in the final chapter of my dissertation would actually allow
one to be a lot more specific about the semantic(!) restrictions that
apply to the context in which such symbols should reasonably appear in,
but the short time frame for publication of OM2 unfortunately makes it
appear unlikely that such a considerably more complex alternative
solution to this problem could be worked out and proven in time.
The price to pay for either solution is that the auto-generated "smart"
XML schemas envisioned for OM CDs cannot be as restrictive syntactically
as was originally hoped. The good news is, such restrictive syntactic
schemas would have disallowed semantically perfectly correct mathematics
from being expressed in its natural form in OpenMath, and we can avoid
this problem before it comes back to haunt us, as eventually it
certainly would. Also, given time and resources, we could actually come
up with a provably correct semantic version of such schemas some day,
probably in the form of a "categorial" type system for OpenMath.
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