Re: on "strict" MathML

From: Andreas Strotmann <andreas.strotmann@ualberta.ca>
Date: Fri, 15 May 2009 10:33:11 -0600
To: David Carlisle <davidc@nag.co.uk>

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

(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(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