adoptions almost there

adoptions/intro.tex

@@ -17,7 +17,7 @@ assembled into libraries (physical and virtual ones), which give researchers and
 practitioners access to the scientific document commons -- modulo physical distribution
 methods like inter-library loan and access right restrictions like membership or
 commercial constraints. Documents are even classified into a domain-based classification
-schemes like the the Math Subject Classification (MSC), and disseminated in information
+schemes like the Math Subject Classification (MSC), and disseminated in information
 systems like Math Reviews and Zentralblatt Math.
 
 Today's mathematical documents have a specific conventionalized structure and metadata
@@ -67,7 +67,7 @@ surprisingly, such a model does not exist, even though knowledge dissemination a
 next-generation publication systems are a the heart of MKM and DML.
 
 In this paper we propose a content-oriented model for knowledge dissemination and its
-aggregation into a communal, shared knowledge commons. As we make of our previous
+aggregation into a communal, shared knowledge commons. As we make use of our previous
 development of the \emph{flexiformal} -- i.e. supporting flexible degrees of
 formality~\cite{Kohlhase:tffm13} -- OMDoc format~\cite{Kohlhase:OMDoc1.2}, which can
 represent formal and informal mathematical documents and developments, we think of this as

adoptions/paper.tex

@@ -45,14 +45,14 @@
   In the traditional knowledge dissemination process in mathematics and sciences, authors
   write semi-selfcontained articles which are then published in journals, conference
   proceedings, preprint archives, and/or given as talks. Other scientists read these,
-  extract the new knowledge, integrate this into their personal mental model of the field,
+  extract the new knowledge, integrate it into their personal mental model of the field,
   and use this as the basis for creating new knowledge which is disseminated in the same
   form.
 
   Somewhat surprisingly, this process has not been modeled from a formal or
   content-based perspective even though it is at the heart of human MKM and DML. 
 
-  In this paper we tackle this problem starting from the practice of starting papers with
+  In this paper we tackle this problem starting from the practice of beginning papers with
   a ``recap'', which briefly introduces context, terminology, and notations and thus ties
   the paper into the knowledge commons. We propose a flexiformal model for knowledge
   dissemination and its aggregation into a communal, shared knowledge commons based on

adoptions/patterns.tex

@@ -29,23 +29,19 @@ perspective, informal mathematical papers refer (and contribute to) realms rathe
 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}
-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
+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}.
 
-% \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}
+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{6.3cm}\vspace*{-2em}
  \begin{tikzpicture}[xscale=.7]
@@ -101,8 +97,7 @@ theories in a pillar are conservative extensions of a bottom theory (denoted wit
 $\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.
+the face and each pillar.  
 
 \subsection{Realms as a Model for Dissemination \& Aggregation} 
 
@@ -175,28 +170,26 @@ on others from the same realm for results, context, and support.
  \caption{General Case for Recaps}\label{fig:rec-gen}
 \end{figure}
 
-
-
 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
+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 \emph{generalization
+  recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and, in the informal case, \emph{postulated
   recap} (\ref{rc:ge}).
 
 
-\subsection{Special case: Plain/Simple Recaps}\label{rc:pl}
+\subsection{Special case: Plain 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
+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
 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.
+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{figure}[ht]\centering
  \begin{tikzpicture}
@@ -285,7 +278,6 @@ realm's literature.  It also makes $v$ exist as induced by $v_1$ modulo conserva
   \draw[conservative] (tcdots1) to (top1);
   \draw[conservative] (pcont) to (top1);
   
-  
   \draw[conservative] (bot2) to (top2);
   \draw[view, bend left = 10] (bot2) to (bot1);
   \draw[view, bend left = 10] (bot1) to (bot2);
@@ -293,6 +285,9 @@ realm's literature.  It also makes $v$ exist as induced by $v_1$ modulo conserva
  \caption{Aggregation graph for plain recaps (Example \ref{ex:covers})}\label{fig:agg-covers}
 \end{figure}
 
+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
@@ -301,7 +296,7 @@ and the cited paper that ensure their isomorphism. Then, the view $v$ is induced
 $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
+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.
@@ -357,10 +352,9 @@ sample papers we studied.
  \caption{Publication graph for equivalence recaps (Example \ref{ex:mnets})}\label{fig:rec-mnets}
 \end{figure}
 
-
 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
+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
@@ -424,21 +418,21 @@ to reduce them to the $\bot$ theory.
 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.
+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
+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}
+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.
 
 \begin{figure}[ht]\centering
  \begin{tikzpicture}
@@ -499,11 +493,16 @@ precisely but there are some interesting things there, we should talk about it}
 
 \subsection{Postulated Recap/Adoption}\label{rc:ge}
 
-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}.
+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$ 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 case in example \ref{ex:course} where the recap theory \cn{SET} includes only
+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
@@ -543,7 +542,7 @@ literature (which we represent as a realm).
   \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[adoption,red] (citp) to node[above] {$\cn{r}$} (recap);
   
   
   \draw[conservative] (recap) to (pcont);
@@ -557,29 +556,31 @@ literature (which we represent as a realm).
  \end{tikzpicture}
  \caption{Publication graph for generalization/unspecified recaps (Example \ref{ex:course})}\label{fig:rec-slides}
 \end{figure}
-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}
-
 
+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}
 
 %%% Local Variables:
 %%% mode: latex

adoptions/phenomena.tex

 With \textbf{dissemination} we mean the process of assembling a mathematical document for
-the purpose of publication. We use the term \textbf{aggregation} for the process of and
+the purpose of publication. We use the term \textbf{aggregation} for the process of an
 individual integrating the knowledge gained from reading or experiencing the respective
 document into their mental model of the domain. For now we will use these two concepts
 intuitively only, it is the purpose of this paper to propose a more rigorous model for
 them. As a first step, we will now have a closer look at the practices in formal and
 informal mathematics.
 
-\subsection{The Structure of informal Mathematical Documents}
+\subsection{The Structure of Informal Mathematical Documents}
 
 Mathematical documents traditionally have:
 \begin{compactenum}
@@ -187,7 +187,7 @@ notes, books, encyclopedias), where the slides often have telegraphic versions o
 statements, which verbalize more rigorous definition.
 
 This is illustrated in Example \ref{ex:course} which is inspired from the notes of a first
-year computer science course taught by the second author. The example is a simplified and
+year computer science course taught by the first author. The example is a simplified and
 self-contained version of the original which in itself is only one instance of a commonly
 occurring pattern in the course notes.
 
@@ -203,7 +203,7 @@ occurring pattern in the course notes.
   power set.
 \end{example}
 
-We observe that course notes in example \ref{ex:course} are self-contained in the sense
+We observe that course notes in Example \ref{ex:course} are self-contained in the sense
 that they can be understood without knowing about the formal development. This
 self-containedness is important intra-course didactics.  But it also has the problem that
 the courses become insular; how are students going to communicate with mathematicians who