usecase.tex 8.67 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
6
7
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''.
	\item Similarly, certain idiosyncracies (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.
\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.
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
	\item For foundations that use product types, 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.
	
	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).\]
	\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$.
	
	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}
Dennis Müller's avatar
Dennis Müller committed
27
28
The Viewfinder algorithm is implemented in the MMT system and exposed within the jEdit-IDE, allowing us to realize the use case
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
29
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
30
31

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

Dennis Müller's avatar
Update    
Dennis Müller committed
37
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 views have been found, the most promising of which points to the theory
Dennis Müller's avatar
Dennis Müller committed
38
39
\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.

Dennis Müller's avatar
Dennis Müller committed
40
41
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
42
43
44
45
46
\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}

47
\section{Inter-Library Viewfinding}\label{sec:across}
Dennis Müller's avatar
Dennis Müller committed
48

Dennis Müller's avatar
Dennis Müller committed
49
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
50
51
52

Obviously, various differences in available foundational primitives and library-specific best practices and idiosyncracies can prevent the algorithm from finding desired matches. There are two approaches to increasing the number of results in these cases:
\begin{itemize}
Dennis Müller's avatar
Dennis Müller committed
53
54
	\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
55
\end{itemize}
Dennis Müller's avatar
Dennis Müller committed
56
57
58
59
60
61
\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.

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.
Dennis Müller's avatar
Dennis Müller committed
62

63
\subsection{Normalization in PVS}\label{sec:normalizeinter}
Dennis Müller's avatar
Dennis Müller committed
64

Dennis Müller's avatar
Dennis Müller committed
65
\ednote{TODO}
Dennis Müller's avatar
Dennis Müller committed
66
\begin{itemize}
67
	\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
68
69
	
	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
70
71
	\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
72
73
74
75
76
	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
77
\end{itemize}
Dennis Müller's avatar
Dennis Müller committed
78
\end{newpart}
Dennis Müller's avatar
Dennis Müller committed
79
80
81

\subsection{Implementation}\label{sec:pvs}
\paragraph{} Using the above normalization methods, we can examplary write down a theory for a commutative binary operator using the Math-in-the-Middle foundation, while targeting e.g. the PVS Prelude library -- allowing us to find all commutative operators, as in Figure \ref{fig:use:pvs}.
Dennis Müller's avatar
Dennis Müller committed
82

Dennis Müller's avatar
Update    
Dennis Müller committed
83
84
\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{pvs}}
Dennis Müller's avatar
Dennis Müller committed
85
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
Dennis Müller's avatar
adnote    
Dennis Müller committed
86
\end{figure}
Dennis Müller's avatar
Dennis Müller committed
87
88
\ednote{8 results for NASA, but NASA doesn't work in jEdit because of limited memory}

89
This example also hints at a way to iteratively improve the results of the viewfinder: 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.