usecase.tex 7.31 KB
 Dennis Müller committed Apr 28, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 \begin{newpart}{moved} \subsection{Normalization}\label{sec:normalizeintra} When elaborating definitions, it is important to consider that this may also reduce the number of results, 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''. Similarly, certain idiosyncracies -- such as PVS's common usage of theory parameters -- 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, but are not recursed into. The subterms that are to be considered holes can be marked as such during preprocessing. \begin{itemize} \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 committed Apr 25, 2018 22 23 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 committed Apr 27, 2018 24 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 committed Apr 25, 2018 25 26  \begin{figure}[ht]\centering  Dennis Müller committed Apr 27, 2018 27  \fbox{\includegraphics[width=\textwidth]{beautysource}}  Dennis Müller committed Apr 25, 2018 28 29 30 31  \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 committed Apr 25, 2018 32 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 committed Apr 25, 2018 33 34 35 36 37 38 39 \cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library. \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}  Dennis Müller committed Apr 28, 2018 40 \section{Inter-Library Viewfinding}\label{sec:across}  Dennis Müller committed Apr 26, 2018 41 42 43 44 45  We have so far assumed one fixed meta-theory for all theories involved; we will now discuss the situation when looking for views between theories in different libraries (and built on different foundations). 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 committed Apr 27, 2018 46  \item In many instances, the translations between two foundations is too complex to be discovered purely syntactically. In these cases we can provide arbitrary translations between theories, which are applied before computing the abstract syntax trees (e.g. alignment-based translations as in \cite{MRLR:alignments:17})  Dennis Müller committed Apr 28, 2018 47  \item We can do additional transformations before preprocessing theories, such as eliminating higher-order abstract syntax encodings or encoding-related redundant information (such as the type of a typed equality, which in the presence of subtyping can be different from the types of both sides of an equation), or elaborating abbreviations/definitions.  Dennis Müller committed Apr 26, 2018 48 49 \end{itemize}  Dennis Müller committed Apr 28, 2018 50 \subsection{Normalization in PVS}\label{sec:normalizeinter}  Dennis Müller committed Apr 26, 2018 51 52 53 54  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. We currently use the following approaches to preprocessing theories: \begin{itemize} \item Free variables in a term, often occurences of theory parameters as e.g. used extensively in the PVS system, are replaced by holes.  Dennis Müller committed Apr 28, 2018 55  \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 committed Apr 27, 2018 56 57  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 committed Apr 26, 2018 58 59  \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 committed Apr 27, 2018 60 61 62 63 64  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 committed Apr 26, 2018 65 66 67 68 \end{itemize} \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 committed Apr 25, 2018 69   Dennis Müller committed Apr 25, 2018 70 71 \begin{figure}[ht]\centering \fbox{\includegraphics[width=\textwidth]{pvs}}  Dennis Müller committed Apr 25, 2018 72 \caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}  Dennis Müller committed Apr 26, 2018 73 \end{figure}  Dennis Müller committed Apr 26, 2018 74 75 \ednote{8 results for NASA, but NASA doesn't work in jEdit because of limited memory}  Dennis Müller committed Apr 28, 2018 76 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.