[om] OMBIND misunderstanding
Andreas Strotmann
Strotmann at rrz.uni-koeln.de
Tue Jan 4 14:37:51 CET 2005
David,
> 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