Re: on "strict" MathML

> 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