[om] DefMP elements

[Andreas Strotmann]

Professor James Davenport wrote:

>On Wed, 3 Dec 2003, Bill Naylor wrote:
>  
>
>>1) Dissallowing self reference during a defining FMP, therefore
>>dissallowing recursive definition.
>>    
>>
>Quite so, in a defining FMP. An evaluating FMP does allow recursive 
>references. The distinction is made so that a system knows whether the 
>expansion of the FMP will always terminate, or will only terminate on 
>concrete nstances (and therefore, if the instance is not concrete, a 
>fixed-point operator will be required, which is probably beyond the scope 
>of most OM-capable applications. 
>  
>
I'm not sure I agree here: most OM applications I know of that could 
handle such definitions at all would have no problem with a recursive 
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.

>>2) Dissallowing multiple defining FMPs, therefore dissallowing different
>>but logically equivalent FMPs, e.g. a definition in terms of integrals
>>versus a definition in terms of recurence relations.
>>    
>>
>One could have several FMPs, but the point of the unique defining one is 
>that the author of the CD is saying that this particular FMP can be used 
>to eliminate this concept in favour of "simpler" ones.
>  
>
Yes, but consider sin/cos: which of the umpteen different defining 
relations would you use?  Doesn't that depend on the concrete context?  
In algebraic robotics applications, for example, the defining relation 
c²+s² = 1 may be all you need; in some cases, the differential equation 
would be a preferred DefMP, but then some CA systems don't handle such 
equations all that well; the definition in terms of exponentials is 
another useful one -- in a complex analysis setting, that is; the formal 
power series definition is another one, e.g. for sines of square 
matrices -- but only if your system handles power series well enough; in 
a highschool textbook, let's not forget, the quotient of lengths of 
sides of a certain type of triangles is yet another obvious candidate by 
virtue of being the "original" definition, but it is not going to make 
many CA systems happy.  How do you decide which one to use?!?  The 
equivalences of such definitions are not all trivial, and therefore an 
application that gets one definition, and one only, when it really needs 
one of the others may very well be worse off with than without a DefMP.

My personal stance would be that a DefMP simply states that it provides 
one possible definition of the concept. Multiple DefMPs simply say that 
there are non-trivial alternative definitions, some of them provided for 
convenience, take your pick depending on your needs. Regular FMPs just 
state generic properties that do not necessarily define the concept, 
i.e. that may apply to other concepts, too (e.g. "sine is an odd 
function").  This is a very important distinction to make, one that 
deserves syntactic distinction.

But I do think that that is the only distinction that FMP vs. DefMP 
should encode.

Still, the review process for CDs may well require that DefMPs follow 
certain guidelines to improve their usefulness, but that's all they 
should be: guidelines. Otherwise we'd constantly have to rewrite the 
rules to capture legitimate uses we didn't think of before. "The world 
(of mathematics) is wondrous beyond the ken of (any one) man" -- isn't 
there a famous quote that runs something like that somewhere?

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