usecase.tex 9.13 KB
 Michael Kohlhase committed Apr 29, 2018 1 We now generalize to view-finding between theories in different libraries (and built on different foundations and meta-theories). Obviously, various differences in available foundational primitives and library-specific best practices and idiosyncrasies can prevent the algorithm from finding desired matches. There are two approaches to increasing the number of results in these cases:  Dennis Müller committed Apr 26, 2018 2 \begin{itemize}  Michael Kohlhase committed Apr 29, 2018 3  \item In many instances, the translations between two foundations is too complex to be discovered purely syntactically. In these cases we can provide arbitrary meta-morphisms between theories\ednote{MK: starting alignments?} -- especially (but not exclusively) on the meta-theories -- which are applied before computing the abstract syntax trees (e.g. alignment-based translations as in \cite{MRLR:alignments:17})  Dennis Müller committed Apr 28, 2018 4  \item We can apply additional foundation-specific normalizations before preprocessing theories, such as eliminating higher-order abstract syntax encodings or implicit arguments, or elaborating specific abbreviations/definitions.  Dennis Müller committed Apr 26, 2018 5 \end{itemize}  Dennis Müller committed Apr 28, 2018 6 7 The normalizations mentioned in Section \ref{sec:normalizeintra} already suggest equating the involved logical primitives (such as logical connectives) via a meta-morphism.  Dennis Müller committed Apr 29, 2018 8 Foundation-specific normalizations specifically for finding views \emph{across} libraries is to our knowledge an as-of-yet unexplored field of investigation. Every formal system has certain unique idiosyncrasies, best practices or widely used features; finding an ideal normalization method is a correspondingly difficult domain-specific problem.  Dennis Müller committed Apr 28, 2018 9   Dennis Müller committed Apr 28, 2018 10 We will discuss some of our findings specifically regarding the PVS library as a case study.  Dennis Müller committed Apr 26, 2018 11   Dennis Müller committed Apr 28, 2018 12 \subsection{Normalization in PVS}\label{sec:normalizeinter}  Michael Kohlhase committed Apr 29, 2018 13 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}.  Dennis Müller committed Apr 28, 2018 14   Michael Kohlhase committed Apr 29, 2018 15 \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}.  Dennis Müller committed Apr 28, 2018 16 17 18  In practice, theory parameters are often used in PVS for the signature of an abstract theory. 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, and includes the theory \cn{monoid\_def} with the same parameters; the axioms for a group are then formalized as a predicate on the theory parameters.  Dennis Müller committed Apr 29, 2018 19 Given that the same practice is used in few other systems (if any), searching for views without treating theory parameters in some way will not give us any useful results on these theories. We offer three approaches to handling these situations:  Dennis Müller committed Apr 28, 2018 20 \begin{enumerate}  Dennis Müller committed Apr 28, 2018 21  \item \emph{Simple treatment:} We can interpret references to theory parameters as free variables and turn them into holes. Includes of parametric theories with arguments are turned into simple includes.  Michael Kohlhase committed Apr 29, 2018 22  \item \emph{Covariant treatment:} We introduce new constants for the theory parameters and replace occurrences of the parameters by constant references. Includes with parameters are again replaced by normal includes.  Dennis Müller committed Apr 28, 2018 23 24 25  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. \item \emph{Contravariant treatment:} Theory parameters are eliminated by binding them as arguments to \emph{each constant in the theory}. References to the treated constants are replaced by applications of the symbols to the parameters of the original include. 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})$.  Michael Kohlhase committed Apr 29, 2018 26  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}$.  Dennis Müller committed Apr 28, 2018 27 \end{enumerate}  Michael Kohlhase committed Apr 29, 2018 28  We have implemented the first two approaches. The first it is the most straight-forward but it lead to many false positives and negatives. The second approach is most useful for inter-library search, since it most closely corresponds to formalizations of abstract theories in other systems. A problem here is that the newly introduced constants are not passed on to includes with the same arguments without additional tranformations.  Dennis Müller committed Apr 28, 2018 29   Dennis Müller committed Apr 28, 2018 30  The third approach would turn every occurence 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.  Dennis Müller committed Apr 28, 2018 31   Michael Kohlhase committed Apr 29, 2018 32 Additionally to the theory parameter related normalization, we use the following techniques:  Dennis Müller committed Apr 26, 2018 33 34  \begin{itemize}  Dennis Müller committed Apr 28, 2018 35  \item We curry function types $(A_1 \times\ldots A_n)\to B$ to $A_1 \to \ldots \to A_n\to B$. We treat lambda-expressions and applications accordingly.  Michael Kohlhase committed Apr 29, 2018 36  For example, $f(\langle a, b\rangle)$ becomes $f(a,b)$ and $4 = \lambda (n,m) : \mathbb N \times \mathbb N .\; n + m$ becomes $f = \lambda n : \mathbb N.\; \lambda m : \mathbb N .\; n + m$.  Dennis Müller committed Apr 26, 2018 37  \item Higher-order abstract syntax encodings are eliminated by raising atomic types, function types, applications and lambdas to the level of the logical framework. This eliminates (redundant) implicit arguments that only occur due to their formalization in the logical framework.  Michael Kohlhase committed Apr 29, 2018 38  For example, the apply-operator in the PVS meta-theory has the LF-type  Dennis Müller committed Apr 27, 2018 39  $(A : \cn{psvtype}) \to (B : \cn{pvstype}) \to \cn{pvsterm}_{A\Rightarrow B} \to \cn{pvsterm}_A \to \cn{pvsterm}_B$  Michael Kohlhase committed Apr 29, 2018 40  Hence every function application in PVS -- as \mmt-term: $\oma{\cn{pvsapply}}{A,B,f,a}$ -- has two additional implicit arguments, which we eliminate by replacing this expression by $\oma{f}{a}$.  Dennis Müller committed Apr 27, 2018 41  This prevents false negatives due to mismatching type arguments in the presence of subtyping.  Dennis Müller committed Apr 26, 2018 42 43 44 \end{itemize} \subsection{Implementation}\label{sec:pvs}  Dennis Müller committed Apr 28, 2018 45   Dennis Müller committed Apr 28, 2018 46 We have tried the first two approaches regarding theory parameters -- i.e. the simple and covariant treatments -- to both inter- and intra-library view finding problems. Concretely, we have used 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}.  Dennis Müller committed Apr 28, 2018 47 48  \begin{figure}[ht]\centering  Dennis Müller committed Apr 29, 2018 49  \begin{tabular}{l | c || c | c}  Dennis Müller committed Apr 29, 2018 50  \textbf{Domain} & \textbf{Normalization} & \textbf{Simple Views} & \textbf{Aggregated} \\\hline\hline  Dennis Müller committed Apr 28, 2018 51 52 53  NASA/monoid & simple & 388 & 154 \\ MitM/monoid & simple & 32 & 17 \\\hline NASA/monoid & covariant & 1077 & 542 \\  Dennis Müller committed Apr 29, 2018 54  MitM/monoid & covariant & 23 & 6 \\  Dennis Müller committed Apr 28, 2018 55  \end{tabular}  Dennis Müller committed Apr 28, 2018 56 \caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}  Dennis Müller committed Apr 28, 2018 57 58 \end{figure}  Dennis Müller committed Apr 29, 2018 59 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.  Dennis Müller committed Apr 28, 2018 60 61 With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.  Michael Kohlhase committed Apr 29, 2018 62 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).  Dennis Müller committed Apr 25, 2018 63   Dennis Müller committed Apr 25, 2018 64 65 \begin{figure}[ht]\centering \fbox{\includegraphics[width=\textwidth]{pvs}}  Dennis Müller committed Apr 25, 2018 66 \caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}  Dennis Müller committed Apr 26, 2018 67 \end{figure}  Dennis Müller committed Apr 29, 2018 68 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.  Dennis Müller committed Apr 26, 2018 69   Michael Kohlhase committed Apr 28, 2018 70 71 %%% Local Variables: %%% mode: latex  Michael Kohlhase committed Apr 29, 2018 72 73 %%% eval: (set-fill-column 5000) %%% eval: (visual-line-mode)  Michael Kohlhase committed Apr 28, 2018 74 75 %%% TeX-master: "paper" %%% End:  Dennis Müller committed Apr 26, 2018 76   Michael Kohlhase committed Apr 28, 2018 77 % LocalWords: ednote centering fbox includegraphics textwidth beautysource smglom pvs  Michael Kohlhase committed Apr 29, 2018 78 79 80 81 82 83 % 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 84 % LocalWords: PVSlibraries:on