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}
Intuitively, a realm \cite{CarFarKoh:rsckmt14} is a theory structure in a theory graph $G$ (i.e. a subgraph of $G$) that abstracts from the development
and provides practitioners with the useful symbols and theorems via an \emph{interface theory}.
We briefly introduce realms and the background concepts below and refer to \cite{CarFarKoh:rsckmt14} for details.
First, in the following, \emph{theories} are named sets of declarations (i.e. symbols, axioms or theorems). Additionally,
\emph{theory morphisms} (or \emph{views}) are truth-preserving mappings from a source theory to a target theory and formalize inheritance and applicability of theorems.
Theories can access and use declarations from other theories by importing them, either directly (\emph{plain includes}), or via a translation (\emph{structures}).
An important concept for realms is that of a \emph{conservative extension} which usually occurs when a theory includes another and contains only
theorems and derived symbols (i.e. adds no axioms or primitive symbols). An essential property of conservative extensions is that if $S'$ is a conservative extension
of $S$ then there is view $v$ between $T$ and $S$ iff there is a view between $T$ and $S'$ in the same direction. In fact, we will often talk about views \emph{modulo conservativity}
below.
\begin{wrapfigure}r{5.3cm}\vspace*{-2em}
\begin{tikzpicture}[xscale=.6]
%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.1,2.6) {$\mathit{Realm}$};
\node (p1-name) at (0.4,1.6) {$\mathit{Pillar_1}$};
% \node (p2-name) at (3,1.6) {$\mathit{Pillar_{\ldots}}$};
\node (p3-name) at (6.6,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}
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
\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 first restrict ourselves to the case where there is a single recap for
simplicity and expositional clarity. This already covers
the majority of research papers we have analyzed; they mainly build on one 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
\begin{tikzpicture}[xscale=.7]
\node (r-name) at (2,-2.1) {$\mathit{Realm}$};
\node (p-name) at (-3,-0.6) {$\mathit{Paper}$};
\node (p1-name) at (0.5,-1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (3.5,-1.6) {$\mathit{Pillar_n}$};
\node[thy] (pcont) at (-3,2) {Contrib.};
\node[thy] (citp) at (0.5,0) {CPaper};
\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 (single) 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 and 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, in the informal case, \emph{postulated
recap} (\ref{rc:ge}).
Finally, we have the case where the paper builds on several others and, therefore, has \emph{multiple recaps} (\ref{rc:mr}).
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 (\textsf{CPaper}),
but gives a concise verbalization of its definition. This allows it to make use of 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 which justifies the new paper becoming part of the
realm's literature (see Figure \ref{fig:agg-covers}). It also makes $v$ exist as induced
by $v_1$ modulo conservativity.
\begin{center}
\begin{subfigure}[b]{0.5\textwidth}
\begin{center}
\begin{tikzpicture}[xscale=.8]
\node (r-name) at (1.5,-2.0) {$\mathit{Realm}$};
\node (p-name) at (-2.4, -0.5) {$\mathit{Paper}$};
\node (p1-name) at (0.5,-1.5) {$\mathit{Pillar_1}$};
\node (p2-name) at (2.75,-1.5) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-2.4,0) {\cn{CACF}};
\node[thy] (pcont) at (-2.4,2) {\cn{MToCACF}};
\node[thy] (citp) at (0.5,0) {CPaper};
\node[thy] (top2) at (2.75,1) {$\top$};
\node[thy] (bot2) at (2.75,-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}\label{fig:rec-covers}
\end{center}
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.45\textwidth}
\begin{center}
\begin{tikzpicture}[xscale=.8]
\node (r-name) at (0.7,-4.0) {$\mathit{Realm}$};
\node (p1-name) at (-0.5,-3.5) {$\mathit{Pillar_1}$};
\node (p2-name) at (2.75,-3.5) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-1.3,-1) {\cn{CACF}};
\node[thy] (pcont) at (-1.3,0) {\cn{MToCACF}};
\node[thy] (citp) at (-0.5,-2) {CPaper};
\node[thy] (top2) at (2.75,1) {$\top$};
\node[thy] (bot2) at (2.75,-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}\label{fig:agg-covers}
\end{center}
\end{subfigure}
\caption{Plain Recaps (Example \ref{ex:covers})}
\end{center}
Plain recaps can also model the formal examples (e.g. Example \ref{ex:mizar}) but in that
situation it is not too interesting as we have the degenerate case for the realm itself.
\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.
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.
\begin{center}
\begin{subfigure}[b]{0.45\textwidth}
\begin{center}
\begin{tikzpicture}[xscale=.8]
\node (r-name) at (1.5,-2.1) {$\mathit{Realm}$};
\node (p-name) at (-2.5,-0.6) {$\mathit{Paper}$};
\node (p1-name) at (0.5,-1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (2.75,-1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-2.5,0) {\cn{MNets}};
\node[thy] (pcont) at (-2.5,2) {\cn{ICMnets}};
\node[thy] (citp) at (0.5,0) {CPaper};
\node[thy] (top2) at (2.75,1) {$\top$};
\node[thy] (bot2) at (2.75,-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}\label{fig:rec-mnets}
\end{center}
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.45\textwidth}
\begin{center}
\begin{tikzpicture}[xscale=.8]
\node (r-name) at (0.25,-2.1) {$\mathit{Realm}$};
\node (p3-name) at (-2.0,-1.6) {$\mathit{Pillar_{n+1}}$};
\node (p1-name) at (0.5,-1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (2.75,-1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-2.0,-1) {\cn{MNets}};
\node[thy] (pcont) at (-2.0,1) {\cn{ICMnets}};
\node[thy] (citp) at (0.5,0) {CPaper};
\node[thy] (top2) at (2.75,1) {$\top$};
\node[thy] (bot2) at (2.75,-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}\label{fig:rec-mnets-aggr}
\end{center}
\end{subfigure}
\caption{Equivalence Recaps (Example \ref{ex:mnets})}
\end{center}
\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 results of the paper back to the (same) realm as they concern
only 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 can form a
realm of its own, namely the realm of accelerated Turing machines with step size $2^n$. Then
we can talk about aggregation with that realm (via the view $\cn{v_{to}}$) but we omit that here
for simplicity -- the aggregation is similar as for equivalence recaps, except with the specialization
realm.
\node (r-name) at (2,-2.1) {$\mathit{Realm_1}$};
\node (r2-name) at (-2.5,-1.6) {$\mathit{Realm_2}$};
\node (p-name) at (-5.2,-0.6) {$\mathit{Paper}$};
\node (p1-name) at (0.5,-1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (3.5,-1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-5.2,0) {\cn{ATM}};
\node[thy] (pcont) at (-5.2,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 for educational material such as the one in Example \ref{ex:course} where $r$ cannot be directly modeled
as either an include or a view. This is caused by the constraint of self-containedness of such materials. Normally,
in the case where a more formal development is used we could represent it as an include and be in the case for plain recaps.
However, the home theory of the new symbols must be the current development in order for it to be self-contained, so we cannot use an include.
Instead we envision a special kind of import that \emph{adopts} the included symbols effectively changing their home theory to the current one.
But, then the view $v$ is not justified so we must also assert its existence.
In that case we call $v$ a \emph{postulated} view and the the relation $r$ is an \emph{adoption} (see Figure \ref{fig:rec-slides}).
We leave working out the precise details of postulated views and adoptions in flexiformal theory graphs for future work.
This is the situation 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 (r-name) at (2,-2.1) {$\mathit{Realm}$};
\node (p-name) at (-3,-0.6) {$\mathit{Paper}$};
\node (p1-name) at (0.5,-1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (3.5,-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[adoption,red] (citp) to node[above] {$\cn{r}$} (recap);
\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}
Note that we omit the aggregation part for this case as the purpose of such educational or
survey material is typically to provide a concise overview of a realm rather than to
contribute to it.
% 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}
Up to now we have only treated cases with single recaps to ease the exposition. But papers
and especially textbooks often recap from different realms and base the rest of the
exposition on them.
% The approach can be extended to multiple recaps from
% the same realm with minimal effort -- but the diagrams become messy. We discuss multiple recaps from different realms
% in Section \ref{rc:mr}.
\begin{figure}[ht]
\begin{center}
\begin{subfigure}[b]{0.45\textwidth}
\begin{center}
\draw[pillar] (-.5,-.8) rectangle (1.5,1.3);
\node at (0.5,-.6) {\it Paper};
\node[thy] (r1) at (0,0) {$R_1$};
\node[thy] (r2) at (1,0) {$R_2$};
\draw[conservative] (r1) to (c);
\draw[conservative] (r2) to (c);
\draw[realm] (-2.1,-.8) rectangle (-0.9,0.3);
\draw[realm] (1.9,-0.8) rectangle (3.1,0.3);
\node (r1-name) at (-1.5,-0.6) {$\mathit{Realm_1}$};
\node (r2-name) at (2.5,-0.6) {$\mathit{Realm_2}$};
\node[thy] (f1) at (-1.5,0.0) {$\mathrm{Face_1}$};
\node[thy] (f2) at (2.5,0.0) {$\mathrm{Face_2}$};
\draw[struct] (f1) -- node[below]{$v_1$} (r1);
\draw[struct] (f2) -- node[below]{$v_2$} (r2);
\draw[realm] (-.5,0.2) rectangle (1.5,3.3);
\node at (0.5,.4) {\it Union Realm};
\node[thy] (t) at (.5,1.0) {$R_1\cup R_2$};
\node[thy] (c) at (.5,2.0) {Contrib.};
\node[thy] (fu) at (.5,3.0) {$\mathrm{Face_\textit{u}}$};
\draw[struct] (fu) -- node[left]{$v$} (c);
\draw[realm] (-2.1,0.2) rectangle (-0.9,1.3);
\draw[realm] (1.9,0.2) rectangle (3.1,1.3);
\node (r1-name) at (-1.5,0.4) {$\mathit{Realm_1}$};
\node (r2-name) at (2.5,0.4) {$\mathit{Realm_2}$};
\node[thy] (f1) at (-1.5,1.0) {$\mathrm{Face_1}$};
\node[thy] (f2) at (2.5,1.0) {$\mathrm{Face_2}$};
\draw[struct] (f1) -- node[below]{$v_1$} (t);
\draw[struct] (f2) -- node[below]{$v_2$} (t);
\end{center}
\end{subfigure}
\caption{Multiple Recaps (Example \ref{ex:rudin})}\label{fig:multiple}
\end{center}
This is the situation in Figure~\ref{fig:multiple-publ} inspired by Example \ref{ex:rudin} from Rudin's book.
Note that the two recaps import directly from the faces rather than from a specific pillar or paper.
This is intended and covers the typical case of recaps in textbooks and survey articles. For instance, as mentioned
in Section \ref{sec:survey}, Rudin does not directly cite literature in the recaps, but aggregates the vast
literature in an appendix.
For the aggregation phase the multiple recaps situation begs the question of where the contribution should be placed.
In the recap in example \ref{ex:rudin} we have separate recaps of vector
spaces and topological spaces (\ref{q:topspace}), and we analyze them as theory morphisms
from their respective realms. In this case, there is the realm of topological vector
spaces (\ref{q:topvs}) which imports from both realms, this is the natural place for the
contributions. In the case such a realm does not exist yet, the paper can be used as the
natural starting point for (first pillar of) the realm. Actually, the ``union realm''
concept in Figure~\ref{fig:multiple-aggr} is a bit simplified. The contribution of the paper
will usually add some conditions -- like conditions (a) and (b) in (\ref{q:topvs}) -- and
use that for the base theories of the realms. This does not invalidate our claim that
there is always a natural realm -- which may have to be created -- for the contribution of
the ``paper''.
%%% 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 itemize conservativity analyzed centering
% LocalWords: CPaper recognize specialization verbalization mizar rec-mnets flexiformal
% LocalWords: self-containedness generalization newpart qquad Rudin's analyze topvs