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
[email protected]
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
[EMAIL PROTECTED] http://kwarc.info/kohlhase
skype: m.kohlhase * International University Bremen until Feb. 2007
----------------------------------------------------------------------
begin:vcard
fn:Michael Kohlhase
n:Kohlhase;Michael
org:Jacobs University;Computer Science
adr:;;Campus Ring 1;Bremen;;28759;Germany
email;internet:[EMAIL PROTECTED]
title:Prof. Dr.
tel;work:+49 421 200 3140
tel;fax:+49 421 200 3140
x-mozilla-html:TRUE
url:http://kwarc.info/kohlhase
version:2.1
end:vcard
_______________________________________________
Om3 mailing list
[email protected]
http://openmath.org/mailman/listinfo/om3
