From MathWeb

Ideas for addressing and naming things in OMDoc 2.0 (Michael, Florian, Christoph):

Contents 1 Goals 2 Referencing 3 Data model 3.1 Storage considerations

Goals

• make every theory-constitutive element referrable to.
• try to be compatible with existing XML standards
• Maintain theory-constitutivity at any price, even without MoC. The idea in OMDoc 1.2 was: constitutive elements must be part of their home theory element. If one write-protects the theory, its constitutive parts are also write-protected.

Referencing

• allow for document-orientied referencing (e.g. by XML IDs) and for semantic referencing – regardless of the physical position of a thing, make it referable to.
  • (See also this blogpost, where it's called "reference by location" vs. "reference by context".)
• absolute references always via whole URLs
• in an OMS, concatenating cdbase+cd+name (with slashes in between) should yield an URL, same as csymbol/@definitionURL in MathML.
  • (See this blogpost for more information.)
• Consider using xml:base standard instead of cdbase
• Use referencing by XML ID (e.g. doc.omdoc#frag-id) as fallback for generic XML tools that do not know OMDoc

Data model

• Turn every referable thing, including theory-constitutive statements, into a file (optionally) – e.g. http://cds.omdoc.org/arith1/plus
  • I don't like this. - Florian
  • Either a statement is included in a theory (and not an own file), or it lives in an own file and then behaves like a theory – i.e. it imports everything it needs, also using morphisms if needed. E.g. a symbol imports other symbols or theories needed for declaring its type.
    • I don't like this at all. - Florian
  • Example: symbols 0 and N (for natural numbers) are their own theories. The Peano axiom imports these two symbols. (See this blogpost for a detailed example.)
  • Note: mutually recursive definitions can't live on their own; they must still be wrapped into a common theory.
  • (Re-)introduce a @name attribute for all statements (constitutive and non-constitutive, as they also had a mandatory home theory in OMDoc 1.2, as well as omtext – i.e. everything that's a "con" in the NarCon model introduced by Kohlhase/Müller/Müller, or, in other words: any scoping element); also treat imports like statements.
    • Note: examples/assertions frequently state things about more than one theory, i.e. it's not always easy to put them into a unique "home theory", as required in OMDoc 1.2
    • There is one namespace for everything with a name attribute in a theory, i.e. there cannot be an axiom and a symbol with the same name. Note: Imported files from other systems may have to be pre-processed, e.g. a symbol "foo" renamed to "sym-foo".
  • If everything is in one theory, treat the "new" symbols/axioms/etc. like sub-theories in OMDoc 1.2.
    • I don't like this at all. - Florian

Storage considerations

• This allows for using the same URL scheme for both the file system and OMBase.
  • A good idea, but I don't expect it to work well. I think it's better to provide a very light database that users install locally. This might even just be a shell script that takes a database query and returns the file or xpointer reference of the queried element. - Florian
    • Yes, but that database must or script must be optional. And a minimum support must also be offered for people who don't install this.
• A theory might then have a main document like http://cds.omdoc.org/arith1/index.xml containing code like

<theory>
<ref .../>
</theory>

• • This is still unclear --Clange 12:24, 2 July 2007 (CEST)
• Allow for relative paths using ../: OK in the file system, but must also be supported by OMBase
  • Problem: What if we have multiple theories in a one-file OMDoc? Referring to ../other-theory/sym would, according to URL standards, refer to another document named other-theory, not to a sibling theory in the same document. Need to clarify! --Clange 12:24, 2 July 2007 (CEST)
  • I.e. we need a different addressing scheme for one-file OMDocs, but this needs only be supported by an intelligent OMDoc-aware application, not by generic XML applications. Proposal: introduce a custom XPointer scheme like #ompath(../other-theory/sym). Exporting such files yields a directory tree, where every statement lives in its own file.
• Note: If files have names without a .omdoc extension, the web server must assign the correct OMDoc MIME type to them. Need to find out whether this works in .htaccess files. Maybe using URL rewriting?
  • Question: If a statement with a name lives in its own file, can/should it then have a @name attribute, too? May its value differ from the file name?
• What if something that was a big theory in OMDoc 1.2 is split into many atomic theories? How can one retrieve these efficiently?
  • In the file system, without any support, it requires inefficient crawling of lots of documents.
  • An intelligent application would cache imports on a higher level (e.g. SWiM or maybe OMBase using ABox extraction to RDF), which allows for efficient queries for any theory that is a constitutive element and imports this one.
  • Question: can't distinguish the imports between constitutive elements of this theory and other theories any more. --Clange 12:24, 2 July 2007 (CEST)
  • URL-encode (i.e. %XX, XX=hex-code) symbol names forbidden in XML (e.g. -> or \) from other systems, such as Twelf. While one could relax the restrictions for the @name attribute itself, referring to names requires an URL and thereby URL encoding.