From: Andreas Strotmann <andreas.strotmann@ualberta.ca>

Date: Fri, 15 May 2009 10:33:11 -0600

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

Cc: www-math@w3.org

Message-Id: <200905151033.12161.andreas.strotmann@ualberta.ca>

Date: Fri, 15 May 2009 10:33:11 -0600

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

Cc: www-math@w3.org

Message-Id: <200905151033.12161.andreas.strotmann@ualberta.ca>

On Thursday 14 May 2009 03:15:17 pm David Carlisle wrote: > > is, that cos x is simply a shorthand for the function lambda x. cos > > x. > > sometines it is in natural language disussion of mathematics but mathml > can't take that view. Take polynomials for example, the polynomials x^2 > and y^2 are distinct entities if considered as polynomials, although > either can colloquially be used to represent the squaring function. > d/dx of x^2 is the poynomial 2x, not the polynomial 2y. You can't make > that distinction if you view d/dx x^2 as syntax for d/dx (lambda x. x^2) > I don't believe that such an interpretation would be compatible with > MathML 1 or 2. 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. I have long argued (since my suggested resolution to the fatal ombind definition error that got dealt with in OM1.1) that defining alpha-conversion at the syntactic level, as OpenMath does, is a serious offense against separation of syntax and semantics and should be removed. Importing it into MathML breaks MathML precisely for reasons such as your example above. That said, the polynomials issue is a red herring, I think, caused by faulty representations of polynomials, and by abuse of the functional notation for a structure that is not cleanly functional. A proper representation of a polynomial would be something more like P(base_ring_or_field,list_of_extension_symbols,polynomial_as_function) accompanied by the definition that diff(P(a,b,c)) = P(a,b,diff(c)) You need this because otherwise constant members of the polynomial ring stop being polynomials (a famous source of ambiguity in CA systems), and you would not be able to tell that 2x is actually a polynomial in x,y, and z, for example. Note that there is no problem with a purely functional notation, and even with alpha-conversion, if you have a representation like this, as the names of symbols that define the polynomial ring are not affected by conversion. When I took algebra 25-odd years ago, I was struck by the definition of a polynomial ring, where a base ring was extended by *symbols* x,y,z (not variables!) with the one defining condition that the symbols be transcendental wrt. the underlying ring (\Q[\pi] was thus quoted as a perfectly fine example). The use of variables instead of symbols violates the transcendence condition as they do range over the base ring - hence the word list_of_extension_symbols above. > > (iv) If B and C are OpenMath objects, and > v1,.., vn are OpenMath variables or attributed > variables, then > > binding (B, v1, ..., vn, C) > > is an OpenMath binding object. > > > Note B is an arbitrary object. > > a given symbol in openmath is only supposed to have one role (and one > arity) so if (in OM2) a particular symbol is a binary operator (say > union) you are not supposed to use that symbol of a head term of > something else (a binder or an apply woth multiple arguments.) > the result is a legal openmath term but just doesn't evaluate. > However there is nothing to stop you _constructing_ an object out of > that symbol which is then used as the head. (although that isn't > actually how we ended up modelling the big operators, see the > predicate_on_list usage in the editor's draft. Thank you for clearing this up for me - it's been a while since I checked. So let me clarify what I had in mind then: 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), and it utterly breaks MathML as we designed it in 2003. As in the case of alpha- conversion, I strongly advise against importing it into MathML from OpenMath - it's yet another example of violating the principle of separation of powers between syntax and semantics. 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. (In my MKM'04 paper and in my '03 dissertation, I proposed a much better, purely semantic, approach to the problem that "role" appears to be designed to resolve, in which the duality between an operator over functional arguments and a homonymous binder symbol is resolved completely naturally, with a single common signature for that single symbol (and thus a possible solution even within the strict limit of one signature per symbol imposed by OpenMath CDs). It also restricts compound binders to sensible ones quite naturally.) Since you have to "align" with OpenMath 2, though, I propose you generate ombind(oma(ignore_role,head),bvar(...),body) from MathML instead of ombind(head,bvar(...),body) as a matter of principle, 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. (You may need to do the same thing to oma heads to allow oma(forall,ombind(lambda...)), which is also perfectly fine in its MathML incarnation.) 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. -- Andreas PS: are you sure you want to use apply_to_list for transfinite argument sets?? (This would happen all the time in model theory.)Received on Friday, 15 May 2009 16:33:33 UTC

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