“KWARC was!”

We are thinking about how to reference theory-constitutive elements in content dictionaries. We had distinguished “reference by location” (via usual URIs) and “reference by context” (via the OMDoc theories and their constitutive elements) in OMDoc 1.1. It was very hard to explain the latter, and the encoding was a little weird, so I dropped it again from OMDoc 1.2. But the concept is valid and important, so here we go again.

This topic is important, since we are thinking about OpenMath3 and we are adding CDs in MathML3. And I guess that there will be quite a while until we can change these two again, so we better get it right. Moreover, the referencing scheme better be compatible with those two.

Here is the idea: we have nested theories in OMDoc1.2, and we need to reference symbols from them. Now, symbols are referenced by their name, which need not be document-unique (and we do not want to do that, since we want to compose theories in documents. That is why their names have three components: the theory name (cd name in OM; which is document-unique at least in OMDoc), and a symbol name, which is theory/cd-unique. And to disambiguate we have URIs for the cds in the cdbase attribute.

We would like to generalize that in OMDoc1.8, theory names should only be unique in their context (which might be the document context or a theory). So far so good, but then we need a path-like referencing scheme at least for the cd names. So we can really combine them in one path/URI as described in a post on MathML/OM referencing.

The next step in OMDoc would be to allow any content element to be theory-like, and allow it to import. Here is a somewhat extreme example of what we would be able to do.

<!-- all statements are theories, so this is also one -->
<symbol name="nat"/>

<!– this symbol declaration imports from theory “nat” –>
<symbol name=”zero”>
<imports=”nat”/>
<type><csymbol pref=”nat/nat”/></type>
</symbol>

<!– this one also needs a function type, so we import it –>
<symbol name=”suc”>
<imports=”nat”/>
<imports=”simple-types”/>
<type>
<apply>
<csymbol pref=”simple-types/funtype”/>
<csymbol pref=”nat”/>
<csymbol pref=”nat”/>
</apply>
</type>
</symbol>

<!– the third Peano Axiom (1&2 are about types) is only about suc –>
<axiom name=”peano3″>
<imports from=”suc”/>
<imports from=”quant1″/>
<bind>
<csymbol pref=”quant1/forall”/>
<bvar><ci>a</ci><ci>b</ci></bvar>
<apply>
<iff/>
<apply><eq/><ci>a</ci><ci>b</ci></apply>
<apply><eq/>
<apply><csymbol pref=”suc/suc”/><ci>a</ci></apply>
<apply><csymbol pref=”suc/suc”/><ci>b</ci></apply>
</apply>
</apply>
</bind>
</axiom>

We are currntly working at an aligned OpenMath/cMathML model for mathematical objects, based on the model for OpenMath objects. This will go into the MathmL3 and OpenMath3 specifications due in spring. Afterwards we will not be able to change much for a long time I expect, so we better get this one right.

There has been some discussion abouth the OpenMath referencing triplet: a symbol (OMS in OM) has three attributes a name, a cd, and a cdbase, e.g. the symbol for addition might be
<OMS cdbase="http://openmath.org/cds" cd="arith1" name="plus"/>

The cdbase and cd attributes determines a content dictionary (in this case the file http://openmath.org/cds/arith1.ocd) and the name attribute a symbol declaration in it (the name of that must be cd-unique).

In MathML3 we want to follow the same general model, but have the definitionURL attribute for specifying meaning. Here we would use the URL http://openmath.org/cds/arith1#plus currently. There was some discussion whether we should have one big CD for MathML or many small ones, … Sam Dooley remarked that if we were to use the OM triplet, then he would like to treat the cd attribute like a cdbase now, which inherits…, then we could write <apply cd="mathml">...<csymbol name="plus"/> ...</apply> (especially if we had one big CD for all MathML, then we could make the cd=”mathml” a default on the <math> element…). Frankly I find this quite attractive (after having thought about it).

I would like to take this idea a little further in MathML3: like MathML2 we use a single URI-type attribute for symbol referencing, let’s call it pref (path ref; just to distinguish it from definitionURL for this post, it could in the end becomd definitionURL to keep backwards compatibility; after all MathML does not say what kind of URLs definitionURL should be; convenient).

So we use pref attributes on csymbols, and take xml:base into the picture we can write

<csymbol pref="http://openmath.org/cds/arith1/plus"/>

<math xml:base="http://openmath.org/cds/">.... <csymbol pref="arith1/plus"/>...</math>

and even

<math xml:base="http://openmath.org/cds/">
<apply xml:base="arith1">
<csymbol pref="plus"/>...</math>
</apply>
</math>


This would make a very simple framework. All the URIs can be used for REST-ful access to the relevant features (symbol declarations in the CDs), and relative URIs work as expected. And if we write content dictionaries in a somewhat atomic way, then we can even supply them on a static web server. It would be quite simple to configure apache that it really generates the right files, for instance, in the directory …/arith1 we could have ocd.php with the CD skeleton and inclusions for the symbol declarations which are represented as files in the directory. e.g. arith1/plus.

That would make it quite simple to set up a structure that would make the cds meaningful.