[Om3] On 'restricting bound variables' in Basic OpenMath

[Professor James Davenport]

On Sun, November 2, 2008 9:45 pm, Chris Rowley wrote:
> 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'.
That is indeed the distinction between OMBIND/OMBVAR and OMA.
> 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.
I am in  very similar situation.

James Davenport
Hebron & Medlock Professor of Information Technology
Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept
Lecturer on CM30070, 30078, 50209, 50123, 50199
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor
IMU Committee on Electronic Information and Communication