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

Michael Kohlhase m.kohlhase at jacobs-university.de
Mon Nov 3 16:11:29 CET 2008

Dear Chris,

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 correct (even though I know this as alpha-renaming). And this is
the best we can hope for, since we have arbitrary binding symbols.
> Michael's idea of adding 'condition' at a basic level relates more
> closely to typing rather than to this pure concept of binding.
>
This is incorrect, <condition> is independent of the notion of typing
(though you might be tempted to fake typing with condition). The main
idea here is that the condition element allows to put a restriction on
all the bound variables _together_. While both mechanisms restrict the
set of instances the bound variables range over, types are restrictions
for _single_ bound variables, and thus attributions (semantics in
MathML) are the appropriate mechanism. BUT in cases where you want to
co-restrict more than one variable, you need a different mechanism,
which is why formal languages (mostly logics) that need such things have
developed the <condition> mechanism (these formalisms often speak of
"guards" for the conditions). Consider for instance the restricted
quantification

$\forall x,y[x-y\ne 0] 1/(x-y)\ne 0$

where I have marked the condition in square brackets. This is not
something you can straightforwardly do with a type. Incidentally, this
is not something that we can straightforwardly express in OpenMath,
since the OMBVAR element is one of the very few we do not allow
> 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 think that you did, actually. So what is the proposed addition:

For OpenMath Objects, I propose to change

binding (B, v1, …, vn, C)

to
binding(B, v1,...,vn[:C,], D)
where C is an optional condition element (I have renamed the old C to D
in the process).

For the XML encoding I would allow an additional OMC child to the OMBVAR
element, so that the example above would look like this

<OMBIND>
<OMBVAR>
<OMV name="x"/>
<OMV name="y"/>
<OMC>
<OMA><OMS cd="arith1" name="ne/>
<OMV name="x"/>
<OMV name="y"/>
</OMA>
<OMC>
</OMBVAR>
<OMA><OMS cd="arith1" name="ne/>
<OMA><OMS cd="artih1" name="divide"><OMV name="x"/><OMV name="y"/></OMA>
</OMA>

Michael
> _______________________________________________
> Om3 mailing list
> Om3 at openmath.org
> http://openmath.org/mailman/listinfo/om3
>

--
----------------------------------------------------------------------
Prof. Dr. Michael Kohlhase,       Office: Research 1, Room 62
Professor of Computer Science     Campus Ring 12,
School of Engineering & Science   D-28759 Bremen, Germany
Jacobs University Bremen*         tel/fax: +49 421 200-3140/-493140
m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
skype: m.kohlhase   * International University Bremen until Feb. 2007
----------------------------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: m_kohlhase.vcf
Type: text/x-vcard
Size: 320 bytes
Desc: not available
Url : http://openmath.org/pipermail/om3/attachments/20081103/d8fde957/attachment.vcf