Commit c08f8c1e authored by Florian Rabe's avatar Florian Rabe
Browse files

no message

parent 48bbb911
......@@ -9,6 +9,31 @@ To increase efficiency, we plan to explore term indexing techniques~\cite{Graf:t
The latter will be important for the library refactoring and merging applications which look for all possible (partial and total) views 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{Enabled Applications}
\ednote{FR: I've moved this here from Sect. 5. I suspect it should be reread carefully.}
Our work enables a number of advanced applications.
Maybe surprisingly, a major bottleneck here concerns less the algorithm or software design challenges but user interfaces.
The theory discovery use case described in Sect.~\ref{sec:usecase} is mostly desirable in a setting where a user is actively writing or editing a theory, so the integration in jEdit is sensible.
However, the inter-library view finding would be a lot more useful in a theory exploration setting, such as when browsing available archives on MathHub~\cite{mathhub} or in the graph viewer integrated in \mmt ~\cite{RupKohMue:fitgv17}.
Additional specialized user interfaces would enable or improve the following use cases:
\begin{compactitem}
\item \textbf{Model-/Countermodel Finding:} If the codomain of a view is a theory representing a specific model, it would tell her that those are \emph{examples} of her abstract theory.
Furthermore, partial views -- especially those that are total on some included theory -- could be insightful \emph{counterexamples}.
%
\item \textbf{Library Refactoring:} Given that the view finder looks for \emph{partial} views, we can use it to find natural extensions of a starting theory. Imagine Jane removing the last of her axioms for ``beautiful sets'' -- the other axioms (disregarding finitude of her sets) would allow her to find e.g. both Matroids and \emph{Ideals}, which would suggest to her to refactor her library accordingly.
Additionally, \emph{surjective} partial views would inform her, that her theory would probably better be refactored as an extension of the codomain, which would allow her to use all theorems and definitions therein.
%
\item \textbf{Theory Generalization:} If we additionally consider views into and out of the theories found, this can make theory discovery even more attractive. For example, a view from a theory of vector spaces intro matroids could inform Jane additionally, that her beautiful sets, being matroids, form a generalization of the notion of linear independence in linear algebra.
%
\item \textbf{Folklore-based Conjecture:} If we were to keep book on our transformations during preprocessing and normalization, we could use the found views for translating both into the codomain as well as back from there into our starting theory.
This would allow for e.g. discovering and importing theorems and useful definitions from some other library -- which on the basis of our encodings can be done directly by the view finder.
A useful interface might specifically prioritize views into theories on top of which there are many theorems and definitions that have been discovered.
\end{compactitem}
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 aggregate and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
\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
......
......@@ -68,7 +68,7 @@ However, at that time no large corpora of formalized mathematics were available
This situation has changed since then as multiple such exports have become available.
In particular, we have developed the MMT language \cite{RK:mmt:10} and the concrete syntax of the OMDoc XML format \cite{omdoc} as a uniform representation language for such corpora.
And we have translated multiple proof assistant libraries into this format, including the ones of PVS in \cite{KMOR:pvs:17} and HOL Light in \cite{KR:hollight:14}.
And we have translated multiple proof assistant libraries into this format, among others those of PVS in \cite{KMOR:pvs:17}.
Building on these developments, we are now able, for the first time, to apply generic methods --- i.e., methods that work at the MMT level --- to search for views in these libraries.
While inspired by the ideas of \cite{NorKoh:efnrsmk07}, our design and implementation are completely novel.
......@@ -86,12 +86,12 @@ separating the term into a hashed representation of its abstract syntax tree (wh
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 -- the use case mention above. 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.
Secondly, we apply this view finder in a concrete case study: In the first, we start with an abstract theory and try to figure out if it already exists in the same library -- the use case mention above. 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.\ednote{FR: this paragraph is vague; also we only have one case study, do we?}
\paragraph{Overview}
In Section~\ref{sec:prelim}, we revise the basics of MMT and the representations of (exemplary) the PVS and HOL Light libraries.
In Section~\ref{sec:prelim}, we revise the basics of MMT and views.
Section~\ref{sec:viewfinder} presents the view finding algorithm restricted to the intra-library case and showcases it for the theory classification use case.
In Section~\ref{sec:across}, we extend the algorithm to inter-library view finding discuss results of applying it to the HOL Light and PVS libraries.
In Section~\ref{sec:across}, we extend the algorithm to inter-library view finding discuss results of applying it to the PVS/NASA library.
Section~\ref{sec:appl} discusses additional applications and Section~\ref{sec:concl} concludes the paper.
%%% Local Variables:
......
......@@ -103,8 +103,8 @@
\section{Inter-Library View Finding}\label{sec:across}
\input{usecase}
\section{Low-Hanging Fruit: Other Applications}\label{sec:appl}
\input{applications}
%\section{Low-Hanging Fruit: Other Applications}\label{sec:appl}
%\input{applications}
\section{Conclusion}\label{sec:concl}
\input{conclusion}
......
......@@ -50,6 +50,8 @@ We have investigated three approaches of handling parametric theories:
\subsection{Implementation}\label{sec:pvs}
\ednote{FR: this should be reread; I didn't have time to finish it up}
We have applied the first two simple and the covariant approach described above.
We wrote a simple theory of monoids in the Math-in-the-Middle foundation and the theory of Monoids in the NASA library as domains with the whole NASA library as target.
The results are summarized in Figure \ref{fig:pvsresults}.
......@@ -68,7 +70,10 @@ The results are summarized in Figure \ref{fig:pvsresults}.
Most of the results in the simple MitM$\to$NASA case are artefacts of the theory parameter treatments -- in fact only two of the 17 results are meaningful (to operations on sets and the theory of number fields). In the covariant case, the more requirements of each simple views lead to fuller (one total) and less spurious views.
With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.
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).
\ednote{FR: give example of an interesting view we found}
\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 parameters).
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
......@@ -76,6 +81,8 @@ As an additional use case, we can write down a theory for a commutative binary o
\end{figure}
This example also hints at a way to iteratively improve the results of the view finder: 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.
\ednote{FR: This second use case looks good, but might deserve some more emphasis, e.g., how many operators were found}
%%% Local Variables:
%%% mode: latex
%%% eval: (set-fill-column 5000)
......
Markdown is supported
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