improvements on OM standard from Tallahassee workshop

Mon Nov 16 17:58:20 CET 1998

<html>
<head>
<title>Tallahassee on OM standard</title>
<BODY TEXT="#000000" BGCOLOR="#FEFAE6" LINK="#0000EE" VLINK="#551A8B" ALINK="#FF0000">
<h1>Tallahassee on OM standard</h1>
<center>
<table width="70%">
<tr><td>
In November 13-14, 1998, at the 11-th OpenMath workshop in
Tallahassee, the OpenMath Standard version 1.5 was accepted with the
understanding that the editors (Caprotti &amp; Cohen) provide a new
version taking into account the points mentioned below and that the
chapter on CDs (4) be further developed, especially with respect to
hierarchy mechanisms.
</td></tr>
</table>
</center>

<h2>Remarks from the workshop</h2>
Minor corrections, such as typos and language improvements, are not listed here.

<h3>Chapters 1 &amp; 2</h3>

<center>
<table width="82%">
<tr><td>
<ol>
<li>Re-install the non-normative Chapter 0 
with an account of the standard's growth, references to relevant
prior papers/documents, acknowledgments, background and motivation.
<li>Add a reference to MathML in the references.
<li>Make clear in section 1.3 or elsewhere,
that OM objects are supposed to be interpreted as being equal
if a bound variable is replaced by another bound variable:
\int sin(x) dx = \int sin(y) dy,
but that the OM language/standard does not come with a method to 
identify the left and right hand side. This kind of equality is called \alpha equality.
Note:
<ul>
<li>perhaps a phrasebook + application should be written specifically for this purpose, 
that is, for \alpha identification, that is, 
checking whether two expressions are equal up to such substititutions;
<li> the alpha equality problem is not completely trivial: in 
\int y sin(x) dx , we cannot just replace x by y.
</ul>
<li>Variables in bindings may be equal. The intepretation is as in composition.
Thus, 
binding(Lambda, x, x, x*x)
CAN be interpreted as
binding(Lambda, x, binding(Lambda, x, x*x)),
so that the first argument x does not really recur in 
binding(Lambda, x, x*x); in other words, the outer binding is a constant function.
Or, with the above semantic interpretation, 
binding(Lambda, x, x, x*x) is \alpha equivalent to
binding(Lambda, y, x, x*x) and to
binding(Lambda, x, y, y*y).

<li>Flattening of attribution is the replacement of a composition of attributions
by a single attribution. It is understood that the flattened attribution
 (which will be defined more explicitly
in the report), is semantically identical to the unflattened one.
<li>The first argument (rather than the last) of attribution will be the actual attributed object.
<li>The order of pairs Si Ai 
in atttribution matters. 
<li>Si = Sj need NOT imply i = j.
<li>In case of
Si = Sj for i &lt; j,
the value
Aj has priority over Ai for the coinciding
attribute.
<li>Attribution can function as either &quot;annotation&quot;
 (adornment, dress up) or as &quot;property&quot;. In the former case, 
replacement of the adorned object by the object itself is probably not harmful,
but in the latter, it may very well be. Therefore, attribution in general should be treated
as a construct rather than an adornment. It may be viewed as semantically equivalent to the
stripped object only if it is clear from the CDs in which the symbols
Si are defined, that the attribution in question is
meant for adornment. This should be clarified.
<li>Make it clear everywhere that symbols depend on CDs.
<li>Interchange order for paragraphs on Error and on Attribution.
</ol>
</td></tr>
</table>
</center>

<p>
<p>
<h3>Chapter 3</h3>

<center>
<table width="82%">
<tr><td>
<ol>
<li>
The fact that the syntax of the XML encoding of OM is more restrictive than the XML syntax
(line -2, page 12) has serious bad consequences. Hence it should be reconsidered.
An example of what can go wrong: suppose one uses the binary encoding (to be) supplied
for XML, or any other XML software package. what comes out after decoding (to follow the example),
is XML code but not necessarily withing the image of the XML encoding of OM.
<li>The table on page 14 has various typos. E.g.,
<ul>
<li>+ in symbname should be *
<li>attrvar has dropped out
<li>varname has = occurring twice
<li>same for base64
</ul>
<li>Other remarks on Figure 3.1
<ul>
<li>Add underscore before last ] in cdname
<li>prevent fpdec from being empty
<li>replace e(-?) by e({-|+}?)
<li>(amc)are the outer brackets in varname really necessary?
<li>Replace the third S? in symbol by S
<li>for object:
in integer, and maybe utf7 and base64,
allow for S adjacent to and inside the container symbols.
<li>
for object: adjust OMATTR with new order of arguments, that is,
bring S? object S? forward.
</ul>
<li>explain the XML idiom such as PCDATA.
<li>On page 16, adjust floating-point number description wrt new requirements.
<li>On page 17, refer for Lambda symbol to quantifier CD rather than ecc.
<li>Explain that the standard binary encoding of XML encoding would be less efficient
(in decoding) than the supplied direct binary encoding of OM.
<li>Consider use of XML tools for XML encoding of OM!
<li>Page 20, line 8, replace exponent 32 by 31.
<li>Page 21: interchange order for paragraphs on Error and on Attribution.
<li>Page 21: Rewrite the sharing paragraph.
<li>Give one or two small examples for the binary encoding.
<li>Consider doubling of the length: length 64 instead of 32.
(Argument: this would capture the full decimal development presently stored of
\pi.)
There is ASN technology for arbitrary long strings; consider and discuss it.

</ol>
</td></tr>
</table>
</center>

<h3>Chapter 4</h3>
The present work is accepted, but there is a strong need for
further development soon!

<br><p>
<p>
<h2>Actions</h2>

<ul>
<li>Angel Diaz will send Sigsam overview paper to amc
<li>St&eacute;fane Dalmas
for binary encoding.
<li>Stephen Buswell for XML encoding.
<li>James Davenport for CD work.
<li>Andreas Strotmann send details not yet mentioned to Arjeh.
</ul>
<address>
<a href="mailto:amc at win.tue.nl">Arjeh Cohen</a>
</address>
</html>