[om] OMBIND misunderstanding

Andreas Strotmann Strotmann at rrz.uni-koeln.de
Tue Jan 4 14:37:51 CET 2005


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

As far as I remember, this was indeed the intention as discussed at 
various OpenMath meetings.  Random() was the prototypical example used, 
I believe, which we figured might need to be definable as something like

   random := bind(lambda,some_randomizer_formula)

in which case the binder lambda would need to be accompanied by zero 
bound variables.

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

More information about the Om mailing list