viewfinder.tex 22 KB
Newer Older
Michael Kohlhase's avatar
Michael Kohlhase committed
1
Let $C$ be a corpus of theories with the same fixed meta-theory $M$.
Dennis Müller's avatar
Dennis Müller committed
2
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}. 
Florian Rabe's avatar
Florian Rabe committed
3

Michael Kohlhase's avatar
Michael Kohlhase committed
4
Note that a view finder is sufficient to solve the theory classification use case from the introduction: 
Dennis Müller's avatar
Dennis Müller committed
5
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.
Florian Rabe's avatar
Florian Rabe committed
6

Florian Rabe's avatar
Florian Rabe committed
7
\paragraph{Efficiency Considerations}
Michael Kohlhase's avatar
Michael Kohlhase committed
8
The cost of this problem quickly explodes.
Dennis Müller's avatar
Dennis Müller committed
9
10
11
First of all, it is advisable to restrict attention to simple views.
Eventually we want to search for arbitrary views as well.
But that problem is massively harder because it subsumes theorem proving: a view from $\Sigma$ to $\Sigma'$ maps $\Sigma$-axioms to $\Sigma'$-proofs, i.e., searching for a view requires searching for proofs.
Florian Rabe's avatar
Florian Rabe committed
12
13

Secondly, if $C$ has $n$ theories, we have $n^2$ pairs of theories between which to search.
Dennis Müller's avatar
Dennis Müller committed
14
15
16
17
18
19
20
21
(It is exactly $n^2$ because the direction matters, and even views from a theory to itself are interesting.)
Moreover, for two theories with $m$ and $n$ constants, there are $n^m$ possible simple views.
(It is exactly $n^m$ because views may map different constants to the same one.)
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.
Florian Rabe's avatar
Florian Rabe committed
22
Moreover, many proof assistant libraries do not follow the little theories paradigm or do not employ any theory-like structuring mechanism at all.
Dennis Müller's avatar
Dennis Müller committed
23
24
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.
Florian Rabe's avatar
Florian Rabe committed
25

Dennis Müller's avatar
Dennis Müller committed
26
Finally, even for a simple view, checking reduces to a set of equality constraints, namely the constraints $\vdash_{\Sigma'}\ov{\sigma}(E)=E'$ for the type-preservation condition.
Florian Rabe's avatar
Florian Rabe committed
27
28
Depending on $M$, this equality judgment may be undecidable and require theorem proving.

Florian Rabe's avatar
Florian Rabe committed
29
\paragraph{Algorithm Overview}
Florian Rabe's avatar
Florian Rabe committed
30
31
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.
Dennis Müller's avatar
Dennis Müller committed
32
This way we can implement view--search generically for arbitrary $M$.
Florian Rabe's avatar
Florian Rabe committed
33
34
35

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$.
Dennis Müller's avatar
Dennis Müller committed
36
Then, we perform the view search on the optimized data structures produced by the first step.
Florian Rabe's avatar
Florian Rabe committed
37
38
39

\subsection{Preprocessing}

Florian Rabe's avatar
Florian Rabe committed
40
The preprocessing phase computes for every constant declaration $c:E$ a normal form $E'$ and then efficiently stores the abstract syntax tree of $E'$.
Florian Rabe's avatar
Florian Rabe committed
41
42
43
Both steps are described below.

\paragraph{Normalization}
Florian Rabe's avatar
Florian Rabe committed
44
45
46
47
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}.
Florian Rabe's avatar
Florian Rabe committed
48
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$.
Dennis Müller's avatar
Dennis Müller committed
49
50
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.
Florian Rabe's avatar
Florian Rabe committed
51
52
53
54
55
56
57
58
59
60
61
62
63

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)$.
Dennis Müller's avatar
Dennis Müller committed
64
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 view would be normalized differently.
Florian Rabe's avatar
Florian Rabe committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
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}
Florian Rabe's avatar
Florian Rabe committed
81

Florian Rabe's avatar
Florian Rabe committed
82
83
84

\paragraph{Abstract Syntax Trees}
We define \textbf{abstract syntax trees} as pairs $(t,s)$ where $t$ is subject to the grammar
Dennis Müller's avatar
Dennis Müller committed
85
 \[t ::= C_{Nat} \mid V_{Nat} \mid \ombind{t}{t^+}{t^+}\]
