[om] problem with "role" proposal for OM2

[Andreas Strotmann]

Dear All,

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 
goes.

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 
decidedly tricky.

 -- 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 
be satisfied.

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 
OpenMath CDs.

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.

Best regards,

 -- 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