Commit f7a206d0 authored by Dennis Müller's avatar Dennis Müller
Browse files

PVS stuff

parent d06be01e
......@@ -58,11 +58,37 @@ The normalizations mentioned in Section \ref{sec:normalizeintra} already suggest
Foundation-specific normalizations specifically for finding morphisms \emph{across} libraries is to our knowledge an as-of-yet unexplored field of investigation. Every formal system has certain unique idiosyncracies, best practices or widely used features; finding an ideal normalization method is a correspondingly difficult domain-specific problem.
We will discuss some of our findings specifically regarding the PVS\cite{pvs} library as a case study.
We will discuss some of our findings specifically regarding the PVS library as a case study.
\subsection{Normalization in PVS}\label{sec:normalizeinter}
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{nasa}.
\paragraph{} While features like subtyping and records are interesting challenges, we will concentrate on one specific idiosyncracy in PVS -- its prevalent use of \emph{theory parameters}.
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.
Given that the same practice is used in few other systems (if any), finding 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:
\begin{enumerate}
\item We can simply treat references to theory parameters as free variables and turn them into holes. Includes of parametric theories with arguments are turned into simple includes.
\item \emph{Covariant treatment:} We introduce new constants for the theory parameters and replace occurences of the parameters by constant references. Includes with parameters are again replaced by normal includes.
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})$.
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 occurences of \cn{inverse\_exists?} in \cn{group} would be replaced by $\oma{\cn{inverse\_exists?}}{S,\circ,e}$.
\end{enumerate}
The first approach is the most straight-forward, but will lead to many false positives and negatives.
We conjecture that 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 pass on to includes without additional tranformations.
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 viewfinding between PVS theories.
\paragraph{} Additionally to the theory parameter related normlalization, we use the following techniques:
\ednote{TODO}
\begin{itemize}
\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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment