[om] DefMP elements

[Professor James Davenport]

On Thu, 4 Dec 2003, Paul Libbrecht wrote:
> 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
> 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...
Exactly so. 
> 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.
Maybe I should have called them 'recursive' rather than 'evaluating'.
James
--
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