usecase.tex 8.1 KB
Newer Older
Florian Rabe's avatar
Florian Rabe committed
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's avatar
Dennis Müller committed
6

Florian Rabe's avatar
Florian Rabe committed
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's avatar
Dennis Müller committed
8

Florian Rabe's avatar
Florian Rabe committed
9
\subsection{The PVS/NASA Library}\label{sec:normalizeinter}
Dennis Müller's avatar
Dennis Müller committed
10

Florian Rabe's avatar
Florian Rabe committed
11
12
13
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}.
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.
Dennis Müller's avatar
Dennis Müller committed
14

15
\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}
Florian Rabe's avatar
Florian Rabe committed
16
17
18
\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.
Dennis Müller's avatar
Dennis Müller committed
19

Florian Rabe's avatar
Florian Rabe committed
20
21
22
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.
23
\end{oldpart}
Dennis Müller's avatar
Dennis Müller committed
24

Florian Rabe's avatar
Florian Rabe committed
25
\paragraph{Theory Structure Normalization}
26
PVS's complex and prevalently used parametric theories critically affect view finding because they affect the structure of theories.
Florian Rabe's avatar
Florian Rabe committed
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's avatar
Dennis Müller committed
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.
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's avatar
Florian Rabe committed
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's avatar
Dennis Müller committed
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's avatar
Florian Rabe committed
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's avatar
Dennis Müller committed
45

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's avatar
Florian Rabe committed
49
%	A problem here is that the newly introduced constants are not passed on to includes with the same arguments without additional tranformations.
50
The third approach will be our method of choice when investigating \emph{intra}-library views of PVS/NASA in future work.
Florian Rabe's avatar
Florian Rabe committed
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.
52

Dennis Müller's avatar
Dennis Müller committed
53
\subsection{Implementation}\label{sec:pvs}
Dennis Müller's avatar
merge    
Dennis Müller committed
54

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's avatar
Florian Rabe committed
62

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's avatar
merge    
Dennis Müller committed
64
65

\begin{figure}[ht]\centering
Dennis Müller's avatar
Dennis Müller committed
66
  \begin{tabular}{l | c || c | c}
Dennis Müller's avatar
Dennis Müller committed
67
  	\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Views} & \textbf{Aggregated} \\\hline\hline
Dennis Müller's avatar
update    
Dennis Müller committed
68
69
70
  	NASA/monoid & simple & 388 & 154 \\
  	MitM/monoid & simple & 32 & 17 \\\hline
  	NASA/monoid & covariant & 1077 & 542 \\
Dennis Müller's avatar
Dennis Müller committed
71
  	MitM/monoid & covariant & 23 & 6 \\
Dennis Müller's avatar
merge    
Dennis Müller committed
72
  \end{tabular}
73
\caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}
Dennis Müller's avatar
merge    
Dennis Müller committed
74
75
\end{figure}

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's avatar
update    
Dennis Müller committed
77
78
With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand. 

Florian Rabe's avatar
Florian Rabe committed
79
80
\ednote{FR: give example of an interesting view we found}

Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
81
82
%%% Local Variables:
%%% mode: latex
Michael Kohlhase's avatar
Michael Kohlhase committed
83
84
%%% eval:  (set-fill-column 5000)
%%% eval:  (visual-line-mode)
Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
85
86
%%% TeX-master: "paper"
%%% End:
Dennis Müller's avatar
Dennis Müller committed
87

88
%  LocalWords:  ednote centering fbox includegraphics textwidth beautysource smglom pvs
Michael Kohlhase's avatar
Michael Kohlhase committed
89
90
91
92
93
94
%  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's avatar
Michael Kohlhase committed
95
%  LocalWords:  PVSlibraries:on