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. 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 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$. 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, $\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}
\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.
\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.
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 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-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})
@@ -29,7 +29,7 @@ Depending on $M$, this equality judgment may be undecidable and require theorem
\paragraph{Algorithm Overview}
A central motivation for our algorithm is that equality in $M$ can be soundly approximated very efficiently by using a normalization function on $M$-expressions.
This has the additional benefit that relatively little meta-theory-specific knowledge is needed, and all such knowledge is encapsulated in a single well-understood function.
Thus, we can implement theory morphism--search generically for arbitrary $M$.
This way we can implement theory morphism--search generically for arbitrary $M$.
Our algorithm consists of two steps.
First, we preprocess all constant declarations in $C$ with the goal of moving as much intelligence as possible into a step whose cost is linear in the size of $C$.
...
...
@@ -37,7 +37,7 @@ Then, we perform the morphism search on the optimized data structures produced b
\subsection{Preprocessing}
The preprocessing phase computes for every constant declaration $c:E$ a normal form $E'$ and then the long abstract syntax tree for$E'$.
The preprocessing phase computes for every constant declaration $c:E$ a normal form $E'$ and then efficiently stores the abstract syntax tree of $E'$.
Both steps are described below.
\paragraph{Normalization}
...
...
@@ -45,8 +45,40 @@ Normalization involves two steps.
Firstly, \textbf{MMT-level} normalization performs generic transformations that do not depend on the meta-theory $M$.
These include elaboration of structured theories and definition expansion, which we mentioned in Sect.~\ref{sec:prelim}.
Importantly, we do not fully eliminate defined constant declarations $c:E=e$ from a theory $\Sigma$: instead, we replace them with primitive constants $c:E$ and replace every occurrence of $c$ in other declarations with $e$.
If $\Sigma$ is the domain theory, we can simply ignore $c:E$ (because morphism do not have to provide an assignment to defined constants).
But if the $\Sigma$ is the codomain theory, retaining $c:E$ increases the number of morphisms we can find.
Secondly, \textbf{meta-theory-level} normalization applies an $M$-specific normalization function.
In general, we assume this normalization to be given as a black box.
However, because many practically important normalization steps are widely reusable, we provide a few building blocks, from which specific normalization functions can be composed.
We skip the details here and only mention a few of these building blocks:
\begin{compactenum}
\item Top-level universal quantifiers and implications are rewritten into the function space of the logical framework using the Curry-Howard correspondence.
\item The order of curried domains of function types is normalized as follows: first all dependent arguments types ordered by the first occurrence of the bound variables; then all non-dependent argument types $A$ ordered by the abstract syntax tree of $A$.
\item Implicit arguments, whose value is determined by the values of the other arguments, such as the type argument of an equality, are dropped.
This has the additional benefit or shrinking the abstract syntax trees and speeding up the search.
\item Equalities are normalized such that the left hand side has a smaller abstract syntax tree.
\end{compactenum}
Above multiple normalization steps make use of a total order on abstract syntax trees $(t,s)$.
We omit the details and only remark that we try to avoid using the names of the constants in $s$ in the definition of the order --- otherwise, declarations that could be matched by a morphism would be normalized differently.
Even when breaking ties between requires comparing two constants, we can first try to recursively compare the syntax trees of their types.
%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 accommodate 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. 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 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$. 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, $\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}
Secondly, \textbf{meta-theory-level} normalization applies an $M$-specific normalization function, which we assume as a black box for now and discuss further in Sect.~\ref{sec:preproc}.
\paragraph{Abstract Syntax Trees}
We define \textbf{abstract syntax trees} as pairs $(t,s)$ where $t$ is subject to the grammar
...
...
@@ -144,38 +176,63 @@ 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 scalability improvements.
\paragraph{Choice of Meta-Theory and Meta-Morphisms}
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:
%
%But often the library contains certain theories that represent concrete mathematical objects, e.g., the real numbers and constants for their operations.
%Most of the time, we want to fix those constants as well instead of finding morphisms that, e.g., map real addition to any other commutative binary operator anywhere in the library.
%But sometimes we do not want to fix them, e.g., if there are multiple axiomatizations of the real numbers that we want to refactor.
%
%Secondly, consider two libraries in logics $L$ and $L'$ between which we want to find inter-library morphisms.
%Here it makes sense to use only the logical framework used to define the two logics as the meta-theory.
%Moreover, if we have already found a partial morphism $m$ that maps, e.g., the propositional connectives of $L$ to those of $L'$, we can use $m$ as a \textbf{meta-morphism}.
%In that case, we are only looking for morphisms that extend $m$.
%
%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:} 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, 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}
\paragraph{Picking starting theories:} If we try to find morphisms between whole collections of theories, we can obviously disregard all theories that are already included in some other theory in our collections, since we work with a normalized (and dependency-closed) version of a theory. Consequently, by only using maximal theories we do not find any fewer morphisms but speed up the search significantly.
The above presentation is intentionally simple to convey the general idea.
In the sequel, we describe a few advanced features of our implementation to enhance scalability.
\paragraph{Caching Preprocessing Results}
Because the preprocessing performs normalization, it can be time-consuming.
Therefore, we allow for storing the preprocessing results to disk and reloading them in a later run.
\paragraph{Fixing the Meta-Theory}
We improve the preprocessing in a way that exploits the common meta-theory, which is meant to be fixed by every morphism.
All we have to do is, when building the abstract syntax trees $(t,s)$, to retain all references to constants of the meta-theory in $t$ instead of replacing them with numbers.
With this change, $s$ will never contain meta-theory constants, and the core algorithm will only find morphisms that fix all meta-theory constants.
Because $s$ is much shorter now, the morphism finding is much faster.
It is worth pointing out that the meta-theory is not always as fixed as one might think.
Often we want to consider to be part of the meta-theory certain constants that are defined early on in the library and then used widely.
In PVS, this makes sense, e.g., for all operations define in the Prelude library (the small library shipped with PVS).
Note that we still only have to cache one set of preprocessing results for each library: changes to the meta-theory only require minor adjustments to the abstract syntax trees without redoing the entire normalization.
\paragraph{Biasing the Core Algorithm}
The core algorithm starts with an assignment $c\mapsto c'$ and then recurses into constant that occur in the declarations of $c$ and $c'$.
This occurs-in relation typically splits the constants into layers.
A typical theory declares types, which then occur in the declarations of function symbols, which then occur in axioms.
Because morphism that only type and function symbols are rarely interesting (because they do not allow transporting non-trivial theorems), we always start with assignments where $c$ is an axiom.
%\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.
\paragraph{Exploiting Theory Structure}
Libraries are usually highly structured using imports between theories.
If $\Sigma$ is imported into $\Sigma'$, then the set of partial morphisms out of $\Sigma'$ is a superset of the set of partial morphisms out of $\Sigma$.
If implemented naively, that would yield a quadratic blow-up in the number of morphism to consider.
Instead, when running our algorithm on an entire library, we only consider morphism between theories that are not imported into other theories.
In an additional postprocessing phase, the domain and codomain of each found partial morphism $\sigma$ are adjusted to the minimal theories that make $\sigma$ well-typed.
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}\vspace*{-1em}
\end{wrapfigure}
We have implemented our view finder algorithm in the MMT system.
A screenshot of Jane's theory of beautiful sets is given in Figure \ref{fig:use:source}.
Right-clicking anywhere within the theory allows Jane to select \cn{MMT}$\to$\cn{Find}\cn{Views\ to...}$\to$\cn{MitM/smglom}.
The latter menu offers a choice of known libraries in which the view finder should look for codomain theories; \cn{MitM/smglom} is the Math-in-the-Middle library based that we have developed \cite{ODK:mitm:16} to describe the common knowledge used in various CICM systems.
After choosing \cn{MitM/smglom}, the view finder finds two morphisms (within less than one second) and shows them (bottom of Figure~\ref{fig:use:source}).
The first of these ($\cn{View0}$) has a theory for matroids as its codomain, which is given in Figure \ref{fig:use:target}.
Inspecting that theory and the assignments in the view, we see that it indeed represents the well-known correspondence between beautiful sets and matroids.
%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.
\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.
