[om] OMBIND misunderstanding

[David Carlisle]

Ramon


> In the OpenMath 2.0 Standard Document, talking about Bindings (Section  
> 2.2), you can read:
> 
> "It is allowed to have no bound variables, but the binder object and the  
> body should be present."
> 
> However, in the Schema the OMBVAR, which is the object including the  
> variables, requires to have ONE OR MORE objects omvar.

As far as I can see this situation (which is clearly a bug) has survived
intact in OpenMath 1.0, 1.1 and 2.0. thank you for drawing attention to
it.

I believe that the intended definition of the binding operator was that
expressed by the text of the standard, and that the schema are
wrong. The Relax NG should have

# variables used in binding constructor
OMBVAR = element OMBVAR { common.attributes, omvar* }
                                                  ^
                                                  ^

with a * here not a +, and appropriate changes to the derived RNG, XSD
and DTD files, (and also to the OpenMath 1 DTD).

In some logical frameworks a function with no arguments is (by
definition) equivalent to its body, in which case allowing zero variable
binders would be harmless but redundant, however in other frameworks
such functions do have meaning (usually modelling some kind of side
effect) and as far as I recall when OMBIND was added to OpenMath (a long
time ago:-) it was explicitly intended to be able to model such functions
with an OMBIND with no variables.

This is a personal reply, but if the other OpenMath Standard editors
agree with this analysis, we will presumably update the public schema
with these corrections (otherwise we will need to issue an update to the
standard to change the text to match the schema).

David

________________________________________________________________________
This e-mail has been scanned for all viruses by Star. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk
________________________________________________________________________
--
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