Commit ce190872 authored by Dennis Müller's avatar Dennis Müller
Browse files

update

parents 8a62aa10 0e8cd520
......@@ -34,4 +34,13 @@ The theory discovery use case described in Sec. \ref{sec:usecase} is mostly desi
\end{itemize}
For some of these use cases it would be advantageous to look for views \emph{into} our working theory instead.
Note that even though the algorithm is in principle symmetric, some aspects often depend on the direction -- e.g. how we preprocess the theories, which constants we use as starting points or how we treat and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
\ No newline at end of file
Note that even though the algorithm is in principle symmetric, some aspects often depend on the direction -- e.g. how we preprocess the theories, which constants we use as starting points or how we treat and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: emph specialized generalization transfomations normalization prioritize
% LocalWords: sec:usecase
......@@ -147,4 +147,117 @@
booktitle = "Intelligent Computer Mathematics",
editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
publisher = "Springer"
}
\ No newline at end of file
}
@Article{imps,
author = "W. Farmer and J. Guttman and F. Thayer",
title = "{IMPS: An Interactive Mathematical Proof System}",
journal = "{Journal of Automated Reasoning}",
pages = "213--248",
volume = "11",
number = "2",
year = "1993",
}
@article{RK:mmt:10,
author = "F. Rabe and M. Kohlhase",
title = "{A Scalable Module System}",
year = "2013",
pages = "1--54",
journal = "Information and Computation",
volume = "230",
number = "1"
}
@book{omdoc,
author = "M. Kohlhase",
title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
series = "{Lecture Notes in Artificial Intelligence}",
number = "4180",
publisher = "Springer",
year = "2006",
}
@inproceedings{KMOR:pvs:17,
author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
year = "2017",
pages = "319--335",
booktitle = "Interactive Theorem Proving",
editor = "M. Ayala-Rincon and C. Munoz",
publisher = "Springer"
}
@inproceedings{KR:hollight:14,
author = "C. Kaliszyk and F. Rabe",
title = "{Towards Knowledge Management for HOL Light}",
year = "2014",
pages = "357--372",
booktitle = "Intelligent Computer Mathematics",
editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
author = {T. Gauthier and C. Kaliszyk},
title = "{Matching concepts across HOL libraries}",
booktitle = {Intelligent Computer Mathematics},
editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
pages = {267--281},
year = 2014,
publisher = {Springer}
}
@Article{lf,
author = "R. Harper and F. Honsell and G. Plotkin",
title = "{A framework for defining logics}",
journal = "{Journal of the Association for Computing Machinery}",
year = 1993,
volume = 40,
number = 1,
pages = "143--184",
}
@inproceedings{pvs,
AUTHOR = {S. Owre and J. Rushby and N. Shankar},
TITLE = "{PVS: A Prototype Verification System}",
BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}",
YEAR = {1992},
EDITOR = {D. Kapur},
PAGES = {748--752},
PUBLISHER = {Springer},
}
@MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS},
howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}}
@MISC{PVSlibraries:base,
title = {{NASA} {PVS} Library},
url = {http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}
@BOOK{Graf:ti96,
title = {Term Indexing},
publisher = {Springer Verlag},
year = {1996},
author = {Graf, Peter},
number = {1053},
series = {LNCS}}
@inproceedings{am:doceng10,crossref={DOCENG10},
author = {Serge Autexier and Normen M{\"u}ller},
title = {Semantics-based Change Impact Analysis for Heterogeneous Collections of Documents},
pages = {97--106},
numpages = {10},
url = {http://doi.acm.org/10.1145/1860559.1860580},
doi = {http://doi.acm.org/10.1145/1860559.1860580},
acmid = {1860580},
keywords = {change impact analysis, document collections, document management, graph rewriting, semantics},
pubs = {nmueller,omoc,omdoc}}
@mastersthesis{iancu:msc,
author = "Mihnea Iancu",
title = "{Management of Change in Declarative Languages}",
year = "2012",
school = "Jacobs University Bremen",
pubs={mscthesis}
}
@proceedings{DOCENG10,
editor = {Michael Gormish and Rolf Ingold},
title = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
booktitle = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
series = {DocEng '10},
year = {2010},
isbn = {978-1-4503-0231-9},
location = {Manchester, United Kingdom},
publisher = {ACM},
keywords = {conference},
address = {New York, NY, USA}}
\ No newline at end of file
We present a general MKM utility that given a \MMT theory and an \MMT library $\cL$ finds
partial and total views into $\cL$.
Such a view-finder can be used to drive various MKM applications ranging from theory classification to library merging and refactoring.
We have presented the first and last of these and show that they are feasible. For the applications discussed but unrealized in this paper, we mainly need to determine the right application context and user interface.
\paragraph{Future Work}
The current view-finder is already efficient enough for the limited libraries we used for testing.
To increase efficiency, we plan to explore term indexing techniques~\cite{Graf:ti96} that support $1:n$ and even $n:m$ matching and unification queries.
The latter will be important for the library refactoring and merging applications which look for all possible (partial and total) morphisms in one or between two libraries.
As such library-scale operations will have to be run together with theory flattening to a fixed point and re-run upon every addition to the library, it will be important to integrate them with the \MMT build system and change management processes~\cite{am:doceng10,iancu:msc}.
\paragraph{Acknowledgments}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Open Archive for Formalizations (KO 2428/13-1).
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: unrealized am:doceng10,iancu:msc Formalizations
......@@ -8,7 +8,7 @@ classification}.
The basic use case is the following: Jane, a mathematician, becomes interested in a class
of mathematical objects, say -- as a didactic example -- something she initially calls
``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
the following properties:
the following properties $Q$:
\begin{compactenum}
\item the empty set is beautiful over $\cB$
\item every subset of a beautiful set is beautiful over $\cB$
......@@ -16,56 +16,50 @@ the following properties:
there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
\end{compactenum}
To see what is known about beautiful sets, she types these three conditions into a theory
classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
$Q$ into a library $\cL$, and returns presentations of target theories and the assignments
made by the views.
% In our example we have the situation in Figure~\ref{fig:theory-classification-ex}.
classifier, which computes any theories in a library $\cL$ that match these (after a
suitable renaming). In our case, Jane learns that her ``beautiful sets'' correspond to
the well-known structure of matroids~\cite{wikipedia:matroid}, so she can directly apply
matroid theory to her problems.
In the base use case, Jane learns that her
``beautiful sets'' correspond to the well-known structure of
matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
problems.
In extended use cases, a theory classifier find theories that share significant structure
with $Q$, so that we can formalize $Q$ with modularly with minimal effort. Say Jane was
interested in ``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition,
then she could just contribute a theory that extends \textsf{matroid} by a formalization
of the fourth condition -- and maybe rethink the name.
% \item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
% information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
% form a generalization of the notion of linear independence from linear algebra.
% \end{compactitem}
%
% \begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
% \begin{tabular}{|p{5cm}|p{5cm}|}\hline
% $Q$ & Result \\\hline
% \begin{lstlisting}[mathescape]
% theory query : F?MitM
% include ?set
% Base : {A} set A
% beautiful {A} set A $\rightarrow$ prop
% empty : $\vdash$ beautiful $\emptyset$
% subset-closed: $\vdash$ {}
% \end{lstlisting}
% &
% \begin{lstlisting}[mathescape]
% theory matroid : F?MitM
% include ?baseset
% independent {A} set A $\rightarrow$
% empty: $\vdash$
% hereditary : $\vdash$
% augmentation: $\vdash$
% \end{lstlisting}
% \\\hline
% \end{tabular}
% \caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
% \end{figure}
\begin{newpart}{MK: this could/should be extended}
In extended use cases, we could
\begin{compactitem}
\item use partial views to find theories that share significant structure with $Q$, so
that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
could just contribute a theory that extends \textsf{matroid} by a formalization of the
fourth condition -- and maybe rethink the name.
\item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
form a generalization of the notion of linear independence from linear algebra.
\end{compactitem}
\end{newpart}
\begin{oldpart}{I would remove this completely -- the theories are given via screenshots later anyway}
\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
\begin{tabular}{|p{5cm}|p{5cm}|}\hline
$Q$ & Result \\\hline
\begin{lstlisting}[mathescape]
theory query : F?MitM
include ?set
Base : {A} set A
beautiful {A} set A $\rightarrow$ prop
empty : $\vdash$ beautiful $\emptyset$
subset-closed: $\vdash$ {}
\end{lstlisting}
&
\begin{lstlisting}[mathescape]
theory matroid : F?MitM
include ?baseset
independent {A} set A $\rightarrow$
empty: $\vdash$
hereditary : $\vdash$
augmentation: $\vdash$
\end{lstlisting}
\\\hline
\end{tabular}
\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
\end{figure}
\end{oldpart}
We reduce the theory classification problem to that of finding theory morphisms (views)
between \MMT theories. $\cL$: given a query theory $Q$, the viewfinder computes all
(total) views from $Q$ into a library $\cL$, and returns presentations of target theories
and the assignments made by the views.
\paragraph{Related Work}
Existing systems have so far only worked with explicitly given theory morphisms, e.g., in IMPS \cite{imps} or Isabelle \cite{isabelle}.
......@@ -85,11 +79,12 @@ Instead, of theory morphisms inside a single corpus, they use machine learning t
Their results can roughly be seen as a single partial morphism from one corpus to the other.
\paragraph{Approach and Contribution}
Our contribution is twofold.
Firstly, we present a the design and implementation of a generic theory morphism finder that works with arbitrary corpora represented in MMT.
The algorithm tries to match two symbols by unifying their types.
This is made efficient by separating the term into a hashed representation of its abstract syntax tree (which serves as a fast plausibility check for pre-selecting matching candidates) and the list of symbol occurrences in the term, into which the algorithm recurses.
Our contribution is twofold. Firstly, we present a the design and implementation of a
generic theory morphism finder that works with arbitrary corpora represented in MMT. The
algorithm tries to match two symbols by unifying their types. This is made efficient by
separating the term into a hashed representation of its abstract syntax tree (which serves
as a fast plausibility check for pre-selecting matching candidates) and the list of symbol
occurrences in the term, into which the algorithm recurses.
Secondly, we apply this view finder in two concrete case studies: In the first, we start with an abstract theory and try to figure out if it already exists in the same library. In the second example, we write down a simple theory of commutative operators in one language to find all commutative operators in another library based on a different language.
......@@ -98,5 +93,11 @@ In Section~\ref{sec:prelim}, we revise the basics of MMT and the representations
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: defemph compactenum textsf formalization vivews generalization centering
% LocalWords: compactitem lstset aboveskip 0pt,belowskip hline lstlisting mathescape
% LocalWords: rightarrow vdash emptyset baseset NorKoh:efnrsmk07 formalized omdoc emph
% LocalWords: standardized emph thibault-paper ednote
......@@ -106,14 +106,7 @@
\input{applications}
\section{Conclusion}\label{sec:concl}
% \paragraph{Future Work} \ednote{term indexing}\ednote{Better normalizing (Norman's thesis)}
\paragraph{Acknowledgments}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Open Archive for Formalizations (KO 2428/13-1).
\input{conclusion}
\renewcommand*{\bibfont}{\small}
\printbibliography
......@@ -121,6 +114,7 @@ Open Archive for Formalizations (KO 2428/13-1).
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: t
%%% End:
......@@ -131,4 +125,4 @@ Open Archive for Formalizations (KO 2428/13-1).
% LocalWords: tableofcontents defemph compactenum emptyset newpart compactitem lstset
% LocalWords: centering aboveskip 0pt,belowskip hline lstlisting mathescape rightarrow
% LocalWords: vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
% LocalWords: usecase
% LocalWords: usecase Unrealized
......@@ -195,5 +195,11 @@ The resulting formalizations are then used as meta-theory for imports of the lib
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: fig:mmt textbf textbf mapsto vdash_ emph hline ctabular ldots,x_m:t_m vec
% LocalWords: ldots,a_n compactitem cdot vec ednote ex:lamsyn urtheory mathcal f,t
% LocalWords: x:A;t oldpart fig:mmtgrammar centering vspace mdframed multirow ldots,x_n
% LocalWords: OAFproject:on vdash formalized formalizations tikzpicture ldots Arith
......@@ -61,7 +61,7 @@ Foundation-specific normalizations specifically for finding morphisms \emph{acro
We will discuss some of our findings specifically regarding the PVS library as a case study.
\subsection{Normalization in PVS}\label{sec:normalizeinter}
PVS~\cite{pvs} is a proof assistant under active development, based on a higher-order logic with predicate subtyping and various convenience features such as record types, update expressions and inductive datatypes. In addition to the \emph{Prelude} library, which contains the most common domains of mathematical discourse and is shipped with PVS itself, there is a large library of formal mathematics developed and maintained by NASA~\cite{nasa}.
PVS~\cite{pvs} is a proof assistant under active development, based on a higher-order logic with predicate subtyping and various convenience features such as record types, update expressions and inductive datatypes. In addition to the \emph{Prelude} library, which contains the most common domains of mathematical discourse and is shipped with PVS itself, there is a large library of formal mathematics developed and maintained by NASA~\cite{PVSlibraries:url}.
\paragraph{} While features like subtyping and records are interesting challenges, we will concentrate on one specific idiosyncracy in PVS -- its prevalent use of \emph{theory parameters}.
......@@ -110,17 +110,31 @@ We have tried the first two approaches regarding theory parameters -- i.e. the s
\begin{figure}[ht]\centering
\begin{tabular}{l | l || c | c}
\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Morphisms} & \textbf{Aggregated} \\\hline
bla & bla & bla & bla
NASA/monoid & simple & 388 & 154 \\
MitM/monoid & simple & 32 & 17 \\\hline
NASA/monoid & covariant & 1077 & 542 \\
MitM/monoid & covariant & & \\
\end{tabular}
\caption{Results of Inter- and Intra-Library Viewfinding in the PVS NASA Library}\label{fig:pvsresults}
\end{figure}
Most of the results in the simple MitM$\to$NASA case are artifacts of the theory parameter treatments -- in fact only two of the 17 results seem accurate. In the covariant case, the first $n$ results look meaningful, the rest are spurious small morphisms that can easily be automatically identified as such.
\paragraph{} As an additional use case, we can examplary write down a theory for a commutative binary operator using the MitM foundation, while targeting the PVS Prelude library -- allowing us to find all commutative operators, as in Figure \ref{fig:use:pvs} (using the simple approach to theory parmeters).
With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.
\paragraph{} As an additional use case, we can write down a theory for a commutative binary operator using the MitM foundation, while targeting the PVS Prelude library -- allowing us to find all commutative operators, as in Figure \ref{fig:use:pvs} (using the simple approach to theory parmeters).
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\end{figure}
This example also hints at a way to iteratively improve the results of the viewfinder: since we can find properties like commutativity and associativity, we can use the results to in turn inform a better normalization of the theory by exploiting these properties. This in turn would potentially allow for finding more views.
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
This example also hints at a way to iteratively improve the results of the viewfinder: since we can find properties like commutativity and associativity, we can use the results to in turn inform a better normalization of the theory by exploiting these properties. This in turn would potentially allow for finding more views.
\ No newline at end of file
% LocalWords: ednote centering fbox includegraphics textwidth beautysource smglom pvs
......@@ -184,6 +184,11 @@ The symbols will hence be encoded in the component $t$ instead of the list $s$.
%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-coloumn 5000)
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: defemph defemph emph vdash_ normalization optimized compactenum textbf th
% LocalWords: t,s ednote renormalize oldpart syms mapsto mapsto ldots,l compactitem
% LocalWords: normalizing subtyping subterms preprocessings ldots ldots formalization
% LocalWords: vdash Rightarrow vdash vdash vdash forall vdash
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment