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,
but gives a concise verbalization of its definition. This allows it to make use of the result in \cite{covers-2} which acts as a conservative
but gives a concise verbalization of its definition. This allows it to make use of the result in \cite{covers-2} which acts as a conservative
extension of \cite{covers-13}. The situation is shown in figure \ref{fig:rec-covers}
extension of \cite{covers-13}. The situation is shown in figure \ref{fig:rec-covers}
Note that, if $r$ is conservative, then we have a \emph{pillar extension} for the realm justifies the new paper becoming part of the realm's literature.
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.
It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\begin{figure}[ht]\centering
\begin{figure}[ht]\centering
...
@@ -159,7 +167,61 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
...
@@ -159,7 +167,61 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\caption{Covers example for Recaps}\label{fig:rec-covers}
\caption{Covers example for Recaps}\label{fig:rec-covers}
Another common situation is that of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the two theories.
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
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.
ensure their isomorphism. Then, the view $v$ is induced by $v_{from}\circ v_1$ modulo conservativity.
...
@@ -169,15 +231,12 @@ This occurs, for instance, in example \ref{ex:mnets} where this intuition is exp
...
@@ -169,15 +231,12 @@ This occurs, for instance, in example \ref{ex:mnets} where this intuition is exp
define multinets.'' (although not proved). Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category.
define multinets.'' (although not proved). Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category.
In fact it is the most common situation in the sample papers we studied.
In fact it is the most common situation in the sample papers we studied.
\begin{oldpart}
\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 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.
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.
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}
Note that adding an equivalent definition corresponds to a \emph{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}.
This corresponds to the mathematical practice of ``contributing to'' a field (or mathematical theory).
\begin{figure}[ht]\centering
\begin{figure}[ht]\centering
\begin{tikzpicture}
\begin{tikzpicture}
...
@@ -239,7 +298,79 @@ This corresponds to the mathematical practice of ``contributing to'' a field (or
...
@@ -239,7 +298,79 @@ This corresponds to the mathematical practice of ``contributing to'' a field (or
\caption{Multinets case for Recaps}\label{fig:rec-mnets}
\caption{Multinets case for Recaps}\label{fig:rec-mnets}
\end{figure}
\end{figure}
\paragraph{Special Case: Specialization Recap}
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}.
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.
