[om] DefMP elements
Strotmann at rrz.uni-koeln.de
Mon Dec 8 11:26:32 CET 2003
Professor James Davenport wrote:
>On Thu, 4 Dec 2003, Andreas Strotmann wrote:
>>Professor James Davenport wrote:
>>>On Thu, 4 Dec 2003, Andreas Strotmann wrote:
>>>>Professor James Davenport wrote:
>>>>definition of functions, be it factorials or Ackermann functions. I
>>>>believe that we should take serious the advice of previous posts that
>>>>this restriction would essentially cripple DefMP.
>>>It cripples ONE FORM OF DefMP, the type that is explcitly declared to be
>>>non-recursive. Mayve the other sort should be called 'recursive' rathen
>>You're right -- my mistake.
>I want to make a simplistic phrasebook easy to implement.
>Maybe I chose the wrong words, but if ML can have "let" and "letrec", why
Certainly. I think we are now basically in agreement that classifying
definitions, given an intuitive naming, is a good thing. However, we are
not at all in agreement about whether only allowing unique definitions
in any given class of definitions is a good thing.
>>I'm rather sceptical that this is feasible at all, except perhaps in
>>extremely simple cases (csc might be one such case, but given the
>>content of your "uncouth" SIGSAM paper, I'm sceptical even in this case
>>that you wouldn't have to go through some special process of defining
>>the complex domain of csc that would go beyond the simple sample
>>definition in your DefMP paper.)
Followup on this one -- here's an example where your definition would be
wrong(!!!): It's in systems of ODEs, if I recall correctly (it's been a
long time, I admit), that you can find the concept of (say) the sine of
a square matrix, which makes sense for two reasons: they're involved in
solutions to ODEs of the same kind that is solved by the real function
sin, and they can be calculated using the power series expansion of
csc of a square matrix can also be defined (within limits) by a suitable
power series expansion, with suitable properties to match. However,
this cannot be the same as the definition of csc as a quotient as in
your example, because csc of a square matrix can exist for matrices that
do not have an inverse (and using the transpose instead of an inverse
gives the wrong results, I suspect). Examples to try include
((1/2,1/2),(1/2,1/2)) and ((0,1),(0,1)) (idem-potent matrices making it
easier to calculate the series).
>>In particular, I don't think that the definition of sine in terms of exp
>>in your paper meets this requirement:
>>a) It would *not* be OK to make that replacement in the context of a
>>high-school geometry textbook, where sin and cos are perfectly well
>>defined in terms of quotients of lengths of sides of triangles, but exp
>>is still several years ahead, completely outside the scope of geometry
>>in fact (and therefore anything but intellectually prior).
>But then the application understands sin/cos.
That is beside the point, James. The point is that a definition
usually(?) isn't universally applicable; contrary to your claim, some of
those you give as examples are indeed incorrect given the right kind of
reasonable context. But universal applicability is what you claim a
DefMP should claim: what I say is that it cannot possibly claim that.
>>b) I would even argue that that replacement is not even OK in the
>>context of real analysis, since it involves complex numbers, which are
>>not intellectually prior either.
Indeed, I personally ran across exactly this problem when we implemented
the first (as far as I know) "real" OpenMath application with Ph.Marti
at U.Nice/ESSI way back: Maple insisted on solving systems of polynomial
equations over the complex numbers, but when you're in the business of
solving systems of real inequalities, this can crash the other
cooperating software systems. Morale: defining real functions in terms
of complex ones is dangerous for the health of an OpenMath application...
I stand by my claim: it is not reasonable to expect any single
definition of a mathematical concept to be universally applicable; much
less is it reasonable to expect any single definition to be universally
useful, be it ever so simple or efficiently computable. A definition, I
believe, cannot be anything except *a* definition: one of many possible
or useful ones that a concept can be reduced to, given the right context.
If you take a closer look at my examples, you may notice that a good
part of the problem is that you do not propose to attach a signature to
your definitions, ending up defining a real function via the complexes
(which is fine if your application is knowledgable enough about the
complex numbers, but a terrible idea if it has no idea whatsoever about
them). The csc problem rests in the fact that you need a definition that
also works for rings, not just fields. However, from a purely
philosophical point of view, I'd still be sceptical about meeting your
stringent requirements even if you did parametrize definitions by
signature: I can still think of several definitions for real exp that
are not trivially equivalent.
As you noted, Jacques' solution is not the preferred one either -- in
all these cases, the concept sine or csc was generalized in a way that
actually works perfectly fine with some (but not all) of the fundamental
K-13 (i.e. MathML) definitions of the concept, so that there is really
no need to introduce any extra versions in separate CDs.
In summary, therefore, my recommendation would be:
a) rename the different classifications of definitions so that they all
contain the word "definition"
b) the name "definition" by itself should name the most general class of
definitions, not the most restrictive
c) do not *require* (but *do* recommend!) that definitions be unique (or
at least that different definitions not be trivially equivalent) --
within any class of definitions
d) use signatures in definitions: this might prevent a definition from
being misapplied in an application that doesn't know any better. This
may well be done in the simple way of using universal quantifiers and
set memberships inside the defining FMPs, so that this may simply be
added as a recommendation to CD writers.
om at openmath.org - general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems
More information about the Om