usecase.tex 13.7 KB
Newer Older
1
2
\begin{newpart}{moved}
\subsection{Normalization}\label{sec:normalizeintra}
Dennis Müller's avatar
Dennis Müller committed
3
4
5
In addition to the above optimizations in the algorithm, we can normalize the theories themselves in various ways to improve the number and quality of the morphisms found. To accomodate these, we add two additional features to the algorithm:
\begin{enumerate}
	\item Some normalizations -- such as elaborating definitions -- may also reduce the number of results, for example if both theories use similar abbreviations for complex terms, or the same concept is declared axiomatically in one theory, but definitionally in the other. For that reason, we can allow \textbf{several abstract syntax trees for the same constant}, such as one with definitions expanded and one ``as is''.
Michael Kohlhase's avatar
Michael Kohlhase committed
6
	\item Similarly, certain idiosyncrasies (such as PVS's common usage of theory parameters, see Section \ref{sec:normalizeinter}) call for not just matching symbol references, but also variables or possibly even complex expressions. To handle these situations, we additionally allow for \textbf{holes} in the constant lists of an abstract syntax tree, which may be unified with any other symbol or hole by the core algorithm, but are not recursed into and do not count as a requirement. The subterms that are to be considered holes can be marked as such during preprocessing or normalizing.
Dennis Müller's avatar
Dennis Müller committed
7
\end{enumerate}
8

Dennis Müller's avatar
Dennis Müller committed
9
The common logical framework used for all the libraries at our disposal  -- namely LF and extensions thereof -- makes it easy to systematically normalize theories built on various logical foundations. On the basis of the above features, we currently use the following approaches to normalizing theories:
10
\begin{itemize}
Dennis Müller's avatar
Dennis Müller committed
11
	\item Free variables in a term are replaced by holes.
Michael Kohlhase's avatar
Michael Kohlhase committed
12
	\item Since judgments -- in our imports -- correspond to constants of type $\vdash P$ for some proposition $P$, we can use the Curry/Howard correspondence to equate the type $\vdash (P \Rightarrow Q)$ with the function type $(\vdash P) \to (\vdash Q)$, as well as the judgment $\vdash \forall x : A.\;P$ with the function type $(x:A) \to \vdash P$.
13
14
15
16
17
18
19
20
21
22
23
	
	Since both styles of formalization are more or less preferred in different systems, we replace each occurence of the former by the latter.
	\item For classical logics, we rewrite all remaining logical connectives using their usual definitions on the basis of negation and conjunction only. Double negations are eliminated.
	\item Typed Equalities are transformed to untyped ones; again getting rid of the redundant type argument of the equality.
	
	For example, the typed equality $\oma{\cn{equals}}{\mathbb N,2,1+1}$ becomes $\oma{\cn{equals}}{2,1+1}$, allowing to match the same equation on e.g. the real numbers.
	\item The arguments of conjunctions and equalities are ordered (currently only by their number of subterms).
\end{itemize}
\end{newpart}

\subsection{Implementation}\label{sec:usecase}
24
The view finder algorithm is implemented in the MMT system and exposed within the jEdit-IDE, allowing us to realize the use case
Dennis Müller's avatar
Dennis Müller committed
25
stated in the introduction. A screenshot of Jane's theory of beautiful sets is given in Figure \ref{fig:use:source}; it
Dennis Müller's avatar
Dennis Müller committed
26
is based on the (basic higher-order logic) foundation of the Math-in-the-Middle library (\cite{ODK:mitm:16} developed natively in MMT.
Dennis Müller's avatar
Dennis Müller committed
27
28

\begin{figure}[ht]\centering
Dennis Müller's avatar
Dennis Müller committed
29
  \fbox{\includegraphics[width=\textwidth]{beautysource}}
Dennis Müller's avatar
Dennis Müller committed
30
  \fbox{\includegraphics[width=\textwidth]{results}}
31
\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the View Finder}\label{fig:use:source}
Dennis Müller's avatar
Dennis Müller committed
32
33
\end{figure}

34
Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \cn{Find\ Views\ to...} $\to$ \cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) that two morphisms have been found, the most promising of which points to the theory
Dennis Müller's avatar
Dennis Müller committed
35
36
\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.

Michael Kohlhase's avatar
Michael Kohlhase committed
37
Note that the latter makes use of 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.
Dennis Müller's avatar
Dennis Müller committed
38

Dennis Müller's avatar
Dennis Müller committed
39
40
41
42
43
\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=0.6\textwidth]{matroids}}
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}
\end{figure}

44
\section{Inter-Library View Finding}\label{sec:across}
Dennis Müller's avatar
Dennis Müller committed
45

Dennis Müller's avatar
Dennis Müller committed
46
We have so far assumed one fixed meta-theory for all theories involved; we will now discuss the situation when looking for morphisms between theories in different libraries (and built on different foundations).
Dennis Müller's avatar
Dennis Müller committed
47

Michael Kohlhase's avatar
Michael Kohlhase committed
48
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's avatar
Dennis Müller committed
49
\begin{itemize}
Dennis Müller's avatar
Dennis Müller committed
50
51
	\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-morphism between theories -- 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})
	\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's avatar
