Theories and Theory Morphism in OMDoc

Discussion with a mathematician

Further Discussions and TODOs

  • Understand Florian's work
  • Understand construction of mathematical notations

Notes of meeting with Florian (November 14th 2008)

  • Q: FOL Theories for connected graph and binomial coefficient? A: Introduction of specific relations e.g. 
       edge(x,y) => connected(x,y)
   connected(x,y) /\ edge(y,z) => connected(x,z)

       0! = 1
   forall n. (n+1)! = (n+1) * n!
  • Q: Can you really model any proof in OMDoc? A: Theory morphism do not replace proofs. We rather aim at the reuse of proofs by identifying the minimal preconditions (properties) for the proof. This gives a good overview on which properties are necessary to complete a proof
  • Reverse mathematics is similar: There you identify all axioms that are necessary for theorem. And you have a lot of interpretations; see  Simpson's book. In reverse mathematics you rather have a star shape
  • Q: What can be modeled with OMDoc? FOL, HOL, ... A: When writing a theory you have to choose a particular logic, e.g. you write a FOL theory or a HOL theory. You can then define theories for logics, which eventually allows you to translate between theories (see Florian's dissertation)
  • OMDoc is a generic approach. We do not focus on analysing mathematical structures but rather to support software engineering processes e.g. to allow to represent modular software specifications. An example for a theory morphism in SW Engineering are refinements, i.e. specialization steps in the engineering process. You start with declarative user requirements and refine these step by step until you reach an imperative specification that you can eventually implement; in the former version you have a lot of unknown and unspecified things that become more and more concrete in the refinement process. For example, take a ring specification and the respective implementation you can find a theory morphism between both
  • Immanuel focusses on finding new theory morphism, i.e. postulated theory morphism. He particular focusses on FOL.
  • Q: So what is the overall goal of OMDoc. Do you expect me, as a mathematician, to write it? A: In the long term, OMDoc shall become a document format. As it is XML we do not expect anyone to write OMDoc. This is why Michael set up an LaTeX-workflow: You can add semantic macros to your LaTeX source, modify your document structure respectively, and eventually (based on LaTeXML) generate XML, i.e. OMDoc from it. Michael says that using sTeX is a 10% increase in effort, but you can benefit from a lot of services already (and we are working on many more: e.g. when changing a definition you can see which parts in the document are affected, you can verify whether all symbols you use have been defined, you can identified cycles in your references etc.)

Notes on prior eMail discussions and Pointers

see Florian's reply, Immi's reply, and Immi's example

Examples:

  • Bourbaki Project is our main case study
  • Translation of Mizar into OMDoc (by Elena Digor)
  • Immanuel has been working with the Mizar corpus
  • GenCS material (Michael's slides)
  • examples from category theory:  page 23 in Topoi: the Categorial Analysis of Logic by Rob Goldblatt