usecase.tex 8.12 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

Florian Rabe's avatar
Florian Rabe committed
15
16
17
\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
18

Florian Rabe's avatar
Florian Rabe committed
19
20
21
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.
Dennis Müller's avatar
Dennis Müller committed
22

Florian Rabe's avatar
Florian Rabe committed
23
24
25
26
27
28
29
30
31
32
33
\paragraph{Theory Structure Normalization}
However, PVS's complex and prevalently used parametric theories critically affect view finding because it affects the structure of theories.
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
34
	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.
Florian Rabe's avatar
Florian Rabe committed
35
36
37
  This works well in the common case a parametric theory is not used with two different instantiations in the same context.
	\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
38
	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
39
40
41
42
%	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
43

Florian Rabe's avatar
Florian Rabe committed
44
45
46
47
48
49
50
	We have implemented the first two approaches.
	The first it 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.
%	A problem here is that the newly introduced constants are not passed on to includes with the same arguments without additional tranformations.
	The third approach will be our method of choice when investigating \emph{intra}-library views of PVS/NASA in future work.
%	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.
	
Dennis Müller's avatar
Dennis Müller committed
51
\subsection{Implementation}\label{sec:pvs}
Dennis Müller's avatar
merge    
Dennis Müller committed
52

Florian Rabe's avatar
Florian Rabe committed
53
54
\ednote{FR: this should be reread; I didn't have time to finish it up}

Florian Rabe's avatar
Florian Rabe committed
55
56
57
We have applied the first two simple and the covariant approach described above.
We wrote 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's avatar
merge    
Dennis Müller committed
58
59

\begin{figure}[ht]\centering
Dennis Müller's avatar
Dennis Müller committed
60
  \begin{tabular}{l | c || c | c}
Dennis Müller's avatar
Dennis Müller committed
61
  	\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Views} & \textbf{Aggregated} \\\hline\hline
Dennis Müller's avatar
update    
Dennis Müller committed
62
63
64
  	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
65
  	MitM/monoid & covariant & 23 & 6 \\
Dennis Müller's avatar
merge    
Dennis Müller committed
66
  \end{tabular}
67
\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
68
69
\end{figure}

Dennis Müller's avatar
Dennis Müller committed
70
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's avatar
update    
Dennis Müller committed
71
72
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
73
74
75
76
\ednote{FR: give example of an interesting view we found}

\paragraph{}
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 parameters).
Dennis Müller's avatar
Dennis Müller committed
77

Dennis Müller's avatar
Update    
Dennis Müller committed
78
79
\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{pvs}}
Dennis Müller's avatar
Dennis Müller committed
80
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
Dennis Müller's avatar
adnote    
Dennis Müller committed
81
\end{figure}
Dennis Müller's avatar
Dennis Müller committed
82
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's avatar
Dennis Müller committed
83

Florian Rabe's avatar
Florian Rabe committed
84
85
\ednote{FR: This second use case looks good, but might deserve some more emphasis, e.g., how many operators were found}

Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
86
87
%%% Local Variables:
%%% mode: latex
Michael Kohlhase's avatar
Michael Kohlhase committed
88
89
%%% eval:  (set-fill-column 5000)
%%% eval:  (visual-line-mode)
Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
90
91
%%% TeX-master: "paper"
%%% End:
Dennis Müller's avatar
Dennis Müller committed
92

93
%  LocalWords:  ednote centering fbox includegraphics textwidth beautysource smglom pvs
Michael Kohlhase's avatar
Michael Kohlhase committed
94
95
96
97
98
99
%  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
100
%  LocalWords:  PVSlibraries:on