applications.tex 3.6 KB
 Dennis Müller committed Apr 28, 2018 1 We have seen how a view finder can be used for theory \emph{discovery} and finding constants with specific desired properties, but many other potential use cases are imaginable. The main problems to solve with respect to these is less about the algorithm or software design challenges, but user interfaces.  Dennis Müller committed Apr 26, 2018 2   Dennis Müller committed Apr 27, 2018 3 The theory discovery use case described in Sec. \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 across-library use case in Sec. \ref{sec:pvs} already 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:  Dennis Müller committed Apr 25, 2018 4 \begin{itemize}  Michael Kohlhase committed Apr 29, 2018 5 \item \textbf{Model-/Countermodel Finding:} If the codomain of a morphism is a theory representing a specific model, it would tell her that those are \emph{examples} of her abstract theory.  Dennis Müller committed Apr 25, 2018 6   Michael Kohlhase committed Apr 29, 2018 7  Furthermore, partial morphisms -- especially those that are total on some included theory -- could be insightful \emph{counterexamples}.  Dennis Müller committed Apr 25, 2018 8   Michael Kohlhase committed Apr 29, 2018 9 \item \textbf{Library Refactoring:} Given that the view finder looks for \emph{partial} morphisms, 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.  Dennis Müller committed Apr 25, 2018 10   Michael Kohlhase committed Apr 29, 2018 11  Additionally, \emph{surjective} partial morphisms 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.  Dennis Müller committed Apr 25, 2018 12   Michael Kohlhase committed Apr 29, 2018 13 14  \item \textbf{Theory Generalization:} If we additionally consider morphisms into and out of the theories found, this can make theory discovery even more attractive. For example, a morphism 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.  Dennis Müller committed Apr 25, 2018 15   Michael Kohlhase committed Apr 29, 2018 16 \item \textbf{Folklore-based Conjecture:} If we were to keep book on our transfomations during preprocessing and normalization, we could use the found morphisms for translating both into the codomain as well as back from there into our starting theory.  Dennis Müller committed Apr 25, 2018 17   Michael Kohlhase committed Apr 29, 2018 18  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.  Dennis Müller committed Apr 25, 2018 19   Michael Kohlhase committed Apr 29, 2018 20  A useful interface might specifically prioritize morphisms into theories on top of which there are many theorems and definitions that have been discovered.  Michael Kohlhase committed Apr 28, 2018 21 \end{itemize}  Dennis Müller committed Apr 28, 2018 22 For some of these use cases it would be advantageous to look for morphisms \emph{into} our working theory instead.  Dennis Müller committed Apr 25, 2018 23   Dennis Müller committed Apr 28, 2018 24 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) morphisms (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).  Michael Kohlhase committed Apr 28, 2018 25   Michael Kohlhase committed Apr 28, 2018 26 27 %%% Local Variables: %%% mode: latex  Michael Kohlhase committed Apr 28, 2018 28 %%% eval: (visual-line-mode) (set-fill-column 5000)  Michael Kohlhase committed Apr 28, 2018 29 30 %%% TeX-master: "paper" %%% End:  Michael Kohlhase committed Apr 28, 2018 31 32  % LocalWords: emph specialized generalization transfomations normalization prioritize  Michael Kohlhase committed Apr 29, 2018 33 34 % LocalWords: sec:usecase newpart sec:pvs mathhub RupKohMue:fitgv17 textbf Countermodel % LocalWords: sec:algparams sec:normalizeintra sec:normalizeinter