[om] DefMP elements. Is OM Turing equivalent?

[Richard Fateman]

What is a non-recursive definition of Lisp Symbolic Expression  (s-exp)?
The usual one looks like this:

An s-exp is an atom
 or a dotted pair (x . y)   where x and y are each s-exp's.

If you want to require a non-recursive definition, then it seems you cannot
define s-exps. 

I believe that one can encode OM in Lisp,
but if I am correct, one cannot encode Lisp in a non-recursive FMP for OM. 

(I guess this raises the question:  "Is OM Turing equivalent?" If so
there are undecidability problems regardless, and forbidding
recursion here is pointless.  If OM is NOT Turing equivalent, what
does it say about its power relative to other formalisms? )

Yours in argumentation,
RJF



Mike Dewar wrote:

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

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