[om] DefMP elements. Is OM Turing equivalent?
Professor James Davenport
jhd at cs.bath.ac.uk
Thu Dec 4 22:28:31 CET 2003
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
More information about the Om
mailing list