[om] DefMP elements. Is OM Turing equivalent?

[Professor James Davenport]

On Thu, 4 Dec 2003, Richard Fateman wrote:
> 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. 
Thi is true, but you can encode it in a recursive one, and what's wrong 
with that for Lisp? 
> (I guess this raises the question:  "Is OM Turing equivalent?" If so
Well, all maths (should be) encodable in OM: there is nothing in the OM 
standard (1) that forbids that.
> 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? )
Maybe I should change "defining" to "eliminating": I don't understand why 
a world that accepts let/letrec can't accept what I wrote, though I admit 
my nomenclature could have been better.
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