[om] DefMP elements

[Professor James Davenport]

On Thu, 4 Dec 2003, Andreas Strotmann wrote:
> 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 
I was thinking of a Pascal phrasebook that replaces sec(x) with 1/cos(x), 
but can't necessarily write Pascal recursive procedures.
> 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'.
> >>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.
No, the DefMP (of either form) to my mnd says much more: that the author 
of the CD is convinced that replacing LHS by RHS is always valid, and no 
information (other than the name in the LHS) is lost. In general, I would 
expect the definition to be in terms of the same Cd, or an intellectually 
prior CD.

None the less, there might be scope for an "alternative-definition" sort 
of FMP, that said 'if you understand the RHS, then this might be a helpful 
definition". 
> 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
--
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