@@ -10,17 +10,17 @@ As an example, we present a large case study where we find view from the MitM li

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.

\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}

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}

\paragraph{Theory Structure Normalization}

PVS's complex and prevalently used parametric theories critically affect view finding because they affect the structure of theories.

...

...

@@ -60,23 +60,21 @@ As a first use case, we can write down a theory for a commutative binary operat

\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.

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}.

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}.

\caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}

\end{figure}

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.

With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.

\ednote{FR: give example of an interesting view we found}

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).

involves two steps: \textbf{MMT-level normalization} performs generic transformations that do not depend on the meta-theory $M$.

These include elaboration of structured theories and definition expansion, which we mentioned in Sect.~\ref{sec:prelim}.

Importantly, we do not fully eliminate defined constant declarations $c:E=e$ from a theory $\Sigma$: instead, we replace them with primitive constants $c:E$ and replace every occurrence of $c$ in other declarations with $e$.

...

...

@@ -228,7 +228,7 @@ The latter menu offers a choice of known libraries in which the view finder shou

\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}\vspace*{-1em}

\end{wrapfigure}

\noindent After choosing \cn{MitM/smglom}, the view finder finds two views (within less than one second) and shows them (Figure~\ref{fig:use:results}).

The first of these ($\cn{View0}$) has a theory for matroids as its codomain, which is given in Figure \ref{fig:use:target}.

The first of these ($\cn{View1}$) has a theory for matroids as its codomain, which is given in Figure \ref{fig:use:target}.

Inspecting that theory and the assignments in the view, we see that it indeed represents the well-known correspondence between beautiful sets and matroids.

%The latter uses predefined propositions in its axioms and uses a type \cn{coll} for the collection of sets, while the former has the statements of the axioms directly in the theory and uses a predicate \cn{beautiful}.

%Additionally, the implication that beautiful sets (or sets in a matroid) are finite is stated as a logical formula in the former, while the latter uses the Curry/Howard correspondence.