Re: on "strict" MathML

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