[om] DefMP elements

[Andreas Strotmann]

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 
>>>than 'evaluating'.
>>>      
>>>
>>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 
>not OpenMath.? 
>  
>
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 
(say) sine.

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

>James
>  
>
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.

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