OpenMath is an extensible standard for representing the semantics of mathematical objects.
OpenMath is an extensible standard for representing the semantics of mathematical objects.
AMC opened the meeting. He reminded the meeting that, for the last three years there had been a funded ESPRIT project on OpenMath. This had led to the development of many individual tools, which were on the verge of “breaking out” and being useful to many. He apologised for any short-comings on the part of the organisers (himself and OC) and thanked MK for his help.
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).
JHD spoke to the issue of Content Dictionaries. There were several points raised for discussion. JHD in particular asked about multiple signatures (see the STS paper). This caused a lively debate with no immediate resolution.
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.
Present: Bernardin (LB), Caprotti (OC), Chicha (YC), Cohen (AMC), Dalmas (SD), Davenport (JHD), Dewar (MCD), Dirat (LD), Dupée (BJD), Gaëtano (MG), Hur (NH), Jebelean (TJ), Kohlhase (MK), Linton (SAL), Miller (BM), Mossakowski (TM), Naylor (WAN), Riem (MR), Strotmann (AS), Timoney (RMT), Traverso (CT), Watt (SMW).
AMC opened the meeting. He reminded the meeting that there had been, as required by the Statutes1, 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.
The meeting elected JHD as its Secretary. CT and BM were elected to check the minutes. AMC was elected as president of the Meeting.
The Meeting confirmed that it was a duly constituted meeting, authorised to conduct the remaining business of the AGM.
The substantive agenda was approved.
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.
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.
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:
meta group needs reworking to match the changes to the standard.JHD felt that, if these issues could be resolved at this meeting, it was a matter of weeks. AS felt that this was achievable.
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”.
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.
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.
Date of Next Meeting. This would be on the Saturday before ISSAC 2001, in July in London Ontario.
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.
SMW spoke to this issue. While we had been discussing content earlier, this was in fact a small part of MathML. In particular he spoke about the distinction between ‘content’ and ‘presentation’ in MathML. He worried that the MathML “out there” would only be presentation unless content was made easier.
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:
There are rules for mixed markup, e.g. mostly content with some
presentation (see csymbol), and for parallel markup, which can
be either at the top-level or fine-grained. To allow fine-grained
parallel markup without having O(n2) blow-up, MathML 2
allows the id and xref attributes. Using xlink:id and
xlink:href allows us to link into Openmath content rather than
MathML content.
XSLT provides a rewriting system for XML expressions. This allows one to:
He explained his style-sheet for differentiating all the formulae
in a Web page (as taught at UWO). So XSLT could expand
<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”.
AS spoke about the work at Florida State University using OpenMath to build a problem-solving environment in climatology. One problem is the heterogeneity of the target machines: workstations for debugging and teraflop machines for production. This environment would have to include NAG routines3, computer algebra, PDE solvers and statistical packages.
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.
MR spoke to this issue, based on work going on at Eindhoven. He noted that the standard specifies that the phrasebook has to translate to/from back-engine syntax, but does not say that it has to be at the back-engine. In his opinion, the phrasebook also had to establish the communication with the back-engine. he asked how CDs should be incorporated in phrasebooks, and how new CDs were to be instantiated. Java provides load-on-demand, so it would be possible for the phrasebook to load new modules for new CDs.
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.
MK spoke to this topic. Last year, he had made proposals to enhance OpenMath so that Content Dictionaries would be more useful in theorem proving. The MathWeb project had identified the following problems.
He therefore wanted to make CDs into “first-class objects”. In particular we need an infrastructure for maintaining and manipulating CDs. He claimed that we should be looking at mathematical texts – OMDoc, rather than just individual formulae – OMOBJ. OMDoc consists of the following elements:
omtext etc.;premises, as well as methods.Theory management is important – an 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.
Till Mossakowski (TM)5 spoke to the Common Algebraic Specification Language. CASL comes out of the CoFI (Common Framework Initiative) collaboration, whose aims are:
A draft design had been tentatively approved by IFIP WG 1.3 in May 1997, and the design was finalised in October 1998. It is hoped that it will get full IFIP endorsement this autumn. It is based on first-order predicate logic, with sort generation constraints, partial functions and subsorts.
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 [Edit (2021):
now at http://www.informatik.uni-bremen.de/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.
AMC commented that there were problems with the SFU library, since none of the official versions of it were compatible with the standard. Therefore the INRIA libraries should be regarded as the official ones. The OpenMath web page should contain a clear view of the officially-supported tools, libraries as well as editors. AS asked about the distribution of the tools produced in the project, in view of the Esprit contract. AMC pointed out that the main concern of the reviewers was that OpenMath should be used. MK said that, from the outside, there seemed to be no tools available, and there had been no progress since Eindhoven last year. MK had some tools he could make available.
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.