usecase.tex 8.54 KB
 Florian Rabe committed Apr 29, 2018 1 2 3 4 5 We now generalize to view finding to different libraries written in different logics. Intuitively, the key idea is that we now have two fixed meta-theories $M$ and $M'$ and a fixed meta-view $m:M\to M'$. However, due to the various idiosyncrasies of logics, tools' library structuring features, individual library conventions, this problem is significantly more difficult than \emph{intra}-library view finding. For example, unless the logics are closely related, meta-views usually do not even exist and must be approximated. Therefore, a lot of tweaking is typically necessary, and it is possible that multiple runs with different trade-offs give different interesting results.  Dennis Müller committed Apr 28, 2018 6   Florian Rabe committed Apr 29, 2018 7 As an example, we present a large case study where we find view from the MitM library used in the running example so far into the PVS/NASA library.  Dennis Müller committed Apr 28, 2018 8   Florian Rabe committed Apr 29, 2018 9 \subsection{The PVS/NASA Library}\label{sec:normalizeinter}  Dennis Müller committed Apr 26, 2018 10   Florian Rabe committed Apr 29, 2018 11 12 PVS~\cite{pvs} is a proof assistant under active development based on a higher-order logic with a number of advanced features. 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}.  Dennis Müller committed Apr 30, 2018 13 14 15 16 17 18 19 20 21 22 23 In \cite{KMOR:pvs:17}, we represent PVS as a meta-theory in MMT and implemented a translator that transforms both libraries into MMT format. we use a meta-view that embeds MitM's higher-order logic into PVS's higher-order logic and make sure that we normalize PVS-formulas in the same way as MitM-formulas. %\begin{oldpart}{MK: this sounds like a left-over from the time we had a PVS->HOL-Light use case. I think this can just be eft out. or reduce to the last sentence and leave out the paragrpah} %\paragraph{Formula Normalization} %Naturally advanced features of the PVS type system such as predicate subtyping, record types, inductive types will not be part of views from MitM, which does not have corresponding features. %Therefore, our view finder can mostly ignore them. % %Instead, we only have to normalize PVS formulas to the extent that they use logical features that correspond to those of MitM. %This is particular the basic higher-order logic. %Thus, we use a meta-view that embeds MitM's higher-order logic into PVS's higher-order logic and make sure that we normalize PVS-formulas in the same way as MitM-formulas. %\end{oldpart}  Dennis Müller committed Apr 28, 2018 24   Florian Rabe committed Apr 29, 2018 25 \paragraph{Theory Structure Normalization}  Michael Kohlhase committed Apr 30, 2018 26 PVS's complex and prevalently used parametric theories critically affect view finding because they affect the structure of theories.  Florian Rabe committed Apr 29, 2018 27 28 29 30 31 32 33 34 35 For example, the theory of groups \cn{group\_def} in the NASA library has three theory parameters $(\cn T,\ast,\cn{one})$ for the signature of groups, and includes the theory \cn{monoid\_def} with the same parameters, and then declares the axioms for a group in terms of these parameters. Without special treatment, we could only find views from/into libraries that use the same theory structure. We have investigated three approaches of handling parametric theories: \begin{compactenum} \item \emph{Simple treatment:} We drop theory parameters and interpret references to them as free variables that match anything. This is of course not sound so that all found views must be double-checked. However, because practical search problems often do not require exact results, even returning all potential views can be useful. \item \emph{Covariant elimination:} We treat theory parameters as if they were constants declared in the body.  Dennis Müller committed Apr 28, 2018 36  In the above mentioned theory \cn{group\_def}, we would hence add three new constants \cn T, $\ast$ and \cn{one} with their corresponding types.  Michael Kohlhase committed Apr 30, 2018 37  This works well in the common case where a parametric theory is not used with two different instantiations in the same context.  Florian Rabe committed Apr 29, 2018 38 39  \item \emph{Contravariant elimination:} The theory parameters are treated as if they were bound separately for every constant in the body of the theory.  Dennis Müller committed Apr 28, 2018 40  In the above mentioned theory \cn{group\_def}, we would change e.g. the unary predicate \cn{inverse\_exists?} with type $T\to\cn{bool}$ to a function with type $(T : \cn{pvstype})\to(\ast : T \to T \to T)\to (\cn{one}:T)\to(T\to\cn{bool})$.  Florian Rabe committed Apr 29, 2018 41 42 43 44 % An include of $\cn{group\_def}(S,\circ,e)$ in some other theory, e.g. \cn{group}, would be replaced by a simple include, but occurrences of \cn{inverse\_exists?} in \cn{group} would be replaced by $\oma{\cn{inverse\_exists?}}{S,\circ,e}$. This is closest to the actual semantics of the PVS module system. But it makes finding interesting views the least likely because it is the most sensitive to the modular structure of individual theories. \end{compactenum}  Dennis Müller committed Apr 26, 2018 45   Michael Kohlhase committed Apr 30, 2018 46 47 48 We have implemented the first two approaches. The first is the most straightforward but it leads to many false positives and false negatives. We have found the second approach to be the most useful for inter-library search since it most closely corresponds to simple formalizations of abstract theories in other libraries.  Florian Rabe committed Apr 29, 2018 49 % A problem here is that the newly introduced constants are not passed on to includes with the same arguments without additional tranformations.  Michael Kohlhase committed Apr 30, 2018 50 The third approach will be our method of choice when investigating \emph{intra}-library views of PVS/NASA in future work.  Florian Rabe committed Apr 29, 2018 51 % would turn every occurrence of e.g. group-related symbols into function applications, which is a rather rare practice in most other systems. However, since this treatment of theory parameters comes closest to the semantics of the parameters, we conjecture that it is the most useful approach for intra-library view finding between PVS theories.  Michael Kohlhase committed Apr 30, 2018 52   Dennis Müller committed Apr 26, 2018 53 \subsection{Implementation}\label{sec:pvs}  Dennis Müller committed Apr 28, 2018 54   Michael Kohlhase committed Apr 30, 2018 55 56 57 58 59 60 61 As a first 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}} \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 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.  Florian Rabe committed Apr 30, 2018 62   Dennis Müller committed Apr 30, 2018 63 To evaluate the approaches to theory parameters we used a simple theory of monoids in the MitM foundation and the theory of monoids in the NASA library as domains for viewfinding with the whole NASA library as target using simple and covariant approaches. The results are summarized in Figure \ref{fig:pvsresults}.  Dennis Müller committed Apr 28, 2018 64 65  \begin{figure}[ht]\centering  Dennis Müller committed Apr 29, 2018 66  \begin{tabular}{l | c || c | c}  Dennis Müller committed Apr 29, 2018 67  \textbf{Domain} & \textbf{Normalization} & \textbf{Simple Views} & \textbf{Aggregated} \\\hline\hline  Dennis Müller committed Apr 28, 2018 68 69  NASA/monoid & simple & 388 & 154 \\ MitM/monoid & simple & 32 & 17 \\\hline  Dennis Müller committed Apr 30, 2018 70 71  NASA/monoid & covariant & 1026 & 566 \\ MitM/monoid & covariant & 22 & 6 \\  Dennis Müller committed Apr 28, 2018 72  \end{tabular}  Dennis Müller committed Apr 28, 2018 73 \caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}  Dennis Müller committed Apr 28, 2018 74 75 \end{figure}  Michael Kohlhase committed Apr 30, 2018 76 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 additional requirements lead to fuller (one total) and less spurious views.  Dennis Müller committed Apr 30, 2018 77 With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand. With the simple approach to theory parameters, most results can be considered artifacts; in the covariant case, the most promising results yield (partial) views into the theories of semigroups, groups, rings (both the multiplicative and additive parts) and most extensions thereof (due to the duplication of theory parameters as constants).  Florian Rabe committed Apr 30, 2018 78   Michael Kohlhase committed Apr 28, 2018 79 80 %%% Local Variables: %%% mode: latex  Michael Kohlhase committed Apr 29, 2018 81 82 %%% eval: (set-fill-column 5000) %%% eval: (visual-line-mode)  Michael Kohlhase committed Apr 28, 2018 83 84 %%% TeX-master: "paper" %%% End:  Dennis Müller committed Apr 26, 2018 85   Michael Kohlhase committed Apr 28, 2018 86 % LocalWords: ednote centering fbox includegraphics textwidth beautysource smglom pvs  Michael Kohlhase committed Apr 29, 2018 87 88 89 90 91 92 % LocalWords: newpart Normalization sec:normalizeintra optimizations normalizations a,b % LocalWords: textbf sec:normalizeinter subterms normalizing vdash vdash Rightarrow % LocalWords: vdash vdash vdash forall vdash formalization mathbb sec:usecase coll emph % LocalWords: subtyping PVSlibraries:url monoid formalized pvstype circ,e circ,e ldots % LocalWords: formalizations ldots langle psvtype pvsterm pvsterm pvsterm mmt-term % LocalWords: pvsapply Monoids Monoids summarized fig:pvsresults hline hline  Michael Kohlhase committed Apr 29, 2018 93 % LocalWords: PVSlibraries:on