[om] DefMP elements
Professor James Davenport
jhd at cs.bath.ac.uk
Thu Dec 4 17:54:52 CET 2003
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
> >>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
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
> 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?
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
More information about the Om