[om] DefMP elements

[Andreas Strotmann]

Professor James Davenport wrote:

>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.
>  
>
If you replace Pascal with Fortran, you have a point, but that's a very 
unlikely candidate for digesting OM CDs, I would have thought.

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

However, I think both should be called "definition". It may be useful to 
add modifiers to that word, such as "simple definition" or "recursive 
definition" or "constructive" vs. "existential" "definition" etc., but 
they should all be called "definition". In addition, "definition" 
without a modifier should be a generic term that can mean any of the 
pre-defined modified forms -- and as such should not be restricted to 
appearing at most once.

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

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

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.

c)  In the context of an algebraic analysis of robot arm movement the 
replacement would wreak total havoc, turning an algebraic problem into a 
transcendental one.

And this doesn't even come close, I suspect, to the problems you'd run 
into trying to find a proper "definition" for exp...

In summary, I'd be *extremely* reluctant to take anybody's word for it 
that a given mathematical concept can be replaced, without loss, by a 
simple formula in *absolutely all* cases. Mathematicians are just too 
prone to, and inventive in, generalizing mathematical concepts beyond 
their original scope -- "sine" being a truly excellent case in point.

Like a pope once said -- he might not completely rule out that somebody 
in his place might be able to make a once-and-for-all-true statement "ex 
cathedra", but he himself didn't quite believe himself capable of that 
remarkable feat.

>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". 
>  
>
That is a good point. To paraphrase what I said above, I think 
"alternative-definition" should simply be called "definition", and other 
special cases of definitions (simple, recursive, approximative, 
implicit,...) should use "xyz-definition" or something of the sort.

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