Skip to content
Snippets Groups Projects
Commit 8fff38e7 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

more

parent d1ba2627
No related branches found
No related tags found
No related merge requests found
......@@ -30,3 +30,6 @@ applicable.
%%% mode: latex
%%% TeX-master: "paper"
%%% End:
% LocalWords: omdoc2 KohRabSac fvip11 ednote leadsto oldpart bluenote KohKoh tfndc11
% LocalWords: tffm13 CarFarKoh tr13 todolist
......@@ -78,11 +78,10 @@ introduces context, terminology, and notations and thus ties the paper into the
commons as a starting point and model it based on OMDoc/MMT theory graphs and the newly
introduced realms \cite{CarFarKoh:rsckmt14}.
In Section~\ref{sec:prel} we lay the foundations by briefly review the structure of
mathematical documents, introduce OMDoc theory graphs and realms. Then, we build our
intuitions about ``recaps'' by looking at some examples in Section \ref{sec:pheno}. We
discuss how to represent them using theory graphs in section
\ref{sec:patterns}. Section~\ref{sec:conc} concludes the paper and discusses future work.
In Section~\ref{sec:pheno} we briefly review the structure of mathematical documents and
build our intuitions about ``recaps'' by looking at some examples. We discuss how to
represent them using theory graphs in section \ref{sec:patterns}. Section~\ref{sec:conc}
concludes the paper and discusses future work.
......@@ -93,4 +92,4 @@ discuss how to represent them using theory graphs in section
% LocalWords: colleages ednote emph prel pheno conc oldpart bluenote KohKoh tfndc11
% LocalWords: tffm13 CarFarKoh tr13 compactenum defemph backmatter defemph inparaenum
% LocalWords: Libary IIAGFFHRPD RabKoh ldots
% LocalWords: Libary IIAGFFHRPD RabKoh ldots rsckmt14
......@@ -96,3 +96,12 @@ pages={477-505},
language={English}
}
@article{RicKor:fgs13,
title={Fundamental Group of $n$-sphere for $n\geq2$},
author = {Marco Riccardi and Artur Kornilowicz},
journal = {Formalized Mathematics},
volume = {20},
number={2},
pages ={97–-104},
doi= {10.2478/v10037-012-0013-1},
year = {2013}}
......@@ -64,3 +64,7 @@ literature) the paper continues with its contribution.
%%% mode: latex
%%% TeX-master: "paper"
%%% End:
% LocalWords: quant-orig labeledquote emph overline varphi mathbb arr mathbb mathrm leq
% LocalWords: inf forall quant-fs14 calculi-orig vee Linial textbf Axm textbf textbf
% LocalWords: Cmpl textbf newpart ednote
No preview for this file type
......@@ -99,4 +99,4 @@
%%% End:
% LocalWords: maketitle semi-selfcontained emph prel pheno conc printbibliography
% LocalWords: setcounter tocdepth tableofcontents newpage
% LocalWords: setcounter tocdepth tableofcontents newpage oldparts
......@@ -16,7 +16,7 @@ which the results of the paper are built. This leverages the literature in two w
due to its truth-preserving semantics.
\end{itemize}
Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads
to a theory of the main contxribution of the paper.
to a theory of the main contribution of the paper.
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
......@@ -103,18 +103,29 @@ pillars and the $n$ views $I_k$ capture the relation of interface-implementation
the face and each pillar. See \cite{CarFarKoh:rsckmt14} for the complete definition and
more examples.
\subsection{Realms in Informal Mathematics}
Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part of a theory graph (although simplified to one recap reference for the paper).
\ednote{what about multiple references}
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 main content of the paper is a theory in itself that includes the recap theory and is a conservative extension of it.
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 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.
Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part
of a theory graph (although simplified to one recap reference for the paper). \ednote{MI:
what about multiple references, MK: should be no problem; we need to add a footnote
here} 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$.
\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}
%Mathematical papers re-introduce concepts with the implied assumption of semantic equivalence in the context of the paper.
%I.e. every statement in the paper holds for the original definition too, but not necessarily the converse.
......@@ -173,18 +184,20 @@ We recognize four special cases for recaps based on the nature of $r$ and discus
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 \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 subcases depending on the relation between the recap and cited theory:
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:ge}).
\subsection{Special case: Plain/Simple 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 \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
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 \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.
\subsection{Special case: Plain/Simple 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 \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 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 \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.
\begin{figure}[ht]\centering
\begin{tikzpicture}
......@@ -278,7 +291,7 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:agg-covers}
\end{figure}
\subsection{Special Case: Equivalence Recap} \label{rc:eq} Another common situation is that
......@@ -355,13 +368,15 @@ sample papers we studied.
\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 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.
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{figure}[ht]\centering
\begin{tikzpicture}
......@@ -379,8 +394,6 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-2.5,-1) {\cn{MNets}};
\node[thy] (pcont) at (-2.5,1) {\cn{ICMnets}};
......@@ -418,17 +431,21 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\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 paper results back to the (same) realm as they concern 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 \ref{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}
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.
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 \ref{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}
......@@ -554,3 +571,9 @@ given in the literature (which we represent as a realm).
%%% 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
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
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 A \defemph{front/backmatter} and \defemph{page margins}, which identify the
scientific metadata:
\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),
......@@ -11,37 +19,50 @@ Mathematical documents traditionally have:
\item acknowledgements of contributions of other researchers or funding agencies.
\item access conditions, e.g. copyright, confidentiality designations, or licenses.
\end{inparaenum}
\item An \defemph{abstract} that gives an executive overview over the document.
\item 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 A \defemph{preview}, which outlines the structure of, the contributions in, and
methods used in the document.
\item A discussion of the \defemph{state of the art} on the topic of document.
\item The establishment of a \defemph{common ground} between the reader and the author,
which
\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 give the ensuing contributions a sound
terminological basis
\end{inparaenum}
\item 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 An \defemph{evaluation} of the contributions in terms of applicability or even
usability.
\item A discussion of \defemph{related work} which reviews the contributions and their
relation to existing approaches and results from the literature
\item A \defemph{conclusion} which summarizes the contribution with the benefit of
hindsight and relates it to the claims made in the introduction.
\item Literature references, an index, a glossary, etc. and possibly appendices that
contain material deemed supplementary to the contributions.
\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
applicability or even usability.
\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
surprisingly stable.
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
analyze in more detail next.
\subsection{Common Ground/Recapitulation in Papers}
A common pattern occurs in scientific papers which often have a preliminaries section to
......@@ -83,13 +104,11 @@ and additionally fixes a hole in the proof mentioned above.
\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 \cite{mnets-ref4, mnets-ref10, mnets-ref12}.}''\ednote{MK: we should
not have the real citations in our paper.} 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.}''
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.}''
\end{example}
\begin{example}\label{ex:atm}
......@@ -149,57 +168,59 @@ We discuss this in section \ref{sec:patterns} and look at how the examples above
\ednote{MK@MK: more, e.g. about the distinction of notations and
differing concepts.}
\subsection{Common Ground in Slides and Background Materials}
\subsection{Secondary Literature: Education/Survey}
\ednote{that is all recap (not really common ground)}
A similar situation obtain with slides and background materials (lecture notes, books,
encyclopedias), 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 occurring pattern in the course notes.
\ednote{MI@MK: maybe you can explain better, I added this since I thought it's important to have it grounded in a concrete
example here, rather than it appear as an imagined one}
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
occurring pattern in the course notes. \ednote{MI@MK: maybe you can explain better, I
added this since I thought it's important to have it grounded in a concrete example
here, rather than it appear as an imagined one}
\begin{example}[A Course grounded in a Formal Library]\label{ex:course}
Take for instance 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
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.
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.
\end{example}
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.
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.
\subsection{Common Ground in Formal Mathematics}
Where applicable, formal mathematical libraries are usually organized in modules representing lists of named declarations
Where applicable, formal mathematical libraries are usually organized in modules
representing lists of named declarations
Where applicable, common ground in formal mathematics is typical 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.
Where applicable, common ground in formal mathematics is typical 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 \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.
\paragraph{Mizar}
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. Example \ref{ex:mizar} shows the common ground part for the article on
``Fundamental Group of $n$-sphere for $n \geq 2$'' \cite{topalg_6}.
from the source documents and the notation reservations which can be seen as a common
ground section.
\begin{example}{http://www.degruyter.com/view/j/forma.2012.20.issue-2/v10037-012-0013-1/v10037-012-0013-1.xml} \label{ex:mizar}
\begin{labeledquote}
\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].
......@@ -215,3 +236,9 @@ $n$ is a natural number.
%%% 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment