[om] Re: [om-a] Draft version of OpenMath 1.1 available

[Michael Kohlhase]

[redirected the discussion to om at openmath.org instead of om-announce]


> <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 think that there is no reason to allow repeated variables in one n-ary
binding, now that currying has gone away. It is important to still allow 

(lambda, v, (application, (lambda, v, v), v)), 

which is used in many type theories. 

The only reason to keep it might be that making repeated variables illegal
is another validity constraint that cannot be enforced in the OpenMath DTD
(It can be enforced by a Schema though), which can be dealt with on the
semantics level. 

All in all, I think that we should follow your suggestion and make repeated
variables in the binder of a single binding object illegal. Could you come
up with specific wording for the standard?


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

No, as far as I can remember, this has been missed. 

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