more

adoptions/intro.tex

@@ -19,7 +19,7 @@ In \ref{sec:prel} we briefly introduce OMDoc and theory graphs. Then, we build o
 We discuss how to represent them using theory graphs in section \ref{sec:patterns}. Finally, in section \ref{sec:conc} we discuss future work and conclude.
 
 
-\begin{oldpart}
+\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

adoptions/paper.tex

@@ -18,6 +18,7 @@
 
 \usepackage[hyperref=auto,style=alphabetic,citestyle=alphabetic,isbn=false,backend=bibtex]{biblatex}
 \addbibresource{local.bib}
+\addbibresource{kwarc.bib}
 \addbibresource{pub_rabe.bib}
 \addbibresource{systems.bib}
 \addbibresource{kwarcpubs.bib}
@@ -56,7 +57,6 @@ adequately represent content of flexible formality.
 \end{abstract}
 
 
-
 \section{Introduction}\label{sec:intro}
 \input{intro}
 
@@ -69,10 +69,10 @@ adequately represent content of flexible formality.
 \section{Theory Patterns in MMT/OMDoc Theory Graphs}\label{sec:patterns}
 \input{patterns}
 
-\section{Services/Authoring Workflows}
-\input{workflows}
+%\section{Services/Authoring Workflows}
+%\input{workflows}
 
-\section{Conclusion and Future Work}\label{sec:concl}
+\section{Conclusion and Future Work}\label{sec:conc}
 \input{conc}
 
 

adoptions/phenomena.tex

-\ednote{to discuss and categorize examples}
+\subsection{Recapitulation in Papers}
 
