From: David Carlisle <davidc@nag.co.uk>

Date: Fri, 15 May 2009 23:12:54 +0100

Message-Id: <200905152212.n4FMCs9T012540@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

Date: Fri, 15 May 2009 23:12:54 +0100

Message-Id: <200905152212.n4FMCs9T012540@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

> 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

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:27:41 UTC
*