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 -->
<!– this symbol declaration imports from theory “nat” –>
<!– this one also needs a function type, so we import it –>
<!– the third Peano Axiom (1&2 are about types) is only about suc –>