[From: http://www.openmath.org/activities/standrews.html.]

University of Saint Andrews

**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.

- 1.
- AMC opened the meeting. He reminded the meeting that there had been,
as required by the Statutes
^{1}, an Annual Meeting in Tallahassee, attended by MS and AS. That meeting had adjourned all its substantive business to this meeting. The auditors had reported to that meeting, and the officers were continued until this meeting, save that AS was now an Auditor, and TH a Deputy Auditor. - 2.
- The meeting elected JHD as its Secretary. CT and BM were elected to check the minutes. AMC was elected as president of the Meeting.
- 3.
- The Meeting confirmed that it was a duly constituted meeting, authorised to conduct the remaining business of the AGM.
- 4.
- The substantive agenda was approved.
- 5.
- MS had pointed out by e-mail that the statutory number of Members-at-Large of the Executive Committee was one more than had been previously thought. MCD nominated, and SMW seconded, AMC for President. This was approved unanimously, as was the re-election of all existing Committee members (nominated by RMT and seconded by JHD). SMW said that, in view of the work done at INRIA, he nominated MG for the vacancy. This was approved unanimously.
- 6.
- OpenMath standard. This had been approved previously, subject to a
question (BM) about the containers for floating-point numbers. This had now
been resolved by the
`bigfloat1`

CD. - 7.
- CD acceptance. MCD explained the procedure, and said that the
Committee had nominated AS and Stan Devitt to review the first batch. These
people would also, drawing on their experience, suggest improvements to the
process. AMC asked how long this review process would take. AS said that
there were some fundamental questions.
- What level of generality was aimed for.
- What level of compatibility with MathML was being aimed for.
- The
`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''.

- 8.
- AMC raised the question of the Web Site. The substantive site is
currently maintained at NAG, though
`openmath.org`is actually in Florida. There had been problems with the mirroring, but a work-around had been found. There is a ``What's new'' page, which can be registered with a Netminder.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.

- 9.
- The meeting elected Michael Kohlhase as a new member. AMC reported that the society now had a bank account in London (Ontario). Gonnet was willing to contribute to the finances. AMC reported that the Executive felt that CD production was the priority, and that they wished to reward the production of good CDs via a small prize. The Executive would be drafting rules.
- 10.
- Date of Next Meeting. This would be on the Saturday before ISSAC 2001, in July in London Ontario.
- 11.
- MK asked about formal standardisation. MCD reported that W3C would be the obvious route, but MathML was essentially occupying this territory. The Esprit project had investigated STEPS, but this seemed quite heavy. He asked for suggestions, especially from BM.

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
ways^{2} 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.

`csymbol`- This contains rendering information (in MathML
presentation) and a URL for semantics, as well as an attribute saying what
the semantics are encoded in. He emphasised that
`csymbol`was a content tag. `semantics`- This is a fancier version of the above. The first
child contains the object being described. Subsequent children can be
`annotation`or`annotation-XML`. The latter can be used for MathML-content or OpenMath, whereas the former is text (PCDATA) which could be in computer algebra languages, or rendering information such as TEX. Again, this is a content object.

XSLT provides a rewriting system for XML expressions. This allows one to:

- define notation for new areas;
- localise notation, for journals or for national differences;
- insert OpenMath semantic information for new domains.

`<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 stylesheets^{4} urgently, so that the academics can publish their
mathematical models in active documents. He needs tools to convert
binary
$\leftrightarrow $XML converters to be OpenMath-compliant. In the area
of physics, he needs:

- units;
- orders of magnitude (to decide which terms to ignore);
- the names of physical laws (since the laws themselves depend on the frame of reference);
- some means of handling commands (already mentioned by MK last year);
- terms from many areas of physics.

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.

**Syntax**- the problem addressed by OpenMath's XML encoding.
**Protocol/Control**- OpenMath does not make any contribution here. He now believes that KQML is the answer here.
**Semantics**- The dictionaries are machine-readable, but not really
machine-understandable, since most descriptions are informal.
Semantics were important, e.g. is
$0\in $
**N**. **Context**- The OpenMath community has discussed ``dynamic CDs'', but no real resolution has been achieved.

`OMDoc`

, rather than just individual formulae -- `OMOBJ`

.
`OMDoc`

consists of the following elements.
- Meta data, in Dublin Core representation.
- Text elements --
`omtext`

etc.; - Definitions, which include CMPs and FMPs.
- Proofs. This could include
`premise`

s, 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`

(
`OMDoc`

can be used for the following.

- 1.
- A communication standard between mechanised reasoning systems,
- 2.
- An input and documentation preparation language for MBase.
- 3.
- A tool supporting the controlled refinement from informal presentation to formal specification of mathematical objects and theories.
- 4.
- A basis for individualised interactive books.

`OMDoc`

is spoken by $\Omega $mega, $\lambda $Clam, InKa, Tramp, MBase,
can be converted to L
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.

- to provide a common framework for algebraic specification;
- it should be attractive to researchers and, ultimately, to industry;
- to supersede previous efforts via better tool support;
- to be free.

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-contained^{6} 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 L^{A}TEX (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.

University of Saint Andrews

This document was generated using the
**LaTeX**2`HTML` 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

- ... Statutes
^{1} - BM asked whether this could be changed, but some members recalled that this was a requirement of Finnish law.
- ...
ways
^{2} - The lack of CDs was one reason why it was not possible to
make OpenMath
*the*extension mechanism. - ... routines
^{3} - The loop unrolling for vector processing also needs to know how `expensive' these are, which is not currently possible in OpenMath.
- ... stylesheets
^{4} - WAN pointed out that DC had these.
- ... (TM)
^{5} `http://www.tzi.de/till`.- ... self-contained
^{6} - Modulo predicate logic and Zermelo-Frankel.