Commit 6671a767 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

carefully re-read, eliminating duplicates

parent c08f8c1e
We present a general MKM utility that given a \MMT theory and an \MMT library $\cL$ finds
partial and total views into $\cL$.
Such a view finder can be used to drive various MKM applications ranging from theory classification to library merging and refactoring.
We have presented the first and last of these and show that they are feasible. For the applications discussed but unrealized in this paper, we mainly need to determine the right application context and user interface.
The theory discovery use case described in Sect.~\ref{sec:usecase} is mostly desirable in a setting where a user is actively writing or editing a theory, so the integration in jEdit is sensible.
However, the inter-library view finding would be a lot more useful in a theory exploration setting, such as when browsing available archives on MathHub~\cite{mathhub} or in the graph viewer integrated in \mmt ~\cite{RupKohMue:fitgv17}.
\paragraph{Future Work}
The current view finder is already efficient enough for the limited libraries we used for testing.
......@@ -10,16 +11,12 @@ The latter will be important for the library refactoring and merging application
As such library-scale operations will have to be run together with theory flattening to a fixed point and re-run upon every addition to the library, it will be important to integrate them with the \MMT build system and change management processes~\cite{am:doceng10,iancu:msc}.
\paragraph{Enabled Applications}
\ednote{FR: I've moved this here from Sect. 5. I suspect it should be reread carefully.}
Our work enables a number of advanced applications.
Maybe surprisingly, a major bottleneck here concerns less the algorithm or software design challenges but user interfaces.
The theory discovery use case described in Sect.~\ref{sec:usecase} is mostly desirable in a setting where a user is actively writing or editing a theory, so the integration in jEdit is sensible.
However, the inter-library view finding would be a lot more useful in a theory exploration setting, such as when browsing available archives on MathHub~\cite{mathhub} or in the graph viewer integrated in \mmt ~\cite{RupKohMue:fitgv17}.
Additional specialized user interfaces would enable or improve the following use cases:
Maybe surprisingly, a major bottleneck here concerns less the algorithm or software design
challenges but user interfaces and determining the right application context.
\begin{compactitem}
\item \textbf{Model-/Countermodel Finding:} If the codomain of a view is a theory representing a specific model, it would tell her that those are \emph{examples} of her abstract theory.
Furthermore, partial views -- especially those that are total on some included theory -- could be insightful \emph{counterexamples}.
\item \textbf{Model-/Countermodel Finding:} If the codomain of a view is a theory representing a specific model, it would tell Jane that those are \emph{examples} of her abstract theory.
Furthermore, partial views -- especially those that are total on some included theory -- could lead to insightful \emph{counterexamples}.
%
\item \textbf{Library Refactoring:} Given that the view finder looks for \emph{partial} views, we can use it to find natural extensions of a starting theory. Imagine Jane removing the last of her axioms for ``beautiful sets'' -- the other axioms (disregarding finitude of her sets) would allow her to find e.g. both Matroids and \emph{Ideals}, which would suggest to her to refactor her library accordingly.
Additionally, \emph{surjective} partial views would inform her, that her theory would probably better be refactored as an extension of the codomain, which would allow her to use all theorems and definitions therein.
......@@ -30,8 +27,6 @@ Additionally, \emph{surjective} partial views would inform her, that her theory
This would allow for e.g. discovering and importing theorems and useful definitions from some other library -- which on the basis of our encodings can be done directly by the view finder.
A useful interface might specifically prioritize views into theories on top of which there are many theorems and definitions that have been discovered.
\end{compactitem}
For some of these use cases it would be advantageous to look for views \emph{into} our working theory instead.
Note that even though the algorithm is in principle symmetric, some aspects often depend on the direction --- e.g. how we preprocess the theories, which constants we use as starting points or how we aggregate and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
\paragraph{Acknowledgments}
......@@ -46,4 +41,4 @@ Open Archive for Formalizations (KO 2428/13-1).
%%% TeX-master: "paper"
%%% End:
% LocalWords: unrealized am:doceng10,iancu:msc Formalizations
% LocalWords: unrealized am:doceng10,iancu:msc Formalizations sec:usecase mathhub RupKohMue:fitgv17 compactitem textbf Countermodel emph Generalization generalization normalization prioritize sec:algparams sec:normalizeintra sec:normalizeinter
......@@ -12,21 +12,21 @@ the following properties $Q$:
\begin{compactenum}
\item the empty set is beautiful over $\cB$
\item every subset of a beautiful set is beautiful over $\cB$
\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
\item If $A$ and $B$ are beautiful over $\cB$ and $A$ has more elements than $B$, then
there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
\end{compactenum}
To see what is known about beautiful sets, she types these three conditions into a theory
To see what is known about beautiful subsets, she types these three conditions into a theory
classifier, which computes any theories in a library $\cL$ that match these (after a
suitable renaming). In our case, Jane learns that her ``beautiful sets'' correspond to
the well-known structure of matroids~\cite{wikipedia:matroid}, so she can directly apply
matroid theory to her problems.
In extended use cases, a theory classifier find theories that share significant structure
with $Q$, so that we can formalize $Q$ with modularly with minimal effort. Say Jane was
with $Q$, so that Jane can formalize $Q$ modularly with minimal effort. Say Jane was
interested in ``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition,
then she could just contribute a theory that extends \textsf{matroid} by a formalization
of the fourth condition -- and maybe rethink the name.
% \item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
of the fourth condition -- and maybe rethink the name.
% \item use existing views in $\cL$ (compositions of views are views) to give Jane more
% information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
% form a generalization of the notion of linear independence from linear algebra.
% \end{compactitem}
......@@ -56,15 +56,12 @@ of the fourth condition -- and maybe rethink the name.
% \caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
% \end{figure}
We reduce the theory classification problem to that of finding theory morphisms (views)
between \MMT theories. $\cL$: given a query theory $Q$, the view finder computes all
(total) views from $Q$ into a library $\cL$, and returns presentations of target theories
and the assignments made by the views.
In this paper we reduce the theory classification problem to that of finding theory morphisms (views) between \MMT theories in a library $\cL$: given a query theory $Q$, the view finder computes all (total) views from $Q$ into $\cL$ and returns presentations of target theories and the assignments made by the views.
\paragraph{Related Work}
Existing systems have so far only worked with explicitly given views, e.g., in IMPS \cite{imps} or Isabelle \cite{isabelle}.
Automatically and systematically searching for new views was first undertaken in \cite{NorKoh:efnrsmk07} in 2006.
However, at that time no large corpora of formalized mathematics were available in standardized formats that would have allowed easily testing the ideas in large corpora.
However, at that time no large corpora of formalized mathematics were available in standardized formats that would have allowed easily testing the ideas in practice.
This situation has changed since then as multiple such exports have become available.
In particular, we have developed the MMT language \cite{RK:mmt:10} and the concrete syntax of the OMDoc XML format \cite{omdoc} as a uniform representation language for such corpora.
......@@ -86,13 +83,13 @@ separating the term into a hashed representation of its abstract syntax tree (wh
as a fast plausibility check for pre-selecting matching candidates) and the list of symbol
occurrences in the term, into which the algorithm recurses.
Secondly, we apply this view finder in a concrete case study: In the first, we start with an abstract theory and try to figure out if it already exists in the same library -- the use case mention above. In the second example, we write down a simple theory of commutative operators in one language to find all commutative operators in another library based on a different language.\ednote{FR: this paragraph is vague; also we only have one case study, do we?}
Secondly, we apply this view finder in two case studies: In the first, we start with an abstract theory and try to figure out if it already exists \emph{in the same library} -- the use case mention above. In the second example, we write down a simple theory of commutative operators in one language to find all commutative operators in \emph{another library based on a different foundation}.
\paragraph{Overview}
In Section~\ref{sec:prelim}, we revise the basics of MMT and views.
Section~\ref{sec:viewfinder} presents the view finding algorithm restricted to the intra-library case and showcases it for the theory classification use case.
In Section~\ref{sec:across}, we extend the algorithm to inter-library view finding discuss results of applying it to the PVS/NASA library.
Section~\ref{sec:appl} discusses additional applications and Section~\ref{sec:concl} concludes the paper.
Section~\ref{sec:concl} concludes the paper and discusses additional applications.
%%% Local Variables:
%%% mode: latex
......
......@@ -6,6 +6,16 @@ In the simplest case, \textbf{theories} $\Sigma$ are lists of \textbf{constant d
Naturally, $E$ must be subject to some type system (which MMT is also parametric in), but the details of this are not critical for our purposes here.
We say that $\Sigma'$ includes $\Sigma$ if it contains every constant declaration of $\Sigma$.
\begin{figure}[htb]\centering
\begin{tabular}{|l|l|l|}\hline
\multicolumn{3}{|c|}{meta-theory: a fixed theory $M$}\\\hline
& Theory $\Sigma$ & iew $\sigma:\Sigma\to\Sigma'$ \\\hline
set of & typed constant declarations $c:E$ & assignments $c\mapsto E'$ \\
$\Sigma$-expressions $E$ & formed from $M$- and $\Sigma$-constants & mapped to $\Sigma'$ expressions \\\hline
\end{tabular}
\caption{Overview of MMT Concepts}\label{fig:mmt}
\end{figure}
Correspondingly, a \textbf{view} $\sigma:\Sigma\to\Sigma'$ is a list of \textbf{assignments} $c\mapsto e'$ of $\Sigma'$-expressions $e'$ to $\Sigma$-constants $c$.
To be well-typed, $\sigma$ must preserve typing, i.e., we must have $\vdash_{\Sigma'}e':\ov{\sigma}(E)$.
Here $\ov{\sigma}$ is the homomorphic extension of $\sigma$, i.e., the map of $\Sigma$-expressions to $\Sigma'$-expressions that substitutes every occurrence of a $\Sigma'$-constant with the $\Sigma'$-expression assigned by $\sigma$.
......@@ -27,22 +37,6 @@ That allows $L$ to concisely define the syntax and inference system of HOL Light
However, for our purposes, it suffices to say that the meta-theory is some fixed theory relative to which all concepts are defined.
Thus, we assume that $\Sigma$ and $\Sigma'$ have the same meta-theory $M$, and that $\ov{\sigma}$ maps all $M$-constants to themselves.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{|l|l|l|}
\hline
\multicolumn{3}{|c|}{meta-theory: a fixed theory $M$}\\
%\hline
\hline
& Theory $\Sigma$ & iew $\sigma:\Sigma\to\Sigma'$ \\
\hline
set of & typed constant declarations $c:E$ & assignments $c\mapsto E'$ \\
$\Sigma$-expressions $E$ & formed from $M$- and $\Sigma$-constants & mapped to $\Sigma'$ expressions \\
\hline
\end{tabular}
\end{center}
\caption{Overview of MMT Concepts}\label{fig:mmt}
\end{figure}
\begin{wrapfigure}r{4.2cm}\vspace*{-2em}
\begin{tabular}{l@{\quad}c@{\quad}l}
......@@ -60,13 +54,12 @@ Complex expressions are of the form $\ombind{o}{x_1:t_1,\ldots,x_m:t_m}{a_1,\ldo
\end{compactitem}
The bound variable context may be empty, and we write $\oma{o}{\vec{a}}$ instead of $\ombind{o}{\cdot}{\vec{a}}$.
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.
\subseteq x \Rightarrow \cn{beautiful}(y)$ would instead 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}}}\]
%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
%\[ \ombind{\forall}{s : \oma{\cn{set}}{X},t : \oma{\cn{set}}{X}}{\oma{\Rightarrow}{\oma{\wedge}{\oma{\cn{beautiful}}{s},\oma{\subseteq}{t,s}},\oma{\cn{beautiful}}{t}}} \]
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 provides a module system 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$.
Defined constants can be eliminated by definition expansion.
......
......@@ -12,6 +12,7 @@ PVS~\cite{pvs} is a proof assistant under active development based on a higher-o
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}.
In \cite{KMOR:pvs:17}, we represent PVS as a meta-theory in MMT and implemented a translator that transforms both libraries into MMT format.
\begin{oldpart}{MK: this sounds like a left-over from the time we had a PVS->HOL-Light use case. I think this can just be eft out. or reduce to the last sentence and leave out the paragrpah}
\paragraph{Formula Normalization}
Naturally advanced features of the PVS type system such as predicate subtyping, record types, inductive types will not be part of views from MitM, which does not have corresponding features.
Therefore, our view finder can mostly ignore them.
......@@ -19,9 +20,10 @@ Therefore, our view finder can mostly ignore them.
Instead, we only have to normalize PVS formulas to the extent that they use logical features that correspond to those of MitM.
This is particular the basic higher-order logic.
Thus, we use a meta-view that embeds MitM's higher-order logic into PVS's higher-order logic and make sure that we normalize PVS-formulas in the same way as MitM-formulas.
\end{oldpart}
\paragraph{Theory Structure Normalization}
However, PVS's complex and prevalently used parametric theories critically affect view finding because it affects the structure of theories.
PVS's complex and prevalently used parametric theories critically affect view finding because they affect the structure of theories.
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 of groups, and includes the theory \cn{monoid\_def} with the same parameters, and then declares the axioms for a group in terms of these parameters.
Without special treatment, we could only find views from/into libraries that use the same theory structure.
......@@ -32,7 +34,7 @@ We have investigated three approaches of handling parametric theories:
However, because practical search problems often do not require exact results, even returning all potential views can be useful.
\item \emph{Covariant elimination:} We treat theory parameters as if they were constants declared in the body.
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.
This works well in the common case a parametric theory is not used with two different instantiations in the same context.
This works well in the common case where a parametric theory is not used with two different instantiations in the same context.
\item \emph{Contravariant elimination:}
The theory parameters are treated as if they were bound separately for every constant in the body of the theory.
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})$.
......@@ -41,20 +43,24 @@ We have investigated three approaches of handling parametric theories:
But it makes finding interesting views the least likely because it is the most sensitive to the modular structure of individual theories.
\end{compactenum}
We have implemented the first two approaches.
The first it is the most straightforward but it leads to many false positives and false negatives.
We have found the second approach to be the most useful for inter-library search since it most closely corresponds to simple formalizations of abstract theories in other libraries.
We have implemented the first two approaches.
The first is the most straightforward but it leads to many false positives and false negatives.
We have found the second approach to be the most useful for inter-library search since it most closely corresponds to simple formalizations of abstract theories in other libraries.
% 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 will be our method of choice when investigating \emph{intra}-library views of PVS/NASA in future work.
The third approach will be our method of choice when investigating \emph{intra}-library views of PVS/NASA in future work.
% would turn every occurrence 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.
\subsection{Implementation}\label{sec:pvs}
\ednote{FR: this should be reread; I didn't have time to finish it up}
As a first 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 parameters).
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\end{figure}
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 views.
We have applied the first two simple and the covariant approach described above.
We wrote 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}.
To evaluate the approaches to theory parameters we used a simple theory of monoids in the MitM foundation and the theory of Monoids in the NASA library as domains for viewfinding with the whole NASA library as target using simple and covariant approaches. The results are summarized in Figure \ref{fig:pvsresults}.
\begin{figure}[ht]\centering
\begin{tabular}{l | c || c | c}
......@@ -67,22 +73,11 @@ The results are summarized in Figure \ref{fig:pvsresults}.
\caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}
\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 views lead to fuller (one total) and less spurious views.
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 additional requirements lead to fuller (one total) and less spurious views.
With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.
\ednote{FR: give example of an interesting view we found}
\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 parameters).
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\end{figure}
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 views.
\ednote{FR: This second use case looks good, but might deserve some more emphasis, e.g., how many operators were found}
%%% Local Variables:
%%% mode: latex
%%% eval: (set-fill-column 5000)
......
Let $C$ be a corpus of theories with the same fixed meta-theory $M$.
We call the problem of finding theory views between theories of $C$ the \defemph{view finding problem} and an algorithm that solves it a \defemph{view finder}.
Note that a view finder is sufficient to solve the theory classification use case from the introduction:
Jane provides a $M$-theory $Q$ of beautiful sets, the view finder computes all (total) views from $Q$ into $C$, and returns presentations of target theories and the assignments made by the views.
Jane provides a $M$-theory $Q$ of beautiful sets, the view finder computes all (total) views from $Q$ into $C$.
\paragraph{Efficiency Considerations}
The cost of this problem quickly explodes.
......@@ -18,7 +17,7 @@ Thus, we can in principle enumerate and check all possible simple views in $C$.
But for large $C$, it quickly becomes important to do so in an efficient way that eliminates ill-typed or uninteresting views early on.
Thirdly, it is desirable to search for \emph{partial} views as well.
In fact, identifying refactoring potential is only possible if we find partial views: then we can refactor the involved theories in a way that yields a total view.
In fact, identifying refactoring potential in libraries is only possible if we find partial views: then we can refactor the involved theories in a way that yields a total view.
Moreover, many proof assistant libraries do not follow the little theories paradigm or do not employ any theory-like structuring mechanism at all.
These can only be represented as a single huge theory, in which case we have to search for partial views from this theory to itself.
While partial views can be reduced to and then checked like total ones, searching for partial views makes the number of possible views that must be checked much larger.
......@@ -41,22 +40,19 @@ The preprocessing phase computes for every constant declaration $c:E$ a normal f
Both steps are described below.
\paragraph{Normalization}
Normalization involves two steps.
Firstly, \textbf{MMT-level} normalization performs generic transformations that do not depend on the meta-theory $M$.
involves two steps: \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 views 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 views we can find.
Secondly, \textbf{meta-theory-level} normalization applies an $M$-specific normalization function.
\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:
However, because many practically important normalization steps are widely reusable, we provide a few building blocks, from which specific normalization functions can be composed. Skipping the details, these include:
\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.
\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 others are dropped, e.g. the type argument of an equality.
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}
......@@ -149,7 +145,7 @@ We define a view by starting with $\sigma=c\mapsto c'$ and recursively adding al
If the above algorithm succeeds, then $\sigma$ is a well-typed partial simple view from $\Sigma$ to $\Sigma'$.
\end{lemma}
\begin{example}\label{ex:beautifinite} Consider two constants $c,c'$ with types $\forall x:\cn{set},y:\cn{set}.\; \cn{beautiful}(x) \wedge y \subseteq x \Rightarrow \cn{beautiful}(y)$ and $\forall x:\cn{powerset},y:\cn{powerset}.\; \cn{finite}(x) \wedge y \subseteq x \Rightarrow \cn{finite}(y)$. Their syntax trees are
\begin{example}\label{ex:beautifinite} Consider two constants $c$ and $c'$ with types $\forall x:\cn{set},y:\cn{set}.\; \cn{beau}\-\cn{tiful}(x) \wedge y \subseteq x \Rightarrow \cn{beautiful}(y)$ and $\forall x:\cn{powerset},y:\cn{powerset}.\; \cn{finite}(x) \wedge y \subseteq x \Rightarrow \cn{finite}(y)$. Their syntax trees are
\[t=t'=\ombind{C_1}{C_2,C_3}{\oma{C_4}{\oma{C_5}{\oma{C_6}{V_2},\oma{C_7}{V_1,V_2}},\oma{C_8}{V_1}}}\]
\[ s=(\forall,\cn{set},\cn{set},\Rightarrow,\wedge,\cn{beautiful},\subseteq,\cn{beautiful})\]
\[ s'=(\forall,\cn{powerset},\cn{powerset},\Rightarrow,\wedge,\cn{finite},\subseteq,\cn{finite})\]
......@@ -159,7 +155,7 @@ Since $t=t'$, we set $c\mapsto c'$ and compare $s$ with $s'$, meaning we check (
To find all views from $\Sigma$ to $\Sigma'$, we first run the core algorithm on every pair of $\Sigma$-constants and $\Sigma'$-constants.
This usually does not yield big views yet.
For example, consider the typical case where theories contain some symbol declarations and some axioms, in which the symbols occur.
Then the core algorithm will only find views that map at most $1$ axiom.
Then the core algorithm will only find views that map at most one axiom.
Depending on what we intend to do with the results, we might prefer to consider them individually (e.g. to yield \emph{alignments} in the sense of \cite{KKMR:alignments:16}). But we can also use these small views as building blocks to construct larger, possibly total ones:
\begin{lemma}[Amalgamating Views]
......@@ -177,7 +173,7 @@ The union of compatible well-typed views 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 a few advanced features of our implementation to enhance scalability.
We now 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.
......@@ -210,24 +206,28 @@ If implemented naively, that would yield a quadratic blow-up in the number of vi
Instead, when running our algorithm on an entire library, we only consider views between theories that are not imported into other theories.
In an additional postprocessing phase, the domain and codomain of each found partial view $\sigma$ are adjusted to the minimal theories that make $\sigma$ well-typed.
\subsection{Implementation}\label{sec:usecase}
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{beautysource}}
\fbox{\includegraphics[width=0.7\textwidth]{results}}
\caption{``Beautiful Sets'' in MMT Surface Syntax and View Finder Results}\label{fig:use:source}
\caption{``Beautiful Sets'' in MMT Surface Syntax}\label{fig:use:source}
\end{figure}
\subsection{Implementation}\label{sec:usecase}
\begin{wrapfigure}r{.61\textwidth}\vspace*{-2em}
\fbox{\includegraphics[width=0.6\textwidth]{matroids}}\vspace*{-.5em}
\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.
\fbox{\includegraphics[width=0.6\textwidth]{results}}
\caption{Views found for ``Beautiful Sets''}\label{fig:use:results}\vspace*{-2em}
\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 views (within less than one second) and shows them (bottom of Figure~\ref{fig:use:source}).
\begin{wrapfigure}l{.61\textwidth}\vspace*{-2em}
\fbox{\includegraphics[width=0.6\textwidth]{matroids}}\vspace*{-.5em}
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}\vspace*{-1em}
\end{wrapfigure}
\noindent After choosing \cn{MitM/smglom}, the view finder finds two views (within less than one second) and shows them (Figure~\ref{fig:use:results}).
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}.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment