[om] DefMP elements

[Jacques Carette]

> Aha - a misunderstanding. OpenMath's (in my proposal) FMPs have a
> `defining` role, that says that textual replacement will eliminate the
> named symbol. Clearly, this can't allow recursion.

Maybe what you are looking for here is what the logicians call a
''conservative extension'' mechanism?  This allows one to introduce lots of
new definitions, but no effective new power.  Of course conservative
extensions can be so simple that all you need is term-rewriting to take them
out, and that is a fairly common case indeed, but not all.

I said:
> In some important cases (see the lambda-calculus literature, or say the
work
> around OBJ3 and co-algebraic specifications), allowing recursion in
defining
> FMPs would allow one to write down definitions from which important
> consequences follow easily; note that a corresponding evaluating FMP may
not
> use recusion at all, because that may well put it in the 'wrong'
complexity
> class!

You replied:
> This one I don't follow.

All I meant to say is that there are a number of formalisms that use
non-terminating recursion to define infinite objects (like Streams).  These
same formalisms are used to define the semantics of OO languages cleanly in
a purely mathematical way.

In any case, I like the idea of calling them all 'definitions' and having
several flavours (like let/letrec) which can warn OM applications of the
complexity of the definition.  Using 'recursive' instead of 'evaluating'
seems like a definite improvement.

Jacques

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