[om] DefMP elements

[Jacques Carette]

> I think that the feeling at Bremen was that dissallowing self-reference
> inside a defining FMP was generally a good thing.  Self-reference and
> hence recursion is of course quite legal for the evaluating case.  

Just a note that this goes against a lot of trends in programming languages
(and their semantics), and established wisdom in type theory (and thus
logic), where there are 'too many' semantic objects whose best (and often
only) definition is recursive.  There is a whole community all of whose
tools (algebraic and co-algebraic specifications) all use fundamentally
recursive definitions, even at the concept level.  Not allowing
self-reference in defining objects just means that lots of very natural
objects will not be definable within OpenMath, only externally, which can
get quite tedious.

Since even basic lambda-calculi have fixed-point operators to resolve
recursive definitions, it would be a shame if OpenMath's DefMP could not be
at least that expressive as well.  

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!

Naive question: is OpenMath only designed to communicate between Computer
Algebra systems, or is the aim to also include theorem provers and other
systems that speak 'math' (like PVS, Coq, model-checking software, etc)?
OpenMath looks very well suited for Maple-Mathematica-MuPad communication,
but say Maple-Coq communication would appear to be 'out of scope'?  If CA
communication is the complete scope, then just ignore the above comments as
they are superfluous.

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