Newer
Older
\subparagraph{Language}
\omdoc \cite{omdoc} (short for \textbf{O}pen \textbf{M}athema\-ti\-cal \textbf{Doc}uments) is a semantics-oriented XML-based markup format for STEM-related documents.
It conceptualizes mathematical objects in three levels as seen in Figure~\ref{fig:levels}: the \emph{object} level for mathematical formulas and their presentations, the \emph{statement} level for definitions, theorems, proofs, etc, and the \emph{theory} level for collections of statements.
Each level comes in two dimensions for the formal representations of the content addressed to mathematical software systems and the narrative structure addressed to humans.
Higher levels may contain expressions of lower ones, and mixtures of dimensions are allowed, leading to a overall format that can handle flexible levels of formality (see~\cite{Kohlhase:tffm13} for a discussion).
\begin{wrapfigure}r{8cm}\vspace*{-1em}
\begin{tabular}{|l|l|l|}\hline
level & formal & narrative \\\hline\hline
object & OpenMath & presentation MathML \\\hline
statement & sequents & paragraphs + cues\\\hline
theory & theories/views & sections, etc.\\\hline
\end{tabular}\vspace*{-.5em}
\caption{Three level \& two dimensions in OMDoc}\label{fig:levels}\vspace*{-.5em}
\end{wrapfigure}
Even at the early state in 1999, \omdoc already had this general architecture and was therefore well-suited in principle for representing Isabelle content, in particular the Isar proof language \cite{Wenzel:1999:TPHOL} that was new at the time.
But the formal part of \omdoc was purely descriptive and lacked a rigorous semantics.
In particular, the role of the logical systems needed for formally stating mathematical properties was almost fully unspecified beyond the idea --- inherited from OpenMath --- that logics are theories as well.
Later \mmt (Meta Meta Theories) \cite{RK:mmt:10} re-conceptualized and refined the formal fragment of \omdoc, greatly enhancing both rigor and expressivity.
It models formal objects and statements using logical frameworks, in particular the judgments-as-types paradigm, and bases \omdoc's theory level on the category of theories and theory morphisms following the development graphs approach \cite{devgraphs}.
The former allows for fine-grained specifications of the semantics of individual objects, and the latter allows for inducing and translating knowledge across theories.
A new \emph{meta-theory} relation links a logical framework to the logics defined in it, thus formalizing the ``logics-as-theories'' approach.
The \omdoc/\mmt language is implemented in the \mmt system (Meta Meta Toolset; see~\cite{rabe:howto:14}), which provides an API for the language constructs at all levels and provides both logical services such as type reconstruction and rewriting and knowledge management services such as IDE and HTML presentation and browsing of libraries.
Because it avoids committing to a specific semantics or logical foundation, foundation-dependent services and features (e.g., type reconstruction) are implemented by splitting the algorithms into a foundation-independent kernel that is user-extensible with foundation-specific rules.
For example, the logical framework LF \cite{lf} is implemented using about 10 rules taking only a few lines of code each.
\subparagraph{Theory Graphs}
Theory graphs are diagrams in the categories of theories and morphisms.
The possible morphisms in \mmt are \textbf{inclusions}, which import all declarations from the domain to the co-domain, \textbf{structures}, which are like includes but copy and translate all declarations, \textbf{views}, which are semantics-preserving translations from domain to codomain, and the \textbf{meta-theory}-relation, which behaves like an include for most purposes.
\begin{wrapfigure}{l}{0.43\textwidth}\vspace*{-.75em}
\providecommand\cn[1]{\ensuremath{\mathsf{#1}}}
\providecommand\myyscale{1}
\providecommand\myxscale{1}
\def\outerthysep{.3mm}
\def\innerthysep{.5mm}
\tikzstyle{thy}=[draw,outer sep=\outerthysep,rounded corners,inner sep=\innerthysep]
\newcommand{\mmtarrowtipmonoright}{right hook}
\newcommand{\mmtarrowtip}{angle 45}
\tikzstyle{meta}=[dotted,-\mmtarrowtip,thick]
\tikzstyle{include}=[\mmtarrowtipmonoright-\mmtarrowtip,thick]
\tikzstyle{view}=[preview,-\mmtarrowtip]
\tikzstyle{struct}=[-\mmtarrowtip,thick]
\usetikzlibrary{decorations,decorations.pathmorphing,decorations.markings}
\tikzstyle{preview}=[decorate, decoration={coil,aspect=0,amplitude=1pt,
segment length=6pt,
pre=lineto,pre length=3pt,
post=lineto,post length=5pt},
thick]
\begin{tikzpicture}[xscale=\myxscale,yscale=\myyscale]
% \draw[view] (-4,2.4) --node[above] {translation} +(2,0);
% \draw[struct] (-4,1.7) --node[above] {import} +(2,0);
% \draw[meta] (-4,1) --node[above] {meta-theory} +(2,0);
\node[thy] (lf) at (0,2.5) {$\cn{LF}$};
\node[thy] (lfx) at (1.8,2.5) {$\cn{LF+X}$};
\node[thy] (fol) at (-1,1.5) {$\cn{FOL}$};
\node[thy] (hol) at (.9,1.5) {$\cn{HOL}$};
\node[thy] (mon) at (-2.5,0) {$\cn{Monoid}$};
\node[thy] (gp) at (-.5,0) {$\cn{CGroup}$};
\node[thy] (rg) at (2,0) {$\cn{Ring}$};
\draw[meta](lf) -- (fol);
\draw[meta](lf) -- (hol);
\draw[meta](fol) -- (mon);
\draw[meta](fol) -- (gp);
\draw[meta](hol) -- (rg);
\draw[include](lf) -- (lfx);
\draw[view](fol) -- node[above] {\footnotesize$\cn{f2h}$} (hol); %$
\draw[struct](gp) to[bend right=10] node[above]
{\footnotesize$\cn{add}$} (rg); %$
\draw[struct](mon) to[out=20,in=160] node[above]
{\footnotesize$\cn{mult}$} (rg); %$
\draw[include](mon) -- (gp);
\draw[view] (fol) to[bend right=30] node[above,near start]{\footnotesize$\cn{folsem}$} (zfc); %$
\draw[view] (mon) -- node[left]{\footnotesize$\cn{mod}$} (zfc); %$
Figure~\ref{fig:tgraph} shows an example of a typical setup of formalizations in \mmt: Dotted lines represent the meta-theory-relation, hooked arrows are includes, squiggly arrows represent views, and the normal arrows represent named structures.
Here LF is used as a logical framework to define some logics, which are then used as meta-theories for algebraic theories.
\begin{newpart}{MK: an extension which explains the setup}
We see three pragmatic levels: the logical frameworks at the top, logics in the middle, and the domain theories at the bottom.
Meaning trickles down from the theories at the top (the ones without meta-theories), which are implemented directly in \mmt/Scala as described for LF above.
This setup can even encode model theory theory morphisms into semantic theories like ZFC set theory.
=======
We see three pragmatic levels: the logical frameworks (meta-meta-theories) at the top, logics (meta-theories) in the middle and the domain theories at the bottom.
Meaning trickles down from \emph{ur-theories} -- which have no meta-theory and which are implemented directly in MMT/Scala as described for LF above -- via the meta-theory-relation.
This setup can even encode model-theory via views (interpretations) into foundational theories like ZFC set theory.
>>>>>>> adeb0e7... less ednotes
%%% Local Variables:
%%% mode: latex
%%% mode: visual-line
%%% fill-column: 5000
%%% TeX-master: "paper"
%%% End:
% LocalWords: omdoc omdoc athema uments conceptualizes sequents re-conceptualized devgraphs formalizing mmtsys lf myyscale myxscale outerthysep innerthysep tikzstyle draw,outer outerthysep,rounded corners,inner newcommand mmtarrowtipmonoright mmtarrowtip mmtarrowtip,thick usetikzlibrary decorations,decorations.pathmorphing,decorations.markings coil,aspect 0,amplitude lineto,pre lineto,post fig:tgraph Kohlhase:tffm13 0,amplitude