[om] DefMP elements

[Paul Libbrecht]

On Jeudi, déce 4, 2003, at 01:56 Europe/Paris, Bill Naylor 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.
>
> I think this is a very good point, it would be very dangerous to
> exclude mathematical community's at the specification level!

To me, OMDoc was made to answer to this point and OpenMath doesn't have 
enough artillery for that:
-> if you want a definition, then you probably want theorems to justify 
this definition (and thus proofs)
-> if you want multiple definitions then you probably want theorems to 
prove the equivalence of these

Declaring DEFMP to disallow self-referencing is for the sake of keeping 
such a notion of definition small and simple: I understand it as a 
syntactical replacement instruction...

Allowing recursion means you need to to prove (or trust?) that 
recursion has an end... at least not something you can do with a schema.

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