@@ -46,12 +46,14 @@ $\Sigma$-expressions $E$ & formed from $M$- and $\Sigma$-constants & mapped to
\caption{Overview of MMT Concepts}\label{fig:mmt}
\end{figure}
It remains to define the exact syntax of expressions:
\begin{ctabular}{l@{\quad}c@{\quad}l}
\begin{wrapfigure}r{4.2cm}\vspace*{-2em}
\begin{tabular}{l@{\quad}c@{\quad}l}
$\Gamma$&$::=$&$(x:E)^\ast$\\
$E$&$::=$&$c \mid x \mid\ombind{E}{\Gamma}{E^+}$\\
\end{ctabular}
Here $c$ refers to constants (of the meta-theory or previously declared in the current theory) and $x$ refers to bound variables.
\end{tabular}\vspace*{-2em}
\end{wrapfigure}
It remains to define the exact syntax of expressions.
In the grammar on the right $c$ refers to constants (of the meta-theory or previously declared in the current theory) and $x$ refers to bound variables.
Complex expressions are of the form $\ombind{o}{x_1:t_1,\ldots,x_m:t_m}{a_1,\ldots,a_n}$, where
\begin{compactitem}
\item$o$ is the operator that forms the complex expression,
...
...
@@ -59,11 +61,12 @@ Complex expressions are of the form $\ombind{o}{x_1:t_1,\ldots,x_m:t_m}{a_1,\ldo
\item$a_i$ is an argument of $o$
\end{compactitem}
The bound variable context may be empty, and we write $\oma{o}{\vec{a}}$ instead of $\ombind{o}{\cdot}{\vec{a}}$.
\begin{newpart}{DM}
For example, the axiom $\forall x:\cn{set},y:\cn{set}.\;\cn{beautiful}(x)\wedge y \subseteq x \Rightarrow\cn{beautiful}(y)$ would be written as $\ombind{\forall}{x:\cn{set},y:\cn{set}}{\oma{\Rightarrow}{\oma{\wedge}{\oma{\cn{beautiful}}{x},\oma{\subseteq}{y,x}},\oma{\cn{beautiful}}{y}}}$ instead.
For example, the axiom $\forall x:\cn{set},y:\cn{set}.\;\cn{beautiful}(x)\wedge y
\subseteq x \Rightarrow\cn{beautiful}(y)$ would be written as \[\ombind{\forall}{x:\cn{set},y:\cn{set}}{\oma{\Rightarrow}{\oma{\wedge}{\oma{\cn{beautiful}}{x},\oma{\subseteq}{y,x}},\oma{\cn{beautiful}}{y}}}\]
instead.
%For example, the second axiom ``Every subset of a beautiful set is beautiful'' (i.e. the term $\forall s,t : \cn{set\ }X.\;\cn{beautiful}(s)\wedge t \subseteq s \Rightarrow \cn{beautiful}(t)$) would be written as
Finally, we remark on a few additional features of the MMT language that are important for large-scale case studies but not critical to understand the basic intuitions of results.
MMT provides a module systems that allows theories to instantiate and import each other. The module system is conservative: every theory can be elaborated into one that only declares constants.
MMT constants may carry an optional definiens, in which case we write $c:E=e$.
...
...
@@ -145,25 +148,23 @@ As part of the OAF project~\cite{OAFproject:on}, we have imported several proof
The resulting formalizations are then used as meta-theory for imports of the libraries of the system under consideration. This results in a theory graph as in Figure \ref{fig:oaf}.
\begin{figure}
\begin{figure}[ht]\centering
\begin{tikzpicture}
\node (MMT) at (2,2.5) {MMT};
\draw[fill=yellow!60] (2,1) ellipse (1.5cm and .6cm);
\node[color=yellow] at (-3.3,1) {Logical Frameworks};
\draw[fill=orange!40] (2,1) ellipse (1.5cm and .6cm);
\node[color=orange] at (-3.3,1) {Logical Frameworks};
\node (L) at (1,1) {LF};
\node (Lx) at (3,1) {LF+X};
\draw[arrow](MMT) -- (L);
\draw[arrow](MMT) -- (Lx);
\draw[arrow](L) -- (Lx);
\draw[fill=red!60] (2,-.5) ellipse (3.2cm and .6cm);
\draw[fill=red!40] (2,-.5) ellipse (3.2cm and .6cm);
\node[color=red] at (-3.3,-.5) {Foundations};
\node at (2,-.7) {\ldots};
\draw[fill=blue!60] (0,-2.25) ellipse (1.9cm and .8cm);
\draw[fill=blue!40] (0,-2.25) ellipse (1.9cm and .8cm);
\node (H) at (0,-.5) {HOL Light};
\node[color=blue!80] at (-3.5,-2) {HOL Light library};
...
...
@@ -175,7 +176,7 @@ The resulting formalizations are then used as meta-theory for imports of the lib
\draw[arrow](H) -- (A);
\draw[arrow](B) -- (A);
\draw[fill=olive] (4,-2.25) ellipse (1.9cm and .8cm);
\draw[fill=olive!40] (4,-2.25) ellipse (1.9cm and .8cm);
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 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.
\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. These can 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}
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:
The common logical framework LF 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:
\begin{itemize}
\item Free variables in a term are replaced by holes.
\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 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$. We arbitrarily normalize to the former.
\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 Typed equalities are transformed to untyped ones; again getting rid of the redundant type argument of the equality. For example, $\oma{\cn{equals}}{\mathbb N,2,1+1}$ becomes $\oma{\cn{equals}}{2,1+1}$, allowing to match the same equation on e.g. $\mathbb{R}$.
\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}
The view finder 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
is based on the (basic higher-order logic) foundation of the Math-in-the-Middle library (\cite{ODK:mitm:16} developed natively in MMT.
The view finder 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 is based on the (basic higher-order logic) foundation of the Math-in-the-Middle library (\cite{ODK:mitm:16} developed natively in MMT.
\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the View Finder}\label{fig:use:source}
\caption{``Beautiful Sets'' in MMT Surface Syntax and View Finder Results}\label{fig:use:source}
\end{figure}
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
\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}\vspace*{-1em}
\end{wrapfigure}
Right-clicking anywhere within the theory allows Jane to select \cn{MMT}$\to$\cn{Find}\cn{Views\ to...}$\to$\cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) about two morphisms, the most promising of which points to the theory \cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.
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.
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.
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).
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:
We now generalize to view-finding between theories in different libraries (and built on different foundations and meta-theories). 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:
\begin{itemize}
\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 In many instances, the translations between two foundations is too complex to be discovered purely syntactically. In these cases we can provide arbitrary meta-morphisms between theories\ednote{MK: starting alignments?} -- 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.
\end{itemize}
\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 idiosyncrasies, best practices or widely used features; finding an ideal normalization method is a correspondingly difficult domain-specific problem.
...
...
@@ -67,38 +56,27 @@ In practice, theory parameters are often used in PVS for the signature of an abs
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:
\begin{enumerate}
\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.
\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.
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 occurrences 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 passed on to includes with the same arguments without additional tranformations.
We have implemented the first two approaches. The first it is the most straight-forward but it lead to many false positives and negatives. 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.
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.
\paragraph{}Additionally to the theory parameter related normalization, we use the following techniques:
Additionally to the theory parameter related normalization, we use the following techniques:
\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.
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).\]
For example, $f(\langle a, b\rangle)$ becomes $f(a,b)$ and $4=\lambda(n,m) : \mathbb N \times\mathbb N .\; n + m$ becomes $f =\lambda n : \mathbb N.\;\lambda m : \mathbb N .\; n + m$.
\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.
For example, the apply-operator in the PVS meta-theory has the LF-type
For example, the apply-operator in the PVS meta-theory has the LF-type
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}$.
Hence every function application 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.
\end{itemize}
\end{newpart}
\subsection{Implementation}\label{sec:pvs}
...
...
@@ -116,11 +94,9 @@ We have tried the first two approaches regarding theory parameters -- i.e. the s
\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 more requirements of each simple morphism lead to fuller (one total) and less spurious morphisms.
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).
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).
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
...
...
@@ -142,3 +118,4 @@ This example also hints at a way to iteratively improve the results of the view
@@ -144,16 +144,12 @@ The union of compatible well-typed morphisms is again well-typed.
\subsection{Optimizations}\label{sec:algparams}
The above presentation is intentionally simple to convey the general idea.
In the sequel, we describe several improvements that we have implemented to be scalable.
The above presentation is intentionally simple to convey the general idea. In the sequel,
we describe several scalability improvements.
\paragraph{Choice of Meta-Theory and Meta-Morphisms}
The above descriptions treats meta-theory constants like any other constant.
As such it finds also morphisms that do not fix the meta-theory.
Our implementation extends our algorithm so that a meta-theory is fixed.
Our implementation extends our algorithm so that a meta-theory is fixed, since we are only interested in domain-morphisms in practice.
All we have to do is when building the abstract syntax trees to retain all references to constants of the meta-theory instead of replacing them with numbers.
%Firstly, consider a library of theories in logic $L$ in which we want to find intra-library morphisms.
%At first glance, the meta-theory should consist of $L$ and the logical framework used to define $L$ (if any).
%Therefore, our algorithm allows fixing a meta-theory:
...
...
@@ -169,12 +165,11 @@ All we have to do is when building the abstract syntax trees to retain all refer
%
%That can be useful because it lets us use the same preprocessing result even if we flexibly change the meta-theory.
%Changing the meta-theory happens more often than one might think, and we present two examples.
The symbols will hence be encoded in the component $t$ instead of the list $s$. This will not only exclude spurious matches, but also reduce the number of plausible matches and consequently speed up the algorithm.
\paragraph{Picking starting pairs:}Note, that we will still find many spurious matches if executed in its general form. The reason being that (for example) all atomic types match each other, as will all binary operators etc. Most of these results will not be interesting. Furthermore, since the algorithm needs to recurse into the lists $s$, many potential matches will need to be checked repeatedly. Both problems can be massively reduced by selecting specific pairs of encodings as \emph{starting pairs} for the algorithm, so that the majority of matching constants will only be considered if the algorithm runs into them during recursing. Potential useful starting points are:
\paragraph{Picking starting pairs:}The core algorithm still finds many spurious matches, as it (for example) matches all atomic types match each other, as will all binary operators etc. Most of these results will not be interesting. Furthermore, since the algorithm needs to recurse into the lists $s$, many potential matches will need to be checked repeatedly. Both problems can be massively reduced by selecting specific pairs of encodings as \emph{starting pairs} for the algorithm, so that the majority of matching constants will only be considered if the algorithm runs into them during recursing. Potential useful starting points are:
\begin{itemize}
\item\emph{Axioms:} Since we are mostly interested in matching constants that share the same mathematical properties, by using axioms as starting point we can ensure that the algorithm only matches constants that have at least one (axiomatic) property in common (e.g. only commutative, or associative operators).
\item\emph{Axioms:} Since we are mostly interested in matching constants that share the same mathematical properties, axioms as starting points ensure that the algorithm only matches constants that have at least one (axiomatic) property in common (e.g. only commutative, or associative operators).
\item\emph{The length of $s$ in the short abstract syntax tree:} By choosing a minimal length for $s$, we can guarantee that only morphisms will be produced that relate a minimal number of distinct constants.
\end{itemize}
...
...
@@ -183,7 +178,7 @@ The symbols will hence be encoded in the component $t$ instead of the list $s$.
\paragraph{Storing Encodings} Finally, for computing the encodings of a theory we only need to know the symbols to be fixed in the component $t$ of an abstract syntax tree, for which only the meta-theories of the theories are relevant. They also determine the specific preprocessings and translations we want to likely use. Since there is only a small number of meta-theories involved that are relevant in practice, we can store and retrieve the encodings for the most important situations. Since computing the encodings (as well as sorting the theories in a library by their dependencies) is the most expensive part of the algorithm, this -- once computed and stored -- makes the view finding process itself rather efficient.
