Newer
Older
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 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}
Mathematical documents traditionally have:
\begin{compactenum}
\item\label{md:metadata} A \defemph{front/backmatter} and \defemph{page margins}, which
identify the scientific metadata:
\begin{inparaenum}[\em i\rm)]
\item author's names, affiliations, and addresses,
\item publication venue, date, and fragment identifiers (e.g. page numbers),
\item classification data, e.g. keywords or MSC codes,
\item acknowledgements of contributions of other researchers or funding agencies.
\item access conditions, e.g. copyright, confidentiality designations, or licenses.
\end{inparaenum}
\item\label{md:abstract} An \defemph{abstract} that gives an executive overview over the
document.
\item\label{md:intro} An \defemph{introduction} that leads the reader into the topic,
discusses the problems solved in the document and their relation to the ``real world'',
and generally argues that reading the paper is worth the reader's attention.
\item\label{md:preview} A \defemph{preview}, which outlines the structure of, the
contributions in, and methods used in the document.
\item\label{md:soa} A discussion of the \defemph{state of the art} on the topic of
document.
\item\label{md:cg} The establishment of a \defemph{common ground} between the reader and
the author, which
\begin{inparaenum}[\em i\rm)]
\item recapitulates or surveys concepts and results from the documents/knowledge commons
to make the document self-contained (for its intended audience)
\item identifies any assumptions and gives the ensuing contributions a sound
terminological basis.
\item\label{md:contri} The \defemph{contributions} part, which contains the development of
new knowledge in form of e.g. new insights, new interpretations of known concepts, new
theorems, new proofs, new applications/examples or new techniques of achieving results.
\item\label{md:eval} An \defemph{evaluation} of the contributions in terms of
\item\label{md:relwork} A discussion of \defemph{related work} which reviews the
contributions and their relation to existing approaches and results from the literature.
\item\label{md:concl} A \defemph{conclusion} which summarizes the contribution with the
benefit of hindsight and relates it to the claims made in the introduction.
\item\label{md:aux} Literature references, an index, a glossary, etc. and possibly
appendices that contain material deemed supplementary to the contributions.
\end{compactenum}
Even though the form or order of the structural elements may vary over publication venues,
and certain elements may be implicit or even missing altogether, the overall structure is
It may be surprising that only one in eleven parts of a mathematical document -- the
``contributions'' -- arguably the largest -- is fully dedicated to transporting the
payload of the paper. All other contribute to either the
dissemination\footnote{\ref{md:metadata}. for referencing, \ref{md:abstract}. for
determining interest}, understanding\footnote{\ref{md:intro}. and \ref{md:concl}. for
broader context, \ref{md:soa}. and \ref{md:relwork}. for problem context,
\ref{md:preview}. for document navigation, \ref{md:eval}. for assessment of value, and
\ref{md:aux}. for further reading} and aggregation processes. We will see that the
latter is mainly driven by the common ground (point \ref{md:cg}. above), which we will
\subsection{Common Ground/Recapitulation in Mathematical Research}\label{sec:cg-preprints}
To get an overview over recaps in the literature, we randomly selected 30 papers from the
new submissions to \url{http://arxiv.org/archive/math} and analyzed their structure. All
had a significant common ground section that recapitulates the central notions and fixes
notations. We show two examples where the mathematics involved is relatively elementary.
\begin{example}\label{ex:covers}
\cite{covers-orig} discusses covers of the multiplicative group of an algebraically
closed field which are formally introduced in the beginning of the paper as follows:
\begin{labeledquote}\sf
\textbf{Definition 1.1} Let $V$ be a vector space over $Q$ and let $F$ be an
algebraically closed field of characteristic $0$. A \emph{cover of the multiplicative
group} of $F$ is a structure represented by an exact sequence
$0 \arr K \arr V \arr F^∗ \arr 1$ , where the map $V \arr F^*$ is a surjective group
homomorphism from $(V, +)$ onto $(F^∗, \cdot)$ with kernel $K$. We will call this map
\emph{exp}.
However, later, the authors source the concept origin to an earlier paper (``\textsf[13]'') and effectively import the terminology,
definitions and theorems. For instance, when establishing results, \cite{covers-orig} mentions
``\textsf{Moreover, with an additional axiom (in $L_{\omega_1\omega}$) stating $K \cong Z$, the
class is categorical in uncountable cardinalities. This was originally proved in [13] but an error was later
found in the proof and corrected in [2]. Throughout this article, we will make the assumption $K \cong Z$.}''.
% However, \cite{covers-orig} uses a
% generalization of the concept in \cite{covers-13} which uses the sequence
% $0 \arr Z \arr C \arr C^* \arr 1$ instead (although later proves some
% generalizations). Moreover, \cite{covers-2} also extends the result in \cite{covers-13}
% and additionally fixes a hole in the proof mentioned above.
In the second example, the situation is a bit more complex, since the import of the
terminology and definitions is not direct, but involves a choice.
\begin{example}\label{ex:mnets} \cite{mnets-orig} studies the properties of multinets. In
the preliminaries section they are introduced with the following definition:
\begin{labeledquote}\sf \textbf{Definition 2.1} The union of all completely reducible
fibers (with a fixed partition into fibers, also called blocks) of a Ceva pencil of degree
$d$ is called a $(k, d)-\mathit{multinet}$ where $k$ is the number of the blocks. The base
$X$ of the pencil is determined by the multinet structure and called the base of the
multinet.
\end{labeledquote} Later in that section some properties of multinets are introduced
with the phrase ``\textsf{Several important properties of multinets are listed below which
have been collected from [4,10,12].}''. The referenced papers all use slightly different
definitions of multinets but they are assumed to be equivalent so that the properties
hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made explicit --
although not proved -- from the start: ``\textsf{There are several equivalent ways to
define multinets. Here we present them using pencils of plane curves.}''
The next example is not from our 30 examples, since we want to show an even more complex
\cite{CalStai:natm09} studies the halting problem for accelerated Turing machines and
starts off the discussion with an informal introduction of the topic.
An accelerated Turing machine (sometimes called Zeno machine) is a Turing machine that
takes $2^{-n}$ units of time (say seconds) to perform its $n$\textsuperscript{th} step;
we assume that steps are in some sense identical except for the time taken for their
execution.
\end{labeledquote}
This is a telegraphic version of the full definition, which is given in the literature.
Actually ~\cite {CalStai:natm09} continues with an overview of the literature, citing no
less than 12 papers, which address the topic of accelerated Turing machines. One of these
supposedly contains the formal definition, which involves generalizing Turing machines to
timed ones, introducing computational time structures, and singling out accelerating ones,
e.g. using (\ref{lq:atm-formal}).
\textbf{Definition 1.3}: An \textbf{accelerated Turing machine} is a \underline{Turing
machine} $M=\langle X,\Gamma,S,s_o,\Box,\delta\rangle$ working with with a
\underline{computational time structure} $T= \tup{\{t_i\}_i,<,+}$ with
$T\subseteq\mathbb{Q_{+}}$ ($\mathbb{Q_{+}}$ is the set of non-negative rationals) such
that $\sum_{i\in \mathbb{N}} t_i <\infty$.
\end{labeledquote}
Note that the definition of an ATM~\cite{CalStai:natm09} is an instance of definition 1.3,
which allows arbitrary time structures.
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
% 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}
% \item either we find the ``real definition'' from the literature and use this as the
% ``origin'' or
% \item we consider the introductory sentence in the recap (e.g. \ref{lq:atm} for ATMs in
% example \ref{ex:atm}) as a definition and use this as the ``origin''.
% \end{compactenum}
% 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: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 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 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.}
\subsection{Secondary Literature: Education/Survey}\label{sec:survey}
A similar effect can be observed with educational materials or survey articles, whose
concern is not to make an original contribution to the knowledge commons, but to prepare a
document that helps an individual or group study or better understand a body of already
established knowledge. Consider for instance, slides and background materials (lecture
notes, text books, encyclopaedias), where the slides often have telegraphic versions of
the real 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 first author. The example is a simplified and
self-contained version of the original which in itself is only one instance of a commonly
\begin{example}[A Course grounded in a Formal Library]\label{ex:course}
A course which introduces (naive) set theory informally, but grounds itself in a formal,
modular definition. In the cited source, we have a careful introduction in the form of
a modular theory graph starting at a theory that introduces membership relation and the
axioms of existence, extensionality, and separation and defines the set constructor
$\{\cdot |\cdot\}$ from these axioms. In the course notes we have a theory that
``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ but not the associated axioms.
Instead it ``defines'' them by alluding to the intuitions of the students. Then the
course notes continue with introducing set operations ranging from set union to the
power set.
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
have learned their maths from other courses? This is where alluding to the literature
comes in, by connecting the course notes with it.
\begin{example}\label{ex:rudin}
The situation in mathematical textbooks is similar in structure to that in research
papers --perhaps more pronounced. Consider the following passage from Rudin's classical
introductory textbook to Functional Analysis~\cite[p. 6f]{Rudin:fa73}.
\textbf{1.5 Topological spaces} A \emph{topological space} is a set $S$ in which a
collection $\tau$ of subsets (called \emph{open sets}) has been specified, with the
following properties: $S$ is open, $\emptyset$ is open, [\ldots] Such a collection is
called a \emph{topology} on $S$. [\ldots]
\end{labeledquote}
This is continued later -- vector spaces have been recapped earlier in section 1.4 --
with:
\textbf{1.6 Topological vector spaces} Suppose $\tau$ is a topology on a vector space $X$
such that
\begin{compactenum}[(a)]
\item \emph{every point of $X$ is a closed set, and}
\item \emph{the vector space operations are continuous with respect to $\tau$}
\end{compactenum}
Under these conditions, $\tau$ is said to be a \emph{vector topology} on $X$, and $X$ is a
\emph{topological vector space}.
\end{labeledquote}
Note that Rudin does not directly cite the literature in these quotes, but in the preface
he mentions the vast literature on function analysis and in Appendix B he cites the
original literature for each chapter. The situation in textbooks is also different from
research articles in that textbooks -- like survey articles, and by their very nature --
do not add new knowledge or new results, but aggregate and organize the already published
ones, possibly reformulating them for a more uniform exposition. But still, one can
distinguish recap parts -- as the ones above -- which are much more telegraphic in nature
from the primary material presented in the textbook.
Where applicable, common ground in formal mathematics is typically established via direct
imports of symbols, theorems, notations, etc. Formal documents emphasize correctness and
do not focus on human readability so they do not re-introduce concepts or provide,
verbalizations of definitions.
For instance, In Isabelle and Coq knowledge is organized in \emph{Theories} and
\emph{Modules} which are effectively named sets of declarations. The incremental
development process is enabled via the \textsc{imports} and, respectively, \textsc{Require
Import} statements that effectively opens a library module by name and enables its
declarations to be used in the current development.
In Mizar, formal documents (called \emph{articles}) can be exported as PDF files in a
human readable format. The narrative documents contain a part that verbalizes the imports
from the source documents and the notation reservations which can be seen as a common
ground section.
\begin{example}\label{ex:mizar}
The common ground part for~\cite{RicKor:fgs13}
\begin{labeledquote}\sf
The notation and terminology used in this paper have been introduced in the
following papers: [4], [11], [12], [19], [9], [3], [5], [6], [21], [22], [1], [2], [7], [18],
[20], [24], [25], [23], [16], [13], [14], [10], [15], and [8].
In this paper $T$ , $U$ are non empty topological spaces, $t$ is a point of $T$ , and
$n$ is a natural number.
\end{labeledquote}
\end{example}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:
% LocalWords: textbf compactenum md defemph backmatter defemph inparaenum soa contri lq
% LocalWords: relwork concl atm covers-orig labeledquote emph arr arr arr arr arr cdot
% LocalWords: exp textsf cong mnets mnets-orig multinets Ceva mathit multinet ednote th
% LocalWords: CalStai natm09 textsuperscript langle rangle subseteq mathbb infty textsc
% LocalWords: self-containedness textsc geq topalg ldots RicKor fgs13 summarizes Rudin
% LocalWords: analyze analyzed generalization generalizations generalizing Rudin's
% LocalWords: flexiformalized verbalization verbalizations emptyset extensionality
% LocalWords: emphasize organized Mizar newpart topvs