Commit 780b85ec authored by Florian Rabe's avatar Florian Rabe
Browse files

Merge branch 'master' of gl.kwarc.info:oaf/alignment-finder

parents bba954a1 e88564c3
- theory discovery
- natural extensions (partial views)
- models
- counter examples
- theorem transport (current theory is codomain)
- prioritize many definitions / theorems
- refactoring advice
- assoc / comm normalization
- term indexing techniques
- use existing views in $\cL$ (compositions of views are vivews) 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.
\ No newline at end of file
We have seen how a viewfinder can be used for theory \emph{discovery}. But with minor variations, extensions or more specialized interfaces many other potential use cases open up, which we plan to investigate in the future:
\begin{itemize}
\item 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 Given that the Viewfinder 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.
\item If we additionally consider views into and out of the theories found, this can make theory discovery even
more attractive. For example, a view from a theory of vector spaces intro matroids could inform Jane additionally,
that her beautiful sets, being matroids, form a generalization of the notion of linear independence in linear algebra.
\item If we were to keep book on our transfomations during preprocessing and normalization, we could use the found
views for translating both into the codomain as well as back from there into our starting 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 viewfinder.
A useful interface might specifically prioritize views into theories on top of which there are many
theorems and definitions that have been discovered.
\item For the last two 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 treat and evaluate the resulting (partial) views.
\item The last example in Section \ref{sec:usecase} shows how we can find properties like commutativity and
associativity, which can in turn inform a better normalization of the theory, which in turn would potentially
allow for finding more views. This could iteratively improve the results of the viewfinder.
\end{itemize}
\ No newline at end of file
......@@ -138,7 +138,7 @@ An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any a
As part of the OAF project \ednote{cite}, we have imported several proof assistant libraries into the MMT system. To motivate some of the design choices made in this paper, we will outline the general procedure behind these imports.
\paragraph{} First, we formalize the core logical foundation of the system. We do so by using the logical framework LF\ednote{cite} (at its core a dependently-typed lambda-calculus) and various extensions thereof, which are implemented in and supported by the MMT system. In LF, we can formalize the foundational primitives using the usual judgments-as-types and higher-order abstract syntax encodings -- hence theorems and axioms are represented as constants with a type $\vdash P$ for some proposition $P$, and primitive constructs like lambdas are formalized as LF-functions taking LF-lambda-expressions -- which serve as a general encoding of any variable binders -- as arguments.
\paragraph{} First, we formalize the core logical foundation of the system. We do so by using the logical framework LF\ednote{cite} (at its core a dependently-typed lambda calculus) and various extensions thereof, which are implemented in and supported by the MMT system. In LF, we can formalize the foundational primitives using the usual judgments-as-types and higher-order abstract syntax encodings -- hence theorems and axioms are represented as constants with a type $\vdash P$ for some proposition $P$, and primitive constructs like lambdas are formalized as LF-functions taking LF-lambda-expressions -- which serve as a general encoding of any variable binders -- as arguments.
The resulting formalizations are then used as meta-theory for imports of the libraries of the system under consideration. This results in a theory graph as in Figure \ref{fig:oaf}.
......
tex/pvs.png

52.6 KB

tex/results.png

46 KB | W: | H:

tex/results.png

45.1 KB | W: | H:

tex/results.png
tex/results.png
tex/results.png
tex/results.png
  • 2-up
  • Swipe
  • Onion skin
......@@ -8,7 +8,7 @@ is based on the (basic higher-order logic) foundation of the Math-in-the-Middle\
\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the Viewfinder}\label{fig:use:source}
\end{figure}
Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \cn{Find\ Views\ to...} $\to$ \cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) that 11 Views have been found, the most promising of which points to the theory
Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \cn{Find\ Views\ to...} $\to$ \cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) that two views have been found, the most promising of which points to the theory
\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.
\begin{figure}[ht]\centering
......@@ -18,7 +18,8 @@ Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \
\paragraph{} Using a different library as target, we can for example quickly write down a theory for a commutative binary operator (still using the Math-in-the-Middle foundation), allowing us to search e.g. the PVS Prelude library for any commutative operators, as in Figure \ref{fig:use:pvs}.
\begin{figure}
Hier könnte Ihre Werbung stehen
\begin{figure}[ht]\centering
\fbox{\includegraphics[width=\textwidth]{pvs}}
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\end{figure}
\ No newline at end of file
\end{figure}
\ednote{8 results for NASA, but NASA doesn't work in jEdit because of limited memory}
\ No newline at end of file
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