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

[Michael Kohlhase]

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