Florian Rabe's avatar
Florian Rabe committed
86
(where $Nat$ is a non-terminal for natural numbers) and $s$ is a list of constant names.
Dennis Müller's avatar
Dennis Müller committed
87
We obtain an abstract syntax tree from an MMT expression $E$ by (i) switching to de-Bruijn representation of bound variables and (ii) replacing all occurrences of constants with $C_i$ in such a way that every $C_i$ refers to the $i$-th element of $s$.
Florian Rabe's avatar
Florian Rabe committed
88

Dennis Müller's avatar
Dennis Müller committed
89
Abstract syntax trees have the nice property that they commute with the application of simple views $\sigma$:
Florian Rabe's avatar
Florian Rabe committed
90
91
92
If $(t,s)$ represents $E$, then $\sigma(E)$ is represented by $(t,s')$ where $s'$ arises from $s$ by replacing every constant with its $\sigma$-assignment.

The above does not completely specify $i$ and $s$ yet, and there are several possible canonical choices among the abstract syntax trees representing the same expression.
Dennis Müller's avatar
Dennis Müller committed
93
The trade-off is subtle because we want to make it easy to both identify and check views later on.
Dennis Müller's avatar
Dennis Müller committed
94
We call $(t,s)$ the \textbf{long} abstract syntax tree for $E$ if $C_i$ replaces the $i$-th occurrence of a constant in $E$ when $E$ is read in left-to-right order.
Florian Rabe's avatar
Florian Rabe committed
95
In particular, the long tree does not merge duplicate occurrences of the same constant into the same number.
Dennis Müller's avatar
Dennis Müller committed
96
The \textbf{short} abstract syntax tree for $E$ arises from the long one by removing all duplicates from $s$ and replacing the $C_i$ accordingly.
Florian Rabe's avatar
Florian Rabe committed
97

Florian Rabe's avatar
Florian Rabe committed
98
\begin{example}
99
Consider again the axiom $\forall x:\cn{set},y:\cn{set}.\; \cn{beautiful}(x) \wedge y \subseteq x \Rightarrow \cn{beautiful}(y)$ with internal representation \[\ombind{\forall}{x:\cn{set},y:\cn{set}}{\oma{\Rightarrow}{\oma{\wedge}{\oma{\cn{beautiful}}{x},\oma{\subseteq}{y,x}},\oma{\cn{beautiful}}{y}}}.\]
Florian Rabe's avatar
Florian Rabe committed
100

Dennis Müller's avatar
Dennis Müller committed
101
The \emph{short} syntax tree and list of constants associated with this term would be:
102
103
104
105
106
\[t=\ombind{C_1}{C_2,C_2}{\oma{C_3}{\oma{C_4}{\oma{C_5}{V_2},\oma{C_6}{V_1,V_2}},\oma{C_5}{V_1}}}\] 
\[s=(\forall,\cn{set},\Rightarrow,\wedge,\cn{beautiful},\subseteq)\]
The corresponding long syntax tree is :
\[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})\]
Florian Rabe's avatar
Florian Rabe committed
107
\end{example}
Dennis Müller's avatar
Dennis Müller committed
108

Florian Rabe's avatar
Florian Rabe committed
109
For our algorithm, we pick the \emph{long} abstract syntax tree, which may appear surprising.
Dennis Müller's avatar
Dennis Müller committed
110
The reason is that shortness is not preserved when applying a simple view: whenever a view maps two different constants to the same constant, the resulting tree is not short anymore.
Florian Rabe's avatar
Florian Rabe committed
111
112
113
Longness, on the other hand, is preserved.
The disadvantage that long trees take more time to traverse is outweighed by the advantage that we never have to renormalize the trees.

Dennis Müller's avatar
Dennis Müller committed
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
%\begin{oldpart}{FR: replaced with the above}
%
%\subsection{The General Algorithm} The aim is to find typing-preserving morphisms between theories, i.e. given a constant $C:t$ in a theory $T_1$, we want to find a view $V:T_1\to T_2$ such that if $V(C)=C'$ and $C':t'\in T_2$, we have $V(t)=t'$. Correspondingly, we need to consider the types of the constants in our two theories, which we assume to be flat.
%
%To run a proper unification algorithm is in our situation infeasible, since the flat version of a theory can become prohibitively large (and obviously finding two unifiable types in two theories is a search problem quadratic in the number of constants). To solve that problem, we first preprocess our theories such that pre-selecting plausibly ``unifiable'' constants becomes as fast as possible.
%
%\paragraph{} We do so by first transforming each constant $C$ in a theory to an \emph{encoding} $(\cn{h}(C),\cn{syms}(C))$ the following way:
%
%Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by enumerating them and storing the symbol's names in a list $\cn{syms}(C)$. 
%
%As a result, we get a pair $(\cn{tree}(C),\cn{syms}(C))$. Now an assignment $V(C)=D$ is valid, iff $\cn{tree}(C)=\cn{tree}(D)$, the lists $\cn{syms}(C)$ and $\cn{syms}(D)$ have the same length and their pairwise assignments $V(\cn{syms}(C)_i)=\cn{syms}(D)_i$ are all valid.
%
%Furthermore, since we only need $\cn{tree}(C)$ for an equality check, we can immediately replace $\cn{tree}(C)$ by an integer hashcode $\cn{h}(C)$.
%
%Now given a constant $C\in T_1$, we can find valid matches in $T_2$ by computing the encodings for each constant in $T_1$ and $T_2$, taking the list of constants $C'\in T_2$ with $\cn{h}(C')=\cn{h}(C)$ and recursing into their respective lists of symbols.
%\end{oldpart}
Florian Rabe's avatar
Florian Rabe committed
130
131
132
133

\subsection{Search}

Consider two constants $c:E$ and $c':E'$ preprocessed into long abstract syntax trees $(t,s)$ and $(t',s')$.
Dennis Müller's avatar
Dennis Müller committed
134
135
It is now straightforward to show the following Lemma:
\begin{lemma}
Dennis Müller's avatar
Dennis Müller committed
136
The assignment $c\mapsto c'$ is well-typed in a view $\sigma$ if $t=t'$ (in which case $s$ and $s'$ must have the same length $l$) and $\sigma$ also contains $s_i\mapsto s'_i$ for $i=1,\ldots,l$.
Dennis Müller's avatar
Dennis Müller committed
137
138
\end{lemma}
Of course, the condition about $s_i\mapsto s'_i$ may be redundant if $s$ contain duplicates; but because $s$ has to be traversed anyway, it is cheap to skip all duplicates. We call the set of assignments $s_i\mapsto s'_i$ the \textbf{prerequisites} of $c\mapsto c'$.
Florian Rabe's avatar
Florian Rabe committed
139

Florian Rabe's avatar
Florian Rabe committed
140
141
142
This lemma is the center of our search algorithm explained in
\begin{lemma}[Core Algorithm]
Consider two constant declarations $c$ and $c'$ in theories $\Sigma'$ and $\Sigma'$.
Dennis Müller's avatar
Dennis Müller committed
143
We define a view by starting with $\sigma=c\mapsto c'$ and recursively adding all prerequisites to $\sigma$ until
Florian Rabe's avatar
Florian Rabe committed
144
\begin{compactitem}
Florian Rabe's avatar
Florian Rabe committed
145
146
 \item either the recursion terminates
 \item or $\sigma$ contains two different assignments for the same constant, in which case we fail.
Florian Rabe's avatar
Florian Rabe committed
147
148
\end{compactitem}

Dennis Müller's avatar
Dennis Müller committed
149
If the above algorithm succeeds, then $\sigma$ is a well-typed partial simple view from $\Sigma$ to $\Sigma'$.
Florian Rabe's avatar
Florian Rabe committed
150
151
\end{lemma}

152
153
154
155
156
157
158
\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
\[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})\]
Since $t=t'$, we set $c\mapsto c'$ and compare $s$ with $s'$, meaning we check (ignoring duplicates) that $\forall\mapsto\forall$, $\cn{set}\mapsto\cn{powerset}$, $\Rightarrow\mapsto\Rightarrow$, $\wedge\mapsto\wedge$, $\cn{beautiful}\mapsto\cn{finite}$ and $\subseteq\mapsto\subseteq$ are all valid.
\end{example}

Dennis Müller's avatar
Dennis Müller committed
159
160
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.
Florian Rabe's avatar
Florian Rabe committed
161
For example, consider the typical case where theories contain some symbol declarations and some axioms, in which the symbols occur.
Dennis Müller's avatar
Dennis Müller committed
162
Then the core algorithm will only find views that map at most $1$ axiom.
Florian Rabe's avatar
Florian Rabe committed
163

Dennis Müller's avatar
Dennis Müller committed
164
165
166
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]
We call two partial views \textbf{compatible} if they agree on all constants for which both provide an assignment.
Florian Rabe's avatar
Florian Rabe committed
167

Dennis Müller's avatar
Dennis Müller committed
168
The union of compatible well-typed views is again well-typed.
Florian Rabe's avatar
Florian Rabe committed
169
\end{lemma}
170
\begin{example}
Dennis Müller's avatar
Dennis Müller committed
171
	Consider the partial view from Example \ref{ex:beautifinite} and imagine a second partial view for the axioms
172
173
	$\cn{beautiful}(\emptyset)$ and $\cn{finite}(\emptyset)$. The former has the requirements
	\[ \forall\mapsto\forall,\quad \cn{set}\mapsto\cn{powerset}\quad \Rightarrow\mapsto\Rightarrow \quad \wedge\mapsto\wedge \quad \cn{beautiful}\mapsto\cn{finite} \quad \subseteq\mapsto\subseteq\]
Dennis Müller's avatar
Dennis Müller committed
174
	The latter requires only $\cn{set}\mapsto\cn{powerset}$ and $\emptyset\mapsto\emptyset$. Since both views agree on all assignments, we can merge them into one view mapping both axioms and all requirements of both.
175
\end{example}
Dennis Müller's avatar
update    
Dennis Müller committed
176

Florian Rabe's avatar
Florian Rabe committed
177
178
\subsection{Optimizations}\label{sec:algparams}

Florian Rabe's avatar
Florian Rabe committed
179
180
181
182
183
184
185
186
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}
Dennis Müller's avatar
Dennis Müller committed
187
We improve the preprocessing in a way that exploits the common meta-theory, which is meant to be fixed by every view.
Florian Rabe's avatar
Florian Rabe committed
188
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.
Dennis Müller's avatar
Dennis Müller committed
189
190
With this change, $s$ will never contain meta-theory constants, and the core algorithm will only find views that fix all meta-theory constants.
Because $s$ is much shorter now, the view search is much faster.
Florian Rabe's avatar
Florian Rabe committed
191
192
193
194
195
196
197
198
199
200

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.
Dennis Müller's avatar
Dennis Müller committed
201
Because views that only map 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.
Florian Rabe's avatar
Florian Rabe committed
202
203
204
205
206

%\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.
Dennis Müller's avatar
Dennis Müller committed
207
208
If $\Sigma$ is imported into $\Sigma'$, then the set of partial views out of $\Sigma'$ is a superset of the set of partial views out of $\Sigma$.
If implemented naively, that would yield a quadratic blow-up in the number of views to consider.
Florian Rabe's avatar
Florian Rabe committed
209

Dennis Müller's avatar
Dennis Müller committed
210
211
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.
Florian Rabe's avatar
Florian Rabe committed
212
213
214
215
216

\subsection{Implementation}\label{sec:usecase}

\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{beautysource}}
Dennis Müller's avatar
Dennis Müller committed
217
  \fbox{\includegraphics[width=0.7\textwidth]{results}}
Florian Rabe's avatar
Florian Rabe committed
218
219
220
221
222
223
224
225
226
227
228
229
\caption{``Beautiful Sets'' in MMT Surface Syntax and View Finder Results}\label{fig:use:source}
\end{figure}

\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.
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.

Dennis Müller's avatar
Dennis Müller committed
230
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}).
Florian Rabe's avatar
Florian Rabe committed
231
232
233
234
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.
Dennis Müller's avatar
Dennis Müller committed
235

Michael Kohlhase's avatar
Michael Kohlhase committed
236
237

%%% Local Variables:
Michael Kohlhase's avatar
Michael Kohlhase committed
238
%%% Mode: latex
Michael Kohlhase's avatar
Michael Kohlhase committed
239
240
%%% eval:  (set-fill-column 5000)
%%% eval:  (visual-line-mode)
Michael Kohlhase's avatar
Michael Kohlhase committed
241
242
%%% TeX-master: "paper"
%%% End:
243
244

%  LocalWords:  defemph defemph emph vdash_ normalization optimized compactenum textbf th
Michael Kohlhase's avatar
Michael Kohlhase committed
245
%  LocalWords:  t,s ednote renormalize oldpart syms mapsto mapsto ldots,l compactitem y,x
246
%  LocalWords:  normalizing subtyping subterms preprocessings ldots ldots formalization
Michael Kohlhase's avatar
Michael Kohlhase committed
247
248
249
%  LocalWords:  vdash Rightarrow vdash vdash vdash forall vdash sec:preproc subseteq c,c
%  LocalWords:  subseteq ex:beautifinite powerset powerset emptyset emptyset normalized
%  LocalWords:  Optimizations sec:algparams axiomatizations