[om] DefMP elements

[Professor James Davenport]

On Wed, 3 Dec 2003, Jacques Carette wrote:

> > 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.
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.
For `evaluating` FMPs this means that enough such substitutions (e.g. 11 
for 10!) will eliminate the symbol for concrete instances, and that, for 
non-concrete instances, if you )the application) know enough about the 
relevant type to build a fixed-point operator, then you can regard these 
as defining. The aim is to allow 'simple' phrasebooks to write out symbols 
their applications don't understand without having to do a detailed parse 
of a defining FMP: if there is one, I can use it.
> 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!
This one I don't follow.
> 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.
The seocnd aim/
--
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