-\begin{oldpart}{Examples list}
-\begin{itemize}
-\item http://arxiv.org/pdf/1502.01212.pdf
-\item http://arxiv.org/pdf/1502.02591.pdf
-\item http://arxiv.org/pdf/1502.02308.pdf
-\item http://arxiv.org/pdf/1502.02413.pdf
-\end{itemize}
-\end{oldpart}
+A common pattern occurs in scientific papers which often have a preliminaries section to
+recapitulate the central notions and fix notations. In its simplest incarnation this can be seen
+as an import. However, in general, it can have a more complex behavior (e.g. see example \ref{ex:atm}).
 
 \begin{example}[http://arxiv.org/pdf/1502.00573.pdf] \label{ex:quant}
  \cite{quant-orig} discusses quantifier elimination in $C^*$-algebras and begins by defining the formulas for $C^*$-algebras after the 
@@ -34,7 +29,6 @@ definition is therefore said to be \emph{quantifier-free}.
  ``The definition above is slightly different from the one in \cite{quant-fs14} [...] 
  Since the two versions are equivalent, we have chosen an approach intended to minimize 
  the technical complexity of the definitions.''.
-
 \end{example}
 
 
@@ -100,14 +94,11 @@ hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made explicit
 define multinets. Here we present them using pencils of plane curves.'' 
 \end{example}
 
-
-
-
-\subsection{Recapitulation in Papers}
-
-A common pattern occurs in scientific papers which often have a preliminaries section to
-recapitulate the central notions and fix notations. In its simplest incarnation this can be seen
-as an import. However, in general, it can have a more complex behavior (e.g. see example \ref{ex:atm}).
+\begin{newpart}{@MI: look closer or try to find an example for this}
+\begin{example}{http://arxiv.org/pdf/1502.05657v1.pdf}
+\ednote{Possible realm merge}
+\end{example}
+\end{newpart}
 
 \begin{example}\label{ex:atm}
 For instance, \cite{CalStai:natm09} contains the sentence
@@ -141,10 +132,9 @@ this we have to disambiguate the concept of an accelerated Turing machine.
 on strawberry}
 \end{oldpart}
 
-In the example above the papers local definition of an ``accelerated Turing machine'' (ATM) 
-is slightly different from the one referenced in the literature.
-Specifically, it's a special case where the computation time structure is $2^{-n}$. 
-Therefore, treating it as an import is not adequate as the two concepts have clearly distinguishable semantics.
+In the examples above the papers local definition of a concept (e.g. of a ``Multinet'' or a ``accelerated Turing machine'' (ATM)) 
+is often slightly different from the one referenced in the literature.
+Therefore, treating it as an import is not always adequate as, sometimes, the two concepts have clearly distinguishable semantics.
 
 We have two choices for grounding a concept $c$ that occurs in recap :
 \begin{compactenum}
@@ -156,24 +146,24 @@ Which one is better depends on the situation.
 If the notion used in the paper is exactly the same as in the literature, we
 should probably choose 1. and just import the respective theory\footnote{Assuming that the
 paper in question has already been flexiformalized} so that we can reference it. In this case 
-the local ``definition'' (e.g. \ref{lq:atm} in example \ref{ex:ex:atm})of $c$ becomes a ``verbalization'' \ednote{introduce verbalizations in preliminaries}
+the local ``definition'' (e.g. \ref{lq:atm} in example \ref{ex:atm})of $c$ becomes a ``verbalization'' \ednote{introduce verbalizations in preliminaries}
 of the original definition in the literature. 
 
 The advantage of this choice is that the statements about $c$ made in the paper
 are directly compatible with any others that also reference this definition of $c$. This
 has enormous advantages for knowledge management and knowledge access.
 
-If the local notion is in any way different (such as in the ATM example above) than 
+If the local notion is in any way different (such as in the multinets or ATM examples above) than 
 the one in the literature (e.g. a generalization or a special case), we are forced into the second possibility. 
 However, while two concepts are different, they are still related -- after all, there was a reason to consider 
 the technical differences so small that they can be neglected. 
 Therefore, we should establish formally the relation between the two variants and their containing theories.
-We call this relation an \emph{adoption} as the local notion adopts (part of) its meaning from the literature.
-In section \ref{sec:repr} we discuss how adoptions can be represented in theory graphs using imports and theory morphisms. 
+We discuss this in section \ref{sec:patterns} and look at how the examples above can be represented in theory graphs using imports and theory morphisms.
 
 \ednote{MK@MK: more, e.g. about the distinction of notations and
   differing concepts.}
 
+\begin{oldpart}{from notes, didn't integrate this in yet}
 \subsection{Slides and Background Materials}
 
 A similar situation obtain with slides and background materials (lecture notes, books,
@@ -186,3 +176,4 @@ reference works, even if they are not the documents that initially introduce the
 in question. Textbooks and lecture notes are natural references as they are the places
 where students first encounter the concepts.  \ednote{MK: The solution for this is ADP and
   transclusion}
+\end{oldpart}
\ No newline at end of file

adoptions/prel.tex

-\ednote{to introduce basic OMDoc notions (docs, theories, declarations, verbalizations, notation definitions, URIs), realms}
\ No newline at end of file
+\subsection{OMDoc}
+\ednote{to introduce basic OMDoc notions (docs, theories, declarations, verbalizations, notation definitions, URIs)}
+
+\subsection{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{figure}[ht]\centering
+ \begin{tikzpicture}
+  %realm
+  \draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.8) rectangle (8,3.5) {};
+  %p1
+  \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-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.5,3.3) {$\mathit{Realm}$};
+  \node (p1-name)  at (0,1.6) {$\mathit{Pillar_1}$};
+  \node (p2-name)  at (3,1.6) {$\mathit{Pillar_{\ldots}}$};
+  \node (p3-name)  at (7.0,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,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 = 15] (bot2) to (bot1);
+  \draw[view, bend left = 15] (bot1) to (bot2);
+  \draw[view, bend left = 15] (bot2) to (bot3);
+  \draw[view, bend left = 15] (bot3) to (bot2);
+
+ \end{tikzpicture}
+ \caption{The architecture of a realm}\label{fig:realm}
+\end{figure}
\ No newline at end of file