conclusion.tex 4.8 KB
 Michael Kohlhase committed Apr 28, 2018 1 We present a general MKM utility that given a \MMT theory and an \MMT library $\cL$ finds  Dennis Müller committed Apr 29, 2018 2 partial and total views into $\cL$.  Dennis Müller committed Apr 28, 2018 3 Such a view finder can be used to drive various MKM applications ranging from theory classification to library merging and refactoring.  Michael Kohlhase committed Apr 30, 2018 4 5 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}.  Michael Kohlhase committed Apr 28, 2018 6 7  \paragraph{Future Work}  Dennis Müller committed Apr 28, 2018 8 The current view finder is already efficient enough for the limited libraries we used for testing.  Michael Kohlhase committed Apr 28, 2018 9 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.  Dennis Müller committed Apr 29, 2018 10 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.  Michael Kohlhase committed Apr 28, 2018 11 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}.  Michael Kohlhase committed Apr 28, 2018 12   Florian Rabe committed Apr 30, 2018 13 14 \paragraph{Enabled Applications} Our work enables a number of advanced applications.  Michael Kohlhase committed Apr 30, 2018 15 16 Maybe surprisingly, a major bottleneck here concerns less the algorithm or software design challenges but user interfaces and determining the right application context.  Florian Rabe committed Apr 30, 2018 17 \begin{compactitem}  Michael Kohlhase committed Apr 30, 2018 18 19 \item \textbf{Model-/Countermodel Finding:} If the codomain of a view is a theory representing a specific model, it would tell Jane that those are \emph{examples} of her abstract theory. Furthermore, partial views -- especially those that are total on some included theory -- could lead to insightful \emph{counterexamples}.  Florian Rabe committed Apr 30, 2018 20 21 22 23 24 25 % \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. %  Michael Kohlhase committed Apr 30, 2018 26 27 \item \textbf{Folklore-based Conjecturing:} If we have theory $T$ describing (the properties of) a class $O$ of objects under consideration and a view $v:S\rightsquigarrow T$, then we can use extensions of $S'$ in $\cL$ with $\iota: S\hookrightarrow S'$ for making conjectures about $O$: The $v$-images of the local axioms of $T'$ would make useful properties to establish about $O$, since they allow pushing out $v$ over $\iota$ to a view $v':S'\rightsquigarrow T'$ and gain $v'(T')$ as properties of $O$. Note that we would need to keep book on our transformations during preprocessing and normalization, so that we could use the found views for translating both into the codomain as well as back from there into our starting theory.  Florian Rabe committed Apr 30, 2018 28 29 30 31 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} 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}).  Michael Kohlhase committed Apr 28, 2018 32 33 34 35 36 37 38 \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  Michael Kohlhase committed Apr 29, 2018 39 40 %%% eval: (set-fill-column 5000) %%% eval: (visual-line-mode)  Michael Kohlhase committed Apr 28, 2018 41 42 %%% TeX-master: "paper" %%% End:  Michael Kohlhase committed Apr 28, 2018 43   Michael Kohlhase committed Apr 30, 2018 44 % LocalWords: unrealized am:doceng10,iancu:msc Formalizations sec:usecase mathhub RupKohMue:fitgv17 compactitem textbf Countermodel emph Generalization generalization normalization prioritize sec:algparams sec:normalizeintra sec:normalizeinter