[om] Bindings / Sparse Linear Algebra and Distributions / Optimization

[David Carlisle]

> but I am still not sure I understand the binding concept in Openmath.

I'm not sure if you mean you are not sure about the notion of binding in
general, or about the specifics of the OMBIND syntax, apologies
if this starts at the wrong level. (Also it's a somewhat trucated
description but I hope it points you in the right direction)

For our purposes one of the main properties of bound variables, as
opposed to unbound `free' variables, is that variables may be renamed
without changing the meaning of the expression, 

In normal mathematical discourse sometimes you write f(x) to mean
`the function f' with the (x) just being a mnemonic for function
application, so you may talk about the function sin(x), sometimes (and
more correctly) you mean by f(x) the value of the function applied to
x.  To refer to the function specifically you might write
x |-> f(x)  (sometimes read x maps to f(x))
in this case you could also just say `f'
but the binding operation (normally known as lambda abstraction)
allows `anonymous' functions that are not assigned a name
so x |-> x^2+1  also written lambda x . x^2 + 1
is the function that squares and adds one.

Note that x |-> x^2+1 and y |-> y^2+1 are the same function.

Other binding operators, besides lambda, are 

logical quantifiers:

forall x . P(x)

or definite integration

int_0 ^ 1 sin (x) dx

If one knew the semantics of all the symbols (as expressed in content
dictionaries) one wouldn't strictly need an OMBIND syntax and everything
could be expressed in functional notation with OMA. 

However for many purposes it is useful to know immediately which are the
bound variables (for example an OpenMath aware search engine would
always want to consider a search successful if the requested expression
was found subject to renaming bound variables (known as alpha
conversion).

So OMBIND takes 

a symbol that is the constructor, which typically is
something like `lambda' or `forall' or `defint'.

Then it takes a list of bound variables often you want to bind more
than one variable at a time: exists x,y,z such that x^2 + y^2 = z^2 

and finally it takes the expression in which the variables are bound.

Incidentally with regard to the example for `forall' that I referred you
to in the Content Dictionaries, someone (correctly) pointed out that the
example could be improved. As it currently appears it is the correct
OpenMath expression for

forall x .  sin(x) < 1

but since this is false unless there is some implied context that x is a
real number, the example probably should say

forall x .  x in R => sin(x) < 1

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