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}. 
Michael Kohlhase's avatar
Michael Kohlhase committed
3
Note that a view finder is sufficient to solve the theory classification use case from the introduction: 
4
Jane provides a $M$-theory $Q$ of beautiful sets, the view finder computes all (total) views from $Q$ into $C$.
Florian Rabe's avatar
Florian Rabe committed
5

Florian Rabe's avatar
Florian Rabe committed
6
\paragraph{Efficiency Considerations}
Michael Kohlhase's avatar
Michael Kohlhase committed
7
The cost of this problem quickly explodes.
Dennis Müller's avatar
Dennis Müller committed
8
9
10
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
11
12

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
13
14
15
16
17
18
19
(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.
20
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.
Florian Rabe's avatar
Florian Rabe committed
21
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
22
23
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
24

Dennis Müller's avatar
Dennis Müller committed
25
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
26
27
Depending on $M$, this equality judgment may be undecidable and require theorem proving.

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

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

\subsection{Preprocessing}

Florian Rabe's avatar
Florian Rabe committed
39
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
40
41
42
Both steps are described below.

\paragraph{Normalization}
43
involves two steps: \textbf{MMT-level normalization} performs generic transformations that do not depend on the meta-theory $M$.
Florian Rabe's avatar
Florian Rabe committed
44
These include elaboration of structured theories and definition expansion, which we mentioned in Sect.~\ref{sec:prelim}.
Florian Rabe's avatar
Florian Rabe committed
45
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
46
47
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
48

49
\textbf{Meta-theory-level normalization} applies an $M$-specific normalization function.
Florian Rabe's avatar
Florian Rabe committed
50
In general, we assume this normalization to be given as a black box.
51
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:
Florian Rabe's avatar
Florian Rabe committed
52
53
\begin{compactenum}
  \item Top-level universal quantifiers and implications are rewritten into the function space of the logical framework using the Curry-Howard correspondence.
54
55
  \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.
Florian Rabe's avatar
Florian Rabe committed
56
57
58
59
  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
60
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
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
77

Florian Rabe's avatar
Florian Rabe committed
78
79
80

\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
81
 \[t ::= C_{Nat} \mid V_{Nat} \mid \ombind{t}{t^+}{t^+}\]
Florian Rabe's avatar
Florian Rabe committed
82
(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
83
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
84

Dennis Müller's avatar
Dennis Müller committed
85
Abstract syntax trees have the nice property that they commute with the application of simple views $\sigma$:
Florian Rabe's avatar
Florian Rabe committed
86
87
88
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
89
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
90
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
91
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
92
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
93

Florian Rabe's avatar
Florian Rabe committed
94
\begin{example}
95
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
96

Dennis Müller's avatar
Dennis Müller committed
97
The \emph{short} syntax tree and list of constants associated with this term would be:
98
99
100
101
102
\[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
103
\end{example}
Dennis Müller's avatar
Dennis Müller committed
104

Florian Rabe's avatar
Florian Rabe committed
105
For our algorithm, we pick the \emph{long} abstract syntax tree, which may appear surprising.
Dennis Müller's avatar
Dennis Müller committed
106
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
107
108
109
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
%\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
126
127
128
129

\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
130
131
It is now straightforward to show the following Lemma:
\begin{lemma}
Dennis Müller's avatar
Dennis Müller committed
132
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
133
134
\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
135

Florian Rabe's avatar
Florian Rabe committed
136
137
138
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
139
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
140
\begin{compactitem}
Florian Rabe's avatar
Florian Rabe committed
141
142
 \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
143
144
\end{compactitem}

Dennis Müller's avatar
Dennis Müller committed
145
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
146
147
\end{lemma}

148
\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
149
150
151
152
153
154
\[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
155
156
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
157
For example, consider the typical case where theories contain some symbol declarations and some axioms, in which the symbols occur.
158
Then the core algorithm will only find views that map at most one axiom.
Florian Rabe's avatar
Florian Rabe committed
159

Dennis Müller's avatar
Dennis Müller committed
160
161
162
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
163

Dennis Müller's avatar
Dennis Müller committed
164
The union of compatible well-typed views is again well-typed.
Florian Rabe's avatar
Florian Rabe committed
165
\end{lemma}
166
\begin{example}
Dennis Müller's avatar
Dennis Müller committed
167
	Consider the partial view from Example \ref{ex:beautifinite} and imagine a second partial view for the axioms
168
169
	$\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
170
	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.
171
\end{example}
Dennis Müller's avatar
update    
Dennis Müller committed
172

Florian Rabe's avatar
Florian Rabe committed
173
174
\subsection{Optimizations}\label{sec:algparams}

Florian Rabe's avatar
Florian Rabe committed
175
The above presentation is intentionally simple to convey the general idea.
176
We now describe a few advanced features of our implementation to enhance scalability.
Florian Rabe's avatar
Florian Rabe committed
177
178
179
180
181
182

\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
183
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
184
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
185
186
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
187
188
189
190
191
192
193
194
195
196

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
197
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
198
199
200
201
202

%\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
203
204
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
205

Dennis Müller's avatar
Dennis Müller committed
206
207
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
208
209
210

\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{beautysource}}
211
  \caption{``Beautiful Sets'' in MMT Surface Syntax}\label{fig:use:source}
Florian Rabe's avatar
Florian Rabe committed
212
213
\end{figure}

214
215
216
\subsection{Implementation}\label{sec:usecase}


Florian Rabe's avatar
Florian Rabe committed
217
\begin{wrapfigure}r{.61\textwidth}\vspace*{-2em}
218
219
220
  \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.
Florian Rabe's avatar
Florian Rabe committed
221
222
223
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.
224
 
Florian Rabe's avatar
Florian Rabe committed
225

226
227
228
229
230
\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}).
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