[om] DefMP elements
Professor James Davenport
jhd at cs.bath.ac.uk
Thu Dec 4 17:45:37 CET 2003
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...
> 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'.
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
More information about the Om