Commit abba2964 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

little fixes

parent 9f8d6a66
\begin{newpart}{DM}
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. 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.
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: 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:
\end{newpart}
\begin{itemize} \begin{itemize}
\item \textbf{Model-/Countermodel Finding:} If the codomain of a morphism is a theory representing a specific model, it would tell her that those \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.
are \emph{examples} of her abstract theory.
Furthermore, partial morphisms -- especially those that are total on some included theory -- could Furthermore, partial morphisms -- especially those that are total on some included theory -- could be insightful \emph{counterexamples}.
be insightful \emph{counterexamples}.
\item \textbf{Library Refactoring:} Given that the view finder looks for \emph{partial} morphisms, we can use it to find natural \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.
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 morphisms would inform her, that her theory would probably better 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.
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 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, \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.
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 transfomations during preprocessing and normalization, we could use the found \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.
morphisms 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 -- 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.
which on the basis of our encodings can be done directly by the view finder.
A useful interface might specifically prioritize morphisms into theories on top of which there are many A useful interface might specifically prioritize morphisms into theories on top of which there are many theorems and definitions that have been discovered.
theorems and definitions that have been discovered.
\end{itemize} \end{itemize}
For some of these use cases it would be advantageous to look for morphisms \emph{into} our working theory instead. For some of these use cases it would be advantageous to look for morphisms \emph{into} our working theory instead.
......
...@@ -221,6 +221,9 @@ ...@@ -221,6 +221,9 @@
PAGES = {748--752}, PAGES = {748--752},
PUBLISHER = {Springer}, PUBLISHER = {Springer},
} }
@online{PVSlibraries:on,crossref={PVSlibraries:base},
urldate = {2014-12-17},
label = {PVS}}
@MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS}, @MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS},
howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}} howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}}
@MISC{PVSlibraries:base, @MISC{PVSlibraries:base,
...@@ -260,4 +263,4 @@ ...@@ -260,4 +263,4 @@
location = {Manchester, United Kingdom}, location = {Manchester, United Kingdom},
publisher = {ACM}, publisher = {ACM},
keywords = {conference}, keywords = {conference},
address = {New York, NY, USA}} address = {New York, NY, USA}}
\ No newline at end of file
...@@ -58,7 +58,7 @@ Foundation-specific normalizations specifically for finding morphisms \emph{acro ...@@ -58,7 +58,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. We will discuss some of our findings specifically regarding the PVS library as a case study.
\subsection{Normalization in PVS}\label{sec:normalizeinter} \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{PVSlibraries:url}. 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:on}.
\paragraph{} While features like subtyping and records are interesting challenges, we will concentrate on one specific idiosyncrasy in PVS -- its prevalent use of \emph{theory parameters}. \paragraph{} While features like subtyping and records are interesting challenges, we will concentrate on one specific idiosyncrasy in PVS -- its prevalent use of \emph{theory parameters}.
......
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