Dennis Müller committed
52
\end{itemize}
Dennis Müller's avatar
Dennis Müller committed
53
54
55
\begin{newpart}{DM}
The normalizations mentioned in Section \ref{sec:normalizeintra} already suggest equating the involved logical primitives (such as logical connectives) via a meta-morphism.

Michael Kohlhase's avatar
Michael Kohlhase committed
56
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 idiosyncrasies, best practices or widely used features; finding an ideal normalization method is a correspondingly difficult domain-specific problem.
Dennis Müller's avatar
Dennis Müller committed
57

Dennis Müller's avatar
Dennis Müller committed
58
We will discuss some of our findings specifically regarding the PVS library as a case study.
Dennis Müller's avatar
Dennis Müller committed
59

60
\subsection{Normalization in PVS}\label{sec:normalizeinter}
Michael Kohlhase's avatar
Michael Kohlhase committed
61
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's avatar
Dennis Müller committed
62

Michael Kohlhase's avatar
Michael Kohlhase committed
63
\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's avatar
Dennis Müller committed
64
65
66

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.

67
Given that the same practice is used in few other systems (if any), searching for morphisms 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's avatar
Dennis Müller committed
68
\begin{enumerate}
Dennis Müller's avatar
merge    
Dennis Müller committed
69
	\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.
Dennis Müller's avatar
Dennis Müller committed
70
	
Michael Kohlhase's avatar
Michael Kohlhase committed
71
	\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's avatar
Dennis Müller committed
72
73
74
75
76
77
78
	
	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's avatar
Michael Kohlhase committed
79
	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's avatar
Dennis Müller committed
80
81
82
\end{enumerate}
	The first approach is the most straight-forward, but will lead to many false positives and negatives.
	
Dennis Müller's avatar
merge    
Dennis Müller committed
83
	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 passed on to includes with the same arguments without additional tranformations.
Dennis Müller's avatar
Dennis Müller committed
84
	
85
	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's avatar
Dennis Müller committed
86
	
Dennis Müller's avatar
merge    
Dennis Müller committed
87
	\paragraph{} Additionally to the theory parameter related normalization, we use the following techniques:
Dennis Müller's avatar
Dennis Müller committed
88
89

\begin{itemize}
90
	\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.
Dennis Müller's avatar
sec 5    
Dennis Müller committed
91
92
	
	For example: \[f = \lambda (n,m) : \mathbb N \times \mathbb N .\; n + m\text{ becomes } f = \lambda n : \mathbb N.\; \lambda m : \mathbb N .\; n + m\] \[f(\langle a, b\rangle)\text{ becomes }f(a,b).\]
Dennis Müller's avatar
Dennis Müller committed
93
94
	\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.
	
Dennis Müller's avatar
sec 5    
Dennis Müller committed
95
96
97
98
99
	For example, the apply-operator in the PVS meta-theory has the LF-type 
	\[(A : \cn{psvtype}) \to (B : \cn{pvstype}) \to \cn{pvsterm}_{A\Rightarrow B} \to \cn{pvsterm}_A \to \cn{pvsterm}_B \]
	Hence every application of a function 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}$.
	
	This prevents false negatives due to mismatching type arguments in the presence of subtyping.
Dennis Müller's avatar
Dennis Müller committed
100
\end{itemize}
Dennis Müller's avatar
Dennis Müller committed
101
\end{newpart}
Dennis Müller's avatar
Dennis Müller committed
102
103

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

105
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's avatar
merge    
Dennis Müller committed
106
107

\begin{figure}[ht]\centering
Dennis Müller's avatar
Dennis Müller committed
108
109
  \begin{tabular}{l | c || c | c}
  	\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Morphisms} & \textbf{Aggregated} \\\hline\hline
Dennis Müller's avatar
update    
Dennis Müller committed
110
111
112
  	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
113
  	MitM/monoid & covariant & 23 & 6 \\
Dennis Müller's avatar
merge    
Dennis Müller committed
114
  \end{tabular}
115
\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
116
117
\end{figure}

Michael Kohlhase's avatar
Michael Kohlhase committed
118
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 morphism lead to fuller (one total) and less spurious morphisms.
Dennis Müller's avatar
merge    
Dennis Müller committed
119

Dennis Müller's avatar
update    
Dennis Müller committed
120
121
122
123
With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand. 


\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 parmeters).
Dennis Müller's avatar
Dennis Müller committed
124

Dennis Müller's avatar
Update    
Dennis Müller committed
125
126
\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{pvs}}
Dennis Müller's avatar
Dennis Müller committed
127
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
Dennis Müller's avatar
adnote    
Dennis Müller committed
128
\end{figure}
129
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 morphisms.
Dennis Müller's avatar
Dennis Müller committed
130

Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
131
132
%%% Local Variables:
%%% mode: latex
Michael Kohlhase's avatar
Michael Kohlhase committed
133
134
%%% eval:  (set-fill-column 5000)
%%% eval:  (visual-line-mode)
Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
135
136
%%% TeX-master: "paper"
%%% End:
Dennis Müller's avatar
Dennis Müller committed
137

138
%  LocalWords:  ednote centering fbox includegraphics textwidth beautysource smglom pvs
Michael Kohlhase's avatar
Michael Kohlhase committed
139
140
141
142
143
144
%  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