[From: http://www.openmath.org/activities/standrews.html.]
James Davenport
10 August 2000
The core of OpenMath is the standard and its CDs. He felt that the standard was largely stable and should be formally accepted by the OpenMath Society meeting. The `core' CDs were being reviewed by Stan Devitt and AS. They had been delayed due to the perpetually-imminent arrival of MathML2. SMW would speak to this later. there were also various other CDs awaiting the acceptance of the `core' CDs.
Phrasebooks were the tools and concrete implementations of CDs. MR would speak to these later. It was important that these exist, to make the task of software developers easier. There are three supporting families of libraries, by MR in Java, by Stephen Braham (which had fallen somewhat behind the standard), also in Java, and from Nice (C and Java).
It was queried whether there should be the times from
arith2 (the commutative one) as well as the one from
arith1. AS pointed out that there were almost no instances in
the core of uses of the arith2 times. JHD countered that it
was impossible to state, say, the Binomial Theorem without the use of
this times. It was agreed to leave things as they were.
AMC closed this session with an appeal for all participants who had not registered to do so, and for those who were eligible to join the OpenMath Society and wished to do so to indicate this to him.
bigfloat1 CD.
meta group needs reworking to match the changes to the
standard.
It was pointed out that there was no procedure for CD amendment. MCD thought that minor changes (as defined in the standard, and involving a change of minor version number) were the purview of the Executive, and major ones (adding symbols) should go through the review process. SMW pointed out that the URL did not identify the CD uniquely. He volunteered to draft the necessary amendment to the standard.
AMC pointed out the necessity to publish CDs, and that we had been waiting for months for MathML version 2. RMT asked how often ``bugs'' were found in CDs. MCD said that AS's fresh pair of eyes had pointed out several incompatibilities, not least with the CD-writing document by JHD.
RMT pointed out that this document should say how difficult it is to write a CD. AS agreed and said that ``Abramowitz and Stegun'' paper showed how difficult it was. AMC urged that there should be a special functions CD, since there was work going on in several places. JHD said that he had spoken to both Nice and UWO on this, but it was waiting for the core CDs. SMW suggested that Patrick Ion (Mathematical Reviews) would, at least, make an excellent reviewer, for technical as well as political reasons.
MK asked about the procedure for externally-written CDs. He said that
there were potentially thousands of theorem-proving and logic CDs. JHD
noted that there were several CD groups he had waiting in the wings, e.g.
polynomial CDs. SMW asked that contact should also be made with Cathode --
AMC volunteered to do this. AMC asked for volunteers to review the
polynomial CDs: it was suggested that these be found in the Macaulay and
Singular groups. It was agreed that the Executive Committee should
nominate a ``CD Editor''.EC
AS reported that MS had been to an ACM-meeting on ``Mathematics on the Web''. He therefore suggested a CD for ``Mathematical Classifications''.
MK said that people contributing a CD would probably want write access to it. He favoured a CVS server for OpenMath, which was the tool in use by, for example, Mozilla. SAL added that GAP used CVS universally. MCD noted that CVS could only be used for development -- official CDs should be archived outside CVS.
There was a problem with consistency between the NAG site and the Tallahassee site, in particular URL's were not consistent. The NAG site should only use relative path names. MCD and BM would investigate.
He recapitulated the early history of OpenMath, starting with experience of
interfacing Maple and other software and 1992. In 1994, Dave Raggert
proposed the <math> tag for HTML 3.0, but this was not accepted. The
HTML Math group was formed by W3C in 1995, and received a proposal
from Wolfram Research, for a language that looked similar to Mathematica.
This did not look like HTML. INRIA/IBM/Maple/Stilo proposed an
``HTML-native'' mathematics, which became MathML. The distinction, in terms
of semantic extensibility, between MathML and OpenMath, became clear. It
should be noticed that presentation allowed extensibility. XML was approved
on February 10, 1998, and MathML on April 7, 1998. As of MathML 1.0,
OpenMath used MathML for rendering, and OpenMath was one of the
ways2 of extending MathML's
semantics. MathML 2 is held up, partially because of the question of
handling flowing equations from right to left in ``arabic'' mode, and
similar non-mathematical issues. Several browsers, natively or via applets
and plugins, support at least presentation MathML. MathML 2 has some
internal changes, but also changes to support XML changes, XSL etc.
There are two mechanisms in MathML 2 to extend MathML by external references.
XSLT provides a rewriting system for XML expressions. This allows one to:
<mx:rank/> to
<semantics>
<ci>rank</ci>
<annotation-xml encoding="OpenMath">
<OMS name="rank" cd="linalg1"/>
</annotation-xml>
</semantics>
[JHD asked why this was a <ci>? The answer was that all content has a
default rendering, which in this case would be <mi>rank</mi>.]
He claimed that this way we could ``hide'' OpenMath semantics in MathML
documents via macro packages, probably domain-specific.
In questions, MK asked whether SMW proposed that OpenMath should include
xlink. SMW thought that it would be a good idea. SAL asked whether
the links could be from content to presentation, rather than the other way
round. SMW said that it was possible, but not as robust. He also explained
that the rules for ``what was clickable'' were vague and non-normative. He
was asked about SVG. It would be nice to be able to place mathematics in
SVG geometric diagrams. BM asked ``what worked now''? SMW pointed to WebEQ
as an applet and Techexplorer as a plug-in. There are still issues about
real-estate control and base-line control in browsers. It was important that the
OpenMath community used MathML with OpenMath content, since no-one else
would. AS asked about the use of non-arabic digits. It would be possible to
use <semantics> for this. OC said that Mozilla rendered theorems
etc. in special ways -- how does this relate to MathML? SMW said that this
was an issue for stylesheets.
As a general remark, he commented that, whereas S-expressions had failed to catch on, XML, a tree-structured data format, seemed to be ``popular''.
The Ctadel system is written in Prolog, which has a C SGML/XML library. AS
has written OpenMath reading and writing routines on top of this library,
to produce Prolog terms like OMA(arguments). Prolog does not
understand binding, but Ctadel does (though the only binder is
lambda, so OpenMath's exists becomes SOME(lambda ...,
which MK commented was a standard trick known as ``higher-order syntax''.),
which adds a complication. CDgroups and CDs are read dynamically, and also
augment the Ctadel help system. He emphasised that this was an important
use of CDs, and stressed the need for them to be comprehensive. One
difficulty was the difference between times in arith1 and
arith2. He had to write several DTD grammars: CDs and OMOBJs.
He needs OpenMath to/from MathML stylesheets4 urgently, so that the academics can publish their mathematical models in active documents. He needs tools to convert binary XML converters to be OpenMath-compliant. In the area of physics, he needs:
OC suggested that AS should look at existing work, e.g. DTDs for chemistry, rather than try to make OpenMath encompass everything. He will need to interface with Geographical Information Systems, which probably means ``Dublin Core'' metadata.
Decoding is more difficult, since in most (excluding Axiom!) systems the result is an untyped string. It is therefore necessary to write a general parser which depends on various ``natural'' assumptions. Unknown objects are translated into symbols in a system-specific CD.
He outlined various advantages of making the phrasebook be part of the
client. They have phrasebooks and servers for Gap, Coq, Mathematica, CoCoa
and R. The code is available at http://crystal.win.tue.nl/public.
SD commented that, in the case of Mathematica, it would make more sense to use Mathlink rather than the Mathematica user language. WAN asked whether the error CD had been implemented. It had not yet been done, but needed to be.
OMDoc, rather than just individual formulae -- OMOBJ.
OMDoc consists of the following elements.
omtext etc.;
premises, as well as method.
OMDoc theory is equivalent to
an OpenMath CD. This should be parameterised, as in lists. He commended the
work of the algebraic specification community to OpenMath. OMDoc
achieves this via theory and import (with renaming).
OMDoc can be used for the following.
OMDoc is spoken by mega, Clam, InKa, Tramp, MBase,
can be converted to LATEX, HTML and MathML, and converted from CASL and
various others. As an example, he presented an abstract data type for the
natural numbers. This was converted into a CD via an XSL program.
They are working on IDA, which is 12Mb of HTML. They can deliver it in
various formats, depending on the declared knowledge level of the reader.
The status of OMDoc can be seen at http://www.mathweb.org.
The project definitely needs authoring tools.
Sub-languages include FOL, while there are extensions such as HOCASL. There seems to be a close correspondence in the small between the elements of CDs and CASL specifications. OpenMath seems to have semantics with respect to text-books, whereas CASL has a self-contained6 formal semantics. CASL libraries (similar to OpenMath CDgroups) have URLs. There is inheritance with renaming.
TM showed some CASL examples, such as Monoids and Natural Numbers. In CASL,
one has to distinguish between the * of Monoid and the * of
CommutativeMonoid. Axioms can be labelled. The view command allows
one to view the natural numbers as a commutative monoid (in two different
ways), which induces a reduction from the class of models of the natural
numbers to the class of models of CommutativeMonoids, and a double lifting
from the theorems of CommutativeMonoids to those of natural numbers. He
showed an algebra structure diagram (remarkably similar to the cover of the
Axiom book). Fields are defined as commutative rings with Group lifted to
the non-zero elements. The specification of vector spaces is parameterised
by a Field. It is possible to have hidden sorts. There is a free
construct, e.g. for building free vector spaces. The real numbers can only
be specified in HOCASL, because of the completeness axiom.
The CASL toolset has a syntax tree, currently in Aterms but probably
to be replaced by XML, with a parser and a static checker, which resolves
overloading (with the coherence rule for subsorts). This tree can be
encoded in FOL/HOL and therefore passed to Isabelle or HOL. Aterm
can be formatted in LATEX (the tool also generates the algebra structure
diagrams). The web site is at http://www.bricks.dk/Projects/CoFI.
There is a rationale in Proc. TAPSOFT '97, LNCS 1214.
AMC wondered about the interfacing with computer algebra, given the whole theory of algebra. TM thought that it was too premature. He quoted Harrison's work on real analysis. He also quoted the use of theorem-proving after the ``pentium bug''. There isn't a separate database, but the CASL libraries can be seen as a database. AS reminded the meeting that, on the advice of the Axiom group, OpenMath was not trying to replicate the Axiom type system. TM commented that CoFI was worried about the size of its theories. There was a boot-strapping problem, since one wants integers in groups (for exponentiation), but one wants to view the integers as a group.
OC asked all speakers to provide her with electronic copies of their talks. She also asked people to contribute any tools they had, via a form available from the workshop page.
AMC announced the Esprit project's open workshop in Heidelberg on 6 October 2000.
This document was generated using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
The command line arguments were:
latex2html -split 0 -show_section_numbers -local_icons -no_navigation -no_footnode -numbered_footnotes -html_version 3.2,math standrews.tex.
The translation was initiated by Mike Dewar on 2000-08-30