At present in OpenMath, binding seems to me to be doing nothing more than defining exactly which (and when) so-called '\alpha-substitutions' 'preserve the semantics of an OpenMath object'.
Michael's idea of adding 'condition' at a basic level relates more closely to typing rather than to this pure concept of binding. Adding Michael's idea to binding seems therefore to be inappropriate. But I am not sure that I have seen a precise definition of what his suggested addition would be, so I may have misunderstood. More generally, there is a more major problem with adding anything like conditions to Basic OpenMath: that this would require the introduction of a Basic OpenMath Object of type 'set membership' or, equivalently (I think:-), 'Boolean', which could be called 'bit'. Thus, if anything needs to be added to basic OpenMath then I would suggest that some Basic Object to represent the primal concept of duality is a prime candidate. This fits with my thoughts on looking at the sets CD too: something there should be introduced at a more fundamental level. One could argue that a Basic Object such as 'integers' imply that 'a total order relation' and hence 'membership in a set of size 2' is also a Basic Object but there is no harm in making this more fundamental idea explicit. Also, it is not entirely clear whether the phrase 'integers in the mathematical sense' implies that the standard order relation is also Basic. _______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
