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

Date: Thu, 14 May 2009 22:15:17 +0100

Message-Id: <200905142115.n4ELFHSE010392@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

Date: Thu, 14 May 2009 22:15:17 +0100

Message-Id: <200905142115.n4ELFHSE010392@edinburgh.nag.co.uk>

To: andreas.strotmann@ualberta.ca

Cc: www-math@w3.org

> 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. > Good example. In my interpretation, differentiation is done over > function spaces, In the version on the current draft, the differention operator does apply to the function space (a lambda term) but the resulting function is re-applied to the variables to make them free again. > It was my understanding from the time that OM2 was being defined that > one of the big changes from OM1 to OM2 implied that something like > ombind(oma(restrict,oma(lift2big,assocop),D),bvar(x),body) (with a > compund head) was no longer allowed, I double checked the OM spec and I see no constraint on the head of a bind. http://www.openmath.org/standard/om20-2004-06-30/omstd20html-2.xml#sec_compound (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. > to use "big" operators instead of "small" ones in strict mathml because > they'd be heads of a bind construct. 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. 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 Thursday, 14 May 2009 21:16:06 UTC

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