Skip to content
Snippets Groups Projects
Commit 463d306e authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

reorganized

parent a730edaa
No related branches found
No related tags found
No related merge requests found
...@@ -9,6 +9,23 @@ applicable. ...@@ -9,6 +9,23 @@ applicable.
\ednote{Interesting theoretical, practical, and social/organizational problems $\leadsto$ \ednote{Interesting theoretical, practical, and social/organizational problems $\leadsto$
OAFF} OAFF}
\begin{oldpart}{from bluenote}
A central idea behind the OMDoc/OpenMath data model is that all symbols have a home
theory (the document that introduced the concept; essentially the content
dictionary). In the context of flexiformal\footnote{i.e. formalized to flexible depths;
see~\cite{KohKoh:tfndc11} and ~\cite{Kohlhase:tffm13} for a discussion of this
notion.} digital libraries, this information design creates a tension between
usability (which demand standardized content dictionaries) and flexibility/locality.
\ednote{Expand, discuss the alternatives, discuss multiple theories and
realms~\cite{CarFarKoh:tr13}.}
\end{oldpart}
\subsection{Services}
\begin{todolist}{expand}
\item auto-generation of recap material from content commons
\item need a community process of moving ``original theory'' towards encyclopedias.
\end{todolist}
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
%%% TeX-master: "paper" %%% TeX-master: "paper"
......
No preview for this file type
...@@ -76,13 +76,13 @@ ...@@ -76,13 +76,13 @@
\section{Introduction}\label{sec:intro} \section{Introduction}\label{sec:intro}
\input{intro} \input{intro}
\section{Preliminaries}\label{sec:prel} % \section{Preliminaries}\label{sec:prel}
\input{prel} % \input{prel}
\section{Theory Level Phenomena in Informal Mathematics}\label{sec:pheno} \section{Establishing Common Ground in Mathematical Documents}\label{sec:pheno}
\input{phenomena} \input{phenomena}
\section{Publication and Dissemination in MMT/OMDoc Theory Graphs}\label{sec:patterns} \section{Publication and Dissemination in Theory Graphs}\label{sec:patterns}
\input{patterns} \input{patterns}
%\input{oldparts} %\input{oldparts}
......
...@@ -2,22 +2,108 @@ In this section we look more closely at the examples from section \ref{sec:pheno ...@@ -2,22 +2,108 @@ In this section we look more closely at the examples from section \ref{sec:pheno
each can be represented using theory graphs. But first, we look at the aspects common to each can be represented using theory graphs. But first, we look at the aspects common to
all examples to form an intuition of the theory graphs structures that are needed. all examples to form an intuition of the theory graphs structures that are needed.
The examples in section \ref{sec:pheno} are each slightly different but they have fundamental common aspects. The examples in section \ref{sec:pheno} are each slightly different but they have
First, each paper starts with establishing a common ground on which the results of the paper are built. This leverages the literature in two ways. fundamental common aspects. First, each paper starts with establishing a common ground on
which the results of the paper are built. This leverages the literature in two ways.
\begin{itemize} \begin{itemize}
\item Firstly, concepts from the literature are used to conveniently build up the local definitions. From the theory graphs perspective \item Firstly, concepts from the literature are used to conveniently build up the local
this functions as a (possibly partial) import. definitions. From the theory graphs perspective this functions as a (possibly partial)
\item Secondly, properties of locally introduced concepts are \emph{adopted} from the literature. Mathematically, this is justified by import.
and (implicit or explicit) subsumption between the local definition and that used by the referenced theorem. \item Secondly, properties of locally introduced concepts are \emph{adopted} from the
From the theory graph perspective this function as a theory morphism that induces the properties locally due to its truth-preserving semantics. literature. Mathematically, this is justified by and (implicit or explicit) subsumption
between the local definition and that used by the referenced theorem. From the theory
graph perspective this function as a theory morphism that induces the properties locally
due to its truth-preserving semantics.
\end{itemize} \end{itemize}
Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads to a theory of the main contxribution of the paper. Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads
to a theory of the main contxribution of the paper.
Secondly, the notion of ``literature'' and the existence of concepts beyond a particular
definition (so that equivalent definitions imply one is talking about the same platonic
concept) are common to all examples. We believe that what happens in mathematical practice
is that definition and foundational choices are abstracted away as implementation details
and the important concepts and their properties are used as an interface to each theory
(in the mathematical sense, e.g. group theory). But this is precisely the situation that
realms try to capture in theory graphs. Therefore, we maintain that, from a theory graph
perspective, informal mathematical papers refer (and contribute to) realms rather than
individual theories.
\subsection{Realms}\label{sec:prel-realms}
Intuitively, a realm \cite{CarFarKoh:rsckmt14} is a theory structure in a theory graph $\gamma$ (i.e. a subgraph of $\gamma$) that abstracts from the development
and provides practitioners with the useful symbols and theorems via an \emph{interface theory}.
% \begin{definition}
% A \emph{realm} $R$ is a tuple $(G, F, C, V, I)$ where :
% \begin{itemize}
% \item $G$ is a theory graph
% \item $F$ is a theory in $G$ called the \emph{interface theory} or (\emph{face}) of $F$
% \item $C$ is a set $\{C_1, C_2, \ldots, C_n\}$ of conservative developments in $G$. We call a subgraph a conservative development
% if all theories in it are conservative extensions of one bottom theory (usually called $\bot$) that is also in the graph. We call each conservative extension a \emph{pillar}
% of the realm.
% \item $V$ is a set of views that establish that the bottom theories $\bot_1, \bot_2, \ldots, \bot_n$ of $C_1, C_2, \ldots, C_n$ are pairwise equivalent.
% \item $I$ is a set of views from $F$ to the top theories $\top_1, \top_2, \ldots, \top_n$ of $C_1, C_2, \ldots, C_n$ that ensure $F$ can act as an interface for each of them.
% \end{itemize}
%
% \end{definition}
\begin{wrapfigure}r{6.3cm}\vspace*{-2em}
\begin{tikzpicture}[xscale=.7]
%realm
\draw[realm] (-1,-1.8) rectangle (8,2.8) {};
%p1
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p..
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
%pn
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (5.5,-1.5) rectangle (7.5,1.8) {};
\node (r-name) at (7.3,2.6) {$\mathit{Realm}$};
\node (p1-name) at (0.2,1.6) {$\mathit{Pillar_1}$};
% \node (p2-name) at (3,1.6) {$\mathit{Pillar_{\ldots}}$};
\node (p3-name) at (6.8,1.6) {$\mathit{Pillar_n}$};
\node[thy] (top1) at (0.5,1) {$\top_1$};
\node[thy] (bot1) at (0.5,-1) {$\bot_1$};
\node[thy] (top2) at (3.5,1) {$\top_{\ldots}$};
\node[thy] (bot2) at (3.5,-1) {$\bot_{\ldots}$};
\node[thy] (top3) at (6.5,1) {$\top_n$};
\node[thy] (bot3) at (6.5,-1) {$\bot_n$};
\node[thy] (r) at (3.5,2.3) {$\;\;\;\;\;F\;\;\;\;\;$};
\draw[view] (r) to node[above] {$\cn{I_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{I_{\ldots}}$} (top2);
\draw[view] (r) to node[above] {$\cn{I_n}$} (top3);
\draw[conservative] (bot1) to node[left] {$C_1$} (top1);
\draw[conservative] (bot2) to node[left] {$C_{\ldots}$} (top2);
\draw[conservative] (bot3) to node[left] {$C_n$} (top3);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot3);
\draw[view, bend left = 10] (bot3) to (bot2);
\end{tikzpicture}
\caption{The architecture of a realm}\label{fig:realm}\vspace*{-1em}
\end{wrapfigure}
Figure \ref{fig:realm} shows a prototypical realm with $F$ as its interface theory (also
called a \emph{face}) and $n$ pillars each representing a different (yet equivalent)
development of the concepts in the face. Common examples are the different ways to define
natural or real numbers. Each pillar is a conservative development in the sense that all
theories in a pillar are conservative extensions of a bottom theory (denoted with
$\bot$). A top theory (denoted with $\top$) aggregates all symbols, axioms and theorems
declared within the pillar. The view pairs at the bottom establish the equivalence of the
pillars and the $n$ views $I_k$ capture the relation of interface-implementation between
the face and each pillar. See \cite{CarFarKoh:rsckmt14} for the complete definition and
more examples.
Secondly, the notion of ``literature'' and the existence of concepts beyond a particular definition (so that equivalent definitions imply one is
talking about the same platonic concept) are common to all examples. We believe that what happens in mathematical practice is that definition and foundational
choices are abstracted away as implementation details and the important concepts and their properties are used as an interface to each theory (in the mathematical sense,
e.g. group theory). But this is precisely the situation that realms try to capture in theory graphs. Therefore, we maintain that, from a theory graph perspective, informal
mathematical papers refer (and contribute to) realms rather than individual theories.
\subsection{Realms in Informal Mathematics} \subsection{Realms in Informal Mathematics}
...@@ -91,7 +177,7 @@ In that situation we have three subcases depending on the relation between the r ...@@ -91,7 +177,7 @@ In that situation we have three subcases depending on the relation between the r
\emph{equivalence recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and \emph{generalization recap} (\ref{rc:ge}). \emph{equivalence recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and \emph{generalization recap} (\ref{rc:ge}).
\paragraph{Special case: Plain/Simple Recaps} \label{rc:pl} \subsection{Special case: Plain/Simple Recaps} \label{rc:pl}
One situation is that of plain recaps where the relation $r$ is an inclusion into the recap from the cited paper. One situation is that of plain recaps where the relation $r$ is an inclusion into the recap from the cited paper.
Typically the include $r$ is a conservative extension of the cited paper. Typically the include $r$ is a conservative extension of the cited paper.
For instance the \emph{covers of the multiplicative group} from example \ref{ex:covers} directly uses the concept from the cited paper, For instance the \emph{covers of the multiplicative group} from example \ref{ex:covers} directly uses the concept from the cited paper,
...@@ -195,21 +281,26 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity. ...@@ -195,21 +281,26 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers} \caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\end{figure} \end{figure}
\paragraph{Special Case: Equivalence Recap} \label{rc:eq} Another common situation is that \subsection{Special Case: Equivalence Recap} \label{rc:eq} Another common situation is that
of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the
two theories. We can represent the relation $r$, in this case, as two views $v_{to}$ and two theories. We can represent the relation $r$, in this case, as two views $v_{to}$ and
$v_{from}$, one in each direction between the recap and the cited paper that ensure their $v_{from}$, one in each direction between the recap and the cited paper that ensure their
isomorphism. Then, the view $v$ is induced by $v_{from} \circ v_1$ modulo conservativity. isomorphism. Then, the view $v$ is induced by $v_{from} \circ v_1$ modulo conservativity.
Moreover, the contribution of the paper carries over to the realm via the view $v_{to}$. Moreover, the contribution of the paper carries over to the realm via the view $v_{to}$.
This occurs, for instance, in example \ref{ex:mnets} where this intuition is explicitly written down in the paper as ``There are several equivalent ways to This occurs, for instance, in example \ref{ex:mnets} where this intuition is explicitly
define multinets.'' (although not proved). Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category. written down in the paper as ``\textsf{There are several equivalent ways to define
In fact it is the most common situation in the sample papers we studied. multinets.}'' (although not proved). In fact it is the most common situation in the
sample papers we studied.
% Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category.
\begin{oldpart}{either put somewhere or delete} \begin{oldpart}{either put somewhere or delete}
The implicit or explicit equivalence of the local definitions in the recap theory that the view $v$ from the face exists and therefore that theorems from the mathematical The implicit or explicit equivalence of the local definitions in the recap theory that
field can be used in the paper. In case the equivalence is implicit we speak of a \emph{postulated} view, i.e. one where the assigned expressions are (partially) informal. the view $v$ from the face exists and therefore that theorems from the mathematical
A flexiformal system can still reason about the meaning travel induced by a postulated view but cannot look into assigned objects and e.g. proof check them. field can be used in the paper. In case the equivalence is implicit we speak of a
\emph{postulated} view, i.e. one where the assigned expressions are (partially)
informal. A flexiformal system can still reason about the meaning travel induced by a
postulated view but cannot look into assigned objects and e.g. proof check them.
\end{oldpart} \end{oldpart}
...@@ -326,7 +417,7 @@ we take into account conservativity to reduce them to the $\bot$ theory. ...@@ -326,7 +417,7 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\paragraph{Special Case: Specialization Recap} \label{rc:sp} \subsection{Special Case: Specialization Recap} \label{rc:sp}
Thirdly, we have the case where $r$ is a specialization relation that can be represented as a view $v_{from}$ from the cited theory to the recap. Thirdly, we have the case where $r$ is a specialization relation that can be represented as a view $v_{from}$ from the cited theory to the recap.
Same as in the previous case, this ensures the existence of $v$ as $v_{from} \circ v_1$ modulo conservativity. Same as in the previous case, this ensures the existence of $v$ as $v_{from} \circ v_1$ modulo conservativity.
However it does not directly contribute the paper results back to the (same) realm as they concern a special case of the concepts in the realm. However it does not directly contribute the paper results back to the (same) realm as they concern a special case of the concepts in the realm.
......
\subsection{The Structure of informal Mathematical Documents}
Mathematical documents traditionally have:
\begin{compactenum}
\item A \defemph{front/backmatter} and \defemph{page margins}, which identify the
scientific metadata:
\begin{inparaenum}[\em i\rm)]
\item author's names, affiliations, and addresses,
\item publication venue, date, and fragment identifiers (e.g. page numbers),
\item classification data, e.g. keywords or MSC codes,
\item acknowledgements of contributions of other researchers or funding agencies.
\item access conditions, e.g. copyright, confidentiality designations, or licenses.
\end{inparaenum}
\item An \defemph{abstract} that gives an executive overview over the document.
\item An \defemph{introduction} that leads the reader into the topic, discusses the
problems solved in the document and their relation to the ``real world'', and generally
argues that reading the paper is worth the reader's attention.
\item A \defemph{preview}, which outlines the structure of, the contributions in, and
methods used in the document.
\item A discussion of the \defemph{state of the art} on the topic of document.
\item The establishment of a \defemph{common ground} between the reader and the author,
which
\begin{inparaenum}[\em i\rm)]
\item recapitulates or surveys concepts and results from the documents/knowledge commons
to make the document self-contained (for its intended audience)
\item identifies any assumptions and give the ensuing contributions a sound
terminological basis
\end{inparaenum}
\item The \defemph{contributions} part, which contains the development of new knowledge in
form of e.g. new insights, new interpretations of known concepts, new theorems, new
proofs, new applications/examples or new techniques of achieving results.
\item An \defemph{evaluation} of the contributions in terms of applicability or even
usability.
\item A discussion of \defemph{related work} which reviews the contributions and their
relation to existing approaches and results from the literature
\item A \defemph{conclusion} which summarizes the contribution with the benefit of
hindsight and relates it to the claims made in the introduction.
\item Literature references, an index, a glossary, etc. and possibly appendices that
contain material deemed supplementary to the contributions.
\end{compactenum}
Even though the form or order of the structural elements may vary over publication venues,
and certain elements may be implicit or even missing altogether, the overall structure is
surprisingly stable.
\subsection{Common Ground/Recapitulation in Papers} \subsection{Common Ground/Recapitulation in Papers}
A common pattern occurs in scientific papers which often have a preliminaries section to A common pattern occurs in scientific papers which often have a preliminaries section to
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment