Re: on "strict" MathML

> The only reason why this argument applies to MathML at all is that you made 
> the grave mistake of importing alpha-conversion from OpenMath into
> MathML. 

It seems to me that alpha conversion is just another name for binding To
say a variable is bound is to say that it only has local scope, and that
consequently its name can be changed consistently in that scope, ie
alpha conversion.

The intention is to not change the interpretation of any mathml2
construct. The mappings to OpenMath/Strict MathML are just added to
chapter 4 to clarify and simplify the exposition. Having the definition
spread over chapter 4 and appendix C in mathml2 proved problematic
as the inconsistencies crept in either within the spec itself or in
people's interpretation of it.


> Importing it into MathML breaks MathML precisely for reasons such as
> your example above. 

There is nothing new here: the fact that bvar is mostly used for bound
variables in MathML but not for all uses of calculus operations has long
been a source of complication when interpreting MathML. The exposition
in The MathML3 draft does not change that interpretation, it just makes
it explicit.



> That said, the polynomials issue is a red herring,

I nearly removed the word "polynomial" from that example to avoid this
comment:-) I could have said "expression" and kept your sin x example.
sin x in MathML that is: <apply><sin/><ci>x</ci></apply>
I don't think there is anything in MathML2 that could justify
interpreting that as meaning the sin function and being the same thing
as <apply><sin/><ci>y</ci></apply>, which appears to be your preferred
interpretation? 

> Just as alpha-conversion, the "role" concept was a mistake when it was first 
> introduced (I argued and voted against it when it was pushed through)

Just because you voted against something doesn't mean it was "pushed
through". Reasonable people can differ and come to different
conclusions.  As it happens I also didn't vote for it (I think) (just as
I definitely voted against OMBind) but (a) that's all history, OpenMath
is what it is, and (b) the role concept doesn't impact really on MathML
(or OpenMath) much at all.  It's just a hook to document the intended
usage of a symbol.

> Roles are responsible for a schizophrenic situation where sum,
> product, int, diff, and all the other MathML symbols that  take bvar
> qualifiers entirely naturally are not allowed, in their OM2
> counterparts, as heads of ombinds, because they are defined as taking a
> functional argument instead there.  

I disagree actually. That restriction doesn't come from the role system
It comes from the convention that a CD can only give symbol one
definition for a fixed arity. The role concept just allows you to name
some of the usages. for example unary and binary minus are two separate
symbols in OM (minus and unary_minus in arith1) they both have the role
"application" so getting rid of role wouldn't allow you to unify these
symbols unless you also got rid of this convention.  Saying that you
can't use a symbol both as an application and a binder is no different
than this.  As I've said previously I wouldn't personally have had
OMBIND or binder symbols and just had a primitive lambda and
consequently always used symbols with application, but that would
still not have allowed the same operator to be used both as a binary and
a "big" operator as they would have different signatures.


> ignore_role being defined in an OM2/MML3 compatibility CD as an
> identity function defined solely for the purpose of working around an
> OpenMath 2 bug. 

I think you are completely overestimating the role of role. It's
sometimes of minor use as documenting the intended use of a symbol, but
it's only mentioned once in the current draft of mathml3 chapter 4 where
it is used (as in OM2) to distinguish whether an annotation has semantic
importance (eg a type attribution) or is simply an informative
annotation (eg rendering or translation to another format) In particular
it plays no part in the mapping to Strict MathML. Certainly I wouldn't
want to elevate it to being implicated in every rewrite as you seem to
suggest.

> PLEASE, do not repeat the mistakes that were made in OpenMath and import them 
> into MathML-Content. It was deliberately kept clean of at least these two 
> bugs, and I at least would hate to see this undone.

No system is perfect, so no doubt there are mistakes in openmath2 and
mathml2 and there will be mistakes in MathMl3, but to try to describe
the mathml3 as some kind of OpenMath takeover of MathML would be to
completely misrepresent what is happening. The Content part of MathML3
is almost identical to that of MathML2 (the only additions being the cd
related attributes as a cd-specific alternative to definitionURL).
If there is any valid MathML2 expression that had a clear semantics
(in particular given the same semantic by chapter 4 and appendix c)
then it should have the same semantic in mathml3 but hopefully it will
be much easier for a reader or implementer to determine that semantic
as it is all specified in one place, in chapter 4 and in a more codified
format. If you find any expression for which that is not the case,
please report it.


The explict alignment with OpenMath is nothing new. The groups designing
OM1/MathML1 and OM2/MathML2 worked hard to keep the languages aligned,
but just documented the alignment outside the spec rather than in it
In for example
http://www.openmath.org/documents/om-mml.pdf
which was the state of the alignment circa 2001.

But having it outside the spec makes it harder to find and harder for
people to rely on. The two major gains that I see in making the
alignment explict in the spec (and in case you are wondering, it wasn't
originally my idea to do so) is that it clarifies the meaning of several
mathml constructs that were previously only implictly defined, and
perhaps more importantly it makes using the csymbol extension mechanism
far more useful. After several years of calm it's heartening to see
quite a lot of activity on content dictionaries again, with "new" groups
not in the origial OM clique specifying symbols in terms of CDs. By
formalising that OM and MathML are using a shared underlying model, this
means that these CD defined symbols are immediately usable in MathML.



> PS: are you sure you want to use apply_to_list for transfinite argument sets?? 
> (This would happen all the time in model theory.)

yes (although it's living dangerously). Basically because the rewrites
have to be entirely structural (and work even if all terms  involved are
just ci with no further semantic information. So whatever
<apply><ci>f<ci><bvar><ci>x</ci></bvar><domainofapplication><ci>D</ci>...
means in terns of OM it has to mean the same thing whatever the various
ci are. the rewrite can't depend on whether the domain D is finite as
that information isn't available. So you just have to ensure that any
symbols used in the translation are sufficienty defined to give the
intended meaning but loosely defined enough to accept any kind of
argument required. 

David






________________________________________________________________________
The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
________________________________________________________________________

Received on Friday, 15 May 2009 22:13:30 UTC