[om] DefMP elements

[Taneli Huuskonen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

"Jacques Carette" <carette at mcmaster.ca> wrote:

[quoting Mike Dewar:]
> > 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.  

Thanks for the clarification, Mike.

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

If I understood James' paper correctly, the point in disallowing
recursion in a defining FMP was that an application could then attempt
to replace unknown symbols with their definitions, possibly recursively.
A recursive definition wouldn't allow one to get rid of the symbol in a
straightforward way.

I can see off hand a couple of ways to allow recursive definitions
nevertheless:

1)  Use explicit fixpoint operators in the definitions.  This should be
    a matter of writing and using an appropriate CD.

2)  Allow syntactically recursive definitions and make it the
    application's responsibility either to translate them to something
    that it understands internally or to fail gracefully.  In any case,
    an application has to be able to deal with unknown symbols,
    undefined expressions and so forth.

3)  Introduce a third type of FMP: an alternative definition.  There
    could be any number of them, and the only requirement would be that
    they have to uniquely define the same object as the main definition.
    Advanced applications, such as theorem provers, might want to use
    some of them, simpler ones could ignore them.

Regards,
Taneli Huuskonen

-----BEGIN PGP SIGNATURE-----
Version: PGPfreeware 5.0i for non-commercial use
Charset: noconv

iQA/AwUBP84nsl+t0CYLfLaVEQJu+wCfax0hQFjtwRw38Yrg5rBgBYguNMcAn3lA
n3+XNhg2sDyMAKF0I9N9EB2+
=VdC9
-----END PGP SIGNATURE-----
-- 
All messages will be PGP signed,  | Hélas, jamais je ne deviendrai
encrypted mail preferred.  Keys:  | rhinocéros, jamais, jamais!  Je ne
http://www.helsinki.fi/~huuskone/ | peux plus changer.  -- Ionesco
--
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