[om] DefMP elements

[Mike Dewar]

I think there may be a misunderstanding here, caused perhaps by a poor
choice of terminology.  There is no proposal to forbid recursion across
the board: James' suggestion is that we should have in effect two kinds
of definitions, one which expresses a concept directly in terms of
simpler ones (his "defining FMP" - FMP stands for "Formal Mathematical
Property"), and one which can be used to reduce a concept to simpler
ones through some multi-step process of evaluation (his "evaluating
FMP").  James makes some philosophical distinctions between these two
cases in the paper whose URL I posted earlier in this thread.

Perhaps a better choice of terminology would be "equivalence" for the
first and "definition" for the second but that might be even more
confusing ...

Mike.

On Thu, Dec 04, 2003 at 07:49:22AM -0800, Richard Fateman wrote:
> Why not just say to people defining FMPs that some brain-dead OM
> applications may be unhappy if FMPs are recursive, and so people
> should consider non-recursive ones to be preferred.  I forget
> what FMP stands for, so I may be using the term incorrectly.
> 
> Forbidding recursion seems like a bad idea, and people will
> view it, perhaps correctly, as showing that OM is strictly
> less capable than the systems it is supposed to define.
> 
> In addition to be verbose, complicated, etc.
> 
> RJF
> 
> 
> 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. 
> >  
> >
> >>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.
> >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
> >  
> >
> 
> --
> 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
> 
> ________________________________________________________________________
> This e-mail has been scanned for all viruses by Star Internet. The
> service is powered by MessageLabs. For more information on a proactive
> anti-virus service working around the clock, around the globe, visit:
> http://www.star.net.uk
> ________________________________________________________________________

________________________________________________________________________
This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk
________________________________________________________________________
--
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