Newer
Older
In this section we look more closely at the examples from section \ref{sec:pheno} and how
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.
The examples in section \ref{sec:pheno} are each slightly different but they have
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.
\item Firstly, concepts from the literature are used to conveniently build up the local
definitions. From the theory graphs perspective this functions as a (possibly partial)
import.
\item Secondly, properties of locally introduced concepts are \emph{adopted} from the
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.
Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads
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}
\ednote{MI@MI need to introduce basic MMT/theory graph concepts, theories views, includes. Additionally conservative developments and its relation with views}
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
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.
\subsection{Realms as a Model for Dissemination \& Aggregation}
Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part
of a theory graph. The ``literature'' for the mathematical theory to which the paper
contributes is represented as a realm with a face and several pillars. The paper
references a document within the field, that is naturally part of a pillar and grounds the
recap theory. The contribution of the paper is a theory in itself that includes the recap
theory and is a conservative extension of it. Again, the fact that we are representing the
contribution in a single theory is a simplification for presentational simplicity which
does not lead to a loss of generality. The view $v$ ensures that the paper can make use of
concepts and theorems from the realm, as they can be accessed via $v$.
In our analysis we restrict ourselves to the case where there is a single recap for
simplicity and expositional clarity. The approach can be extended to multiple recaps from
the same realm with minimal effort -- but the diagrams become messy. This already covers
the majority of research papers we have analyzed; they build on an earlier paper and
extend it. Indeed, all three examples from Section~\ref{sec:cg-preprints} fall into this
category, they import the definitions and terminology from a central cited paper, but call
on others from the same realm for results, context, and support.
%Mathematical papers re-introduce concepts with the implied assumption of semantic equivalence in the context of the paper.
%I.e. every statement in the paper holds for the original definition too, but not necessarily the converse.
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p-name) at (-1.7,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[->] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
We recognize four special cases for recaps based on the nature of $r$ and discuss each
individually below. First we have to decide the home theory of the symbols that the recap
introduces. If the home is the cited theory then $r$ is an import then we have a
\emph{plain recap} (\ref{rc:pl}) . Otherwise, we have new symbols in the recap theory
that are somehow related with the ones in the cited one. In that situation we have three
sub-cases depending on the relation between the recap and cited theory: \emph{equivalence
recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and \emph{generalization
recap} (\ref{rc:ge}).
\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. Typically the include $r$ is a conservative extension of the
cited paper. For instance the ``\textsf{covers of the multiplicative group}'' from
example \ref{ex:covers} directly uses the concept from the cited paper, but gives a
concise verbalization of its definition. This allows it to make use of the result the
results in two other papers higher up in the pillar of the cited paper. The situation is
shown in figure \ref{fig:rec-covers} Note that, if $r$ is conservative, then we have a
\textbf{pillar extension} for the realm justifies the new paper becoming part of the
realm's literature. It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{CACF}};
\node[thy] (pcont) at (-3,2) {\cn{MToCACF}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[conservative,red] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Publication graph for plain recaps (Example \ref{ex:covers})}\label{fig:rec-covers}
\node (p1-name) at (-2,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-1.5,-1) {\cn{CACF}};
\node[thy] (pcont) at (-1.5,0) {\cn{MToCACF}};
\node[thy] (top1) at (-0.5,1) {$\top$};
\node[thy] (tcdots1) at (0.5,-0.5) {$\cdots$};
\node[thy] (citp) at (-0.5,-2) {Cited Paper};
\node[thy] (top2) at (3.5,1) {$\top$};
\node[thy] (bot2) at (3.5,-3) {$\bot$};
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[conservative,red] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (tcdots1);
\draw[conservative] (tcdots1) to (top1);
\draw[conservative] (pcont) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Aggregation graph for plain recaps (Example \ref{ex:covers})}\label{fig:agg-covers}
\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 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 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}$.
This occurs, for instance, in example \ref{ex:mnets} where this intuition is explicitly
written down in the paper as ``\textsf{There are several equivalent ways to define
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.
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{MNets}};
\node[thy] (pcont) at (-3,2) {\cn{ICMnets}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red, bend left = 10] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 10] (recap) to node[above] {$\cn{v_{to}}$} (citp);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Publication graph for equivalence recaps (Example \ref{ex:mnets})}\label{fig:rec-mnets}
Note that adding an equivalent definition corresponds to a \textbf{realm extension}, where
the face is fixed, and the view from the face to the current theory can be
postulated. Therefore, in figure \ref{fig:rec-mnets} the paper effectively extends the
realm (or the current pillar) as introduced in section \ref{sec:prel-realms}. This
corresponds to the mathematical practice of ``contributing to'' a field (or mathematical
theory). This resulting realm after knowledge aggregation is shown in Figure
\ref{fig:rec-mnets-aggr}, where the new paper contributes a new pillar to the realm. The
equivalence is ensured by $v_{from}$ and $v_{to}$ as we take into account conservativity
to reduce them to the $\bot$ theory.
\node (p3-name) at (-2.8,1.6) {$\mathit{Pillar_{n+1}}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (pcont) at (-2.5,1) {\cn{ICMnets}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view,red, bend left = 10] (bot1) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 10] (recap) to node[above] {$\cn{v_{to}}$} (bot1);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Aggregation graph for equivalence recaps (Example \ref{ex:mnets})}\label{fig:rec-mnets-aggr}
\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. 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.
This is the case in example \ref{ex:atm} where the definition from the paper is a
specialization of the one in the literature. In \cite{CalStai:natm09}, the definition of
the accelerated Turing machine involves a concrete step size ($2^{-n}$), whereas the
definition it recaps allows arbitrary sequences of step sizes as long as their sum remains
finite. Thus we have the situation in Figure~\ref{fig:rec-atm}. Theory \cn{ATM} contains
the (opaque) sentence (\ref{lq:atm}), but there cannot be a view from \cn{ATM} to \cn{atm}
as that is more general. But we do have a view to \cn{atm(2^{-n})}, which naturally arises
in treatments of accelerated Turing machines as an example. That special case forms a
realm of its own. \ednote{expand on this}
\ednote{@MK the old version of the ATM case is below as oldpart, the second part I removed because it doesn't fit
precisely but there are some interesting things there, we should talk about it}
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (r2-name) at (-2.1,-1.6) {$\mathit{Realm_2}$};
\node (p-name) at (-4.5,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-5,0) {\cn{ATM}};
\node[thy] (pcont) at (-5,2) {\cn{ATMhalt}};
\node[thy] (citpex) at (-2.5,-1) {$\cn{atm}(2^{-n})$};
\draw[view] (recap) to node[above] {$\cn{v_{to}}$} (citpex);
\draw[include] (citp) to (citpex);
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {atm};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Publication graph for specialization recaps (Example \ref{ex:atm})}\label{fig:rec-atm}
Finally, we have the case where $s$ is a plain (partial) include that does not entail
conservativity and therefore does not entail the existence $v$. In that case we call $v$ a
\emph{postulated} view and the recap itself an \emph{adoption}.
This is the case in example \ref{ex:course} where the recap theory \cn{SET} includes only
the symbols $\in$ and $\{\cdot,\cdot\}$ from the formal development \cn{ZFset}, but not
their axioms. Instead the symbols are ``defined'' by alluding to the literature (common
knowledge). We claim this verbalization effectively postulates the existence of $v$, by
implying that the semantics of the two symbols is compatible with that given in the
literature (which we represent as a realm).
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{SET}};
\node[thy] (pcont) at (-3,2) {\cn{SETOPS}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {\cn{ZFset}};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[pinclude,red] (citp) to (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\caption{Publication graph for generalization/unspecified recaps (Example \ref{ex:course})}\label{fig:rec-slides}
Actually, the very paper you are reading can also serve as an example of adoption; it
recaps the notion of a realm from~\cite{CarFarKoh:rsckmt14} in \ref{sec:prel-realms}
above, but instead of giving a formal definition, it only gives a suggestive diagram and
names its parts, leaving the details to be imagined -- or looked up -- by the
reader.\ednote{MK@MI, I think the remark fits best here.}
\begin{oldpart}{from the equivalence example}
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
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}
\begin{oldpart}{this cannot be understood here}
In informal mathematics $v$ is usually not explicitly given, but it may or may not be
justified. In case it is not we call $v$ a \emph{postulated} view. The relation $r$ is
between the recap and the cited paper is left unspecified at this point as we
distinguish several cases below.
\end{oldpart}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:
% LocalWords: pheno emph prel-realms CarFarKoh rsckmt14 ldots wrapfigure vspace xscale
% LocalWords: tikzpicture ysep pn mathit cn rec-gen ednote oldpart pcont citp rc pl sp
% LocalWords: ge rec-covers textbf tcdots1 cdots circ mnets textsf multinets prel atm
% LocalWords: rec-mnets-aggr CalStai natm09 rec-atm lq ATMhalt citpex cdot cdot ZFset
% LocalWords: pinclude rec-slides agg-covers