[om] DefMP elements

[Jacques Carette]

I find that Andreas Strotmann's email eloquently voices many concerns that
are similar to mine.  Thanks!

To elaborate on a few points:

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

This is my position now too.

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

Thank you so much for this example - I think that will really help the
discussion.

The above points to a real (thorny) issue: many simple concepts (like sin)
have many equivalent definitions, in the usual context.  However these
definitions do not uniformly generalize, and in fact give different concepts
when generalized.  They all 'collapse' to something equivalent when
specialized.  So it does not make sense to pick one definition over another,
as the context matters too much.

I call this the 'Bourbaki syndrome': trying to come up with universal,
most-general definitions for any concept in mathematics.  I think that the
history of mathematics contains enough precedent to clearly show that this
is futile.  It would be much wiser to embrace this fact right into the
design of OM instead of trying to skirt around it.

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

I completely agree with this claim.  My experience within Maple directly
supports it too - many a difficulty is created because one piece of code
uses one definition of a concept which later turns out to incorrectly
generalize to a different context.

On the specific recommendations:
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
===========
I definitely agree with those first 3.

As to the fourth:
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.
============
Could you be more precise?  I believe I agree, but perhaps an example would
help a lot.

My understanding is you mean for the definition to explicitly mention the
concepts it needs defined for it to be meaningful.  So a complex definition
of exp would need the notions of complex numbers, series, convergence over
the complex, to exist.  This would be a nasty looking signature if expanded,
but if it is expressed all in terms of CD references, it would probably be
quite compact.

On the other hand, aren't you saying that perhaps OMDoc should be that
'main' method of communication, and OpenMath serving OMDoc in the same way
that XML serves OpenMath?

Jacques

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