[om-a] Draft version of OpenMath 1.1 available

[Andreas Strotmann]

Hi,

can someone explain to me the reasoning behind the following:

<quote>
Repeated occurrences of the same variable in a binding operator are
allowed. An OpenMath application should treat a binding with multiple
occurrences of the same variable as equivalent to the binding in which all
but the last occurrence of each variable is replaced by a new variable
which does not occur free in the body of the binding.
binding (lambda, v , v ,application (times,v ,v) )  is semantically
equivalent to:
binding (lambda , v' , v ,application (times,v ,v) )  so that the
resulting function is actually a constant in its first argument (v'  does
not occur free in the body application (times,v ,v) )).
</quote>

In particular, why not just make repeated variables ``erroneous'' in the
CLtL sense (undefined, but not an error) instead of this arbitrary rule?

Without the currying rule for OMBIND, its original rationale is gone, and
what's more, it contradicts the variable-renaming rule in the preceding
paragraph of the draft (which incidentally needs to be generalized to the
n-variables case, I just realized).

I'm sure this was discussed in Pisa- what was the tenor of the discussion?

Thanks,

 -- Andreas

--
om-announce at openmath.org  -  public announcements concerning OpenMath
Post discussion to om at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-announce-owner at openmath.org for assistance with any problems