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{newpart}{DM}
We have seen how a viewfinder can be used for theory \emph{discovery} and finding constants with specific desired properties, but many other potential use cases are imaginable. The main problems to solve with respect to these is less about the algorithm or software design challenges, but user interfaces.
The theory discovery use case described in Sec. \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 across-library use case in Sec. \ref{sec:pvs} already 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:
\end{newpart}
\begin{itemize}
\item If the codomain of a view is a theory representing a specific model, it would tell her that those
\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 Given that the Viewfinder looks for \emph{partial} views, we can use it to find natural
\item\textbf{Library Refactoring:}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.
...
...
@@ -15,11 +19,11 @@ We have seen how a viewfinder can be used for theory \emph{discovery}. But with
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
\item\textbf{Theory Generalization:}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
\item\textbf{Folklore-based Conjecture:}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 --
...
...
@@ -27,16 +31,11 @@ We have seen how a viewfinder can be used for theory \emph{discovery}. But with
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}
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 treat and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
title="{IMPS: An Interactive Mathematical Proof System}",
journal="{Journal of Automated Reasoning}",
pages="213--248",
volume="11",
number="2",
year="1993",
}
@Book{isabelle,
author="L. Paulson",
title="{Isabelle: A Generic Theorem Prover}",
publisher="Springer",
series="Lecture Notes in Computer Science",
volume="828",
year="1994",
}
@INPROCEEDINGS{NorKoh:efnrsmk07,
author={Immanuel Normann and Michael Kohlhase},
title={Extended Formula Normalization for $\epsilon$-Retrieval and
Sharing of Mathematical Knowledge},
pages={266--279},
crossref={MKM07},
keywords={conference},
pubs={mkohlhase,mws,omdoc}}
@inproceedings{KMOR:pvs:17,
author="M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
title="{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
year="2017",
pages="319--335",
booktitle="Interactive Theorem Proving",
editor="M. Ayala-Rincon and C. Munoz",
publisher="Springer"
}
@inproceedings{hol_isahol_matching,
author={T. Gauthier and C. Kaliszyk},
title="{Matching concepts across HOL libraries}",
booktitle={Intelligent Computer Mathematics},
editor={S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
pages={267--281},
year=2014,
publisher={Springer}
}
@online{OAFproject:on,
label={OAF},
url={https://kwarc.info/projects/oaf/},
title={{OAF}: An Open Archive for Formalizations},
urldate={2018-04-26}}
@Article{lf,
author="R. Harper and F. Honsell and G. Plotkin",
title="{A framework for defining logics}",
journal="{Journal of the Association for Computing Machinery}",
year=1993,
volume=40,
number=1,
pages="143--184",
}
@inproceedings{KKMR:alignments:16,
author="C. Kaliszyk and M. Kohlhase and D. M{\"u}ller and F. Rabe",
title="{A Standard for Aligning Mathematical Concepts}",
year="2016",
pages="229--244",
booktitle="Work in Progress at CICM 2016",
editor="A. Kohlhase and M. Kohlhase and P. Libbrecht and B. Miller and F. Tompa and A. Naummowicz and W. Neuper and P. Quaresma and M. Suda",
publisher="CEUR-WS.org"
}
@inproceedings{ODK:mitm:16,
author="P. Dehaye and M. Iancu and M. Kohlhase and A. Konovalov and S. Leli{\`e}vre and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and T. Wiesing",
title="{Interoperability in the ODK Project: The Math-in-the-Middle Approach}",
year="2016",
pages="117--131",
booktitle="Intelligent Computer Mathematics",
editor="M. Kohlhase and L. {de Moura} and M. Johansson and B. Miller and F. Tompa",
publisher="Springer"
}
@inproceedings{MRLR:alignments:17,
author="D. M{\"u}ller and C. Rothgang and Y. Liu and F. Rabe",
title="{Alignment-based Translations Across Formal Systems Using Interface Theories}",
year="2017",
pages="77--93",
booktitle="Proof eXchange for Theorem Proving",
editor="C. Dubois and B. {Woltzenlogel Paleo}",
publisher="Open Publishing Association"
}
@INPROCEEDINGS{mathhub,
author="M. Iancu and C. Jucovschi and M. Kohlhase and T. Wiesing",
title="{System Description: MathHub.info}",
booktitle="Intelligent Computer Mathematics",
editor="S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
pages="431--434",
publisher="Springer",
year={2014},
}
@inproceedings{RupKohMue:fitgv17,
author={Marcel Rupprecht and Michael Kohlhase and Dennis M{\"u}ller},
@@ -67,14 +67,14 @@ Automatically and systematically searching for new theory morphisms was first un
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.
This situation has changed since then as multiple such exports have become available.
In particular, we have developed the MMT language \cite{RK:mmt} and the concrete syntax of the OMDoc XML format \cite{omdoc} as a uniform representation language for such corpora.
And we have translated multiple proof assistant libraries into this format, including the ones of PVS in \cite{KMOR:pvs:17} and HOL Light in \cite{RK:hollight:15}.
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.
And we have translated multiple proof assistant libraries into this format, including the ones of PVS in \cite{KMOR:pvs:17} and HOL Light in \cite{KR:hollight:14}.
Building on these developments, we are now able, for the first time, to apply generic methods --- i.e., methods that work at the MMT level --- to search for theory morphisms in these libraries.
While inspired by the ideas of \cite{NorKoh:efnrsmk07}, our design and implementation are completely novel.
In particular, the theory makes use of the rigorous language-independent definitions of \emph{theory} and \emph{theory morphism} provided by MMT, and the practical implementation makes use of the MMT system, which provides high-level APIs for these concepts.
\cite{cezary+thibault-paper} applies techniques related to ours to a related problem.
\cite{hol_isahol_matching} applies techniques related to ours to a related problem.
Instead, of theory morphisms inside a single corpus, they use machine learning to find similar constants in two different corpora.
Their results can roughly be seen as a single partial morphism from one corpus to the other.
...
...
@@ -86,7 +86,7 @@ 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 two concrete case studies. \ednote{add 1-2 sentences for each case study}
Secondly, we apply this view finder in two concrete case studies: In the first, we start with an abstract theory and try to figure out if it already exists in the same library. 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.
\paragraph{Overview}
In Section~\ref{sec:prelim}, we revise the basics of MMT and the representations of (exemplary) the PVS and HOL Light libraries.
We present a method for finding morphisms between formal theories, both within as well
as across libraries based on different logical foundations. These morphisms can yield
both (more or less formal) \emph{alignments} between individual symbols as well as
truth-preserving morphisms between whole theories. As they induce new theorems in the
target theory for any of the source theory, theory morphisms are high-value elements of
as across libraries based on different logical foundations.
% These morphisms can yield both (more or less formal) \emph{alignments} between individual symbols as well as truth-preserving morphisms between whole theories.
As they induce new theorems in the target theory for any of the source theory, theory morphisms are high-value elements of
a modular formal library. Usually, theory morphisms are manually encoded, but this
practice requires authors who are familiar with source and target theories at the same
time, which limits the scalability of the manual approach.
...
...
@@ -97,13 +97,12 @@
\section{Preliminaries}\label{sec:prelim}
\input{prelim}
\section{Finding Theory Morphisms}\label{sec:viewfinder}
\section{Finding Theory Morphisms Intra-Library}\label{sec:viewfinder}
@@ -21,7 +21,7 @@ In particular, if we represent proofs as typed terms, theory morphisms preserve
This property makes theory morphism so valuable for structuring, refactoring, and integrating large corpora.
MMT achieves language-independence through the use of \textbf{meta-theories}: every MMT-theory may designate a previously defined theory as its meta-theory.
For example, when represent the HOL Light library in MMT, we first write a theory $L$ for HOL Light.
For example, when we represent the HOL Light library in MMT, we first write a theory $L$ for the logical primitives of HOL Light.
Then each theory in the HOL Light library is represented as a theory with $L$ as its meta-theory.
In fact, we usually go one step further: $L$ itself is a theory, whose meta-theory is a logical framework such as LF.
That allows $L$ to concisely define the syntax and inference system of HOL Light.
...
...
@@ -39,7 +39,7 @@ Thus, we assume that $\Sigma$ and $\Sigma'$ have the same meta-theory $M$, and t
& Theory $\Sigma$& Morphism $\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'$by homomorphic extension \\
$\Sigma$-expressions $E$& formed from $M$- and $\Sigma$-constants & mapped to $\Sigma'$expressions\\
\hline
\end{tabular}
\end{center}
...
...
@@ -59,8 +59,11 @@ Complex expressions are of the form $\ombind{o}{x_1:t_1,\ldots,x_m:t_m}{a_1,\ldo
\item$a_i$ is an argument of $o$
\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, \ednote{give examples}
\begin{newpart}{DM}
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.
%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
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 constants may carry an optional definiens, in which case we write $c:E=e$.
...
...
@@ -90,55 +93,55 @@ Defined constants can be eliminated by definition expansion.
%\end{center}
%\end{example
\begin{oldpart}{FR: replaced with the above}
For the purposes of this paper, we will work with the (only slightly simplified) grammar given in Figure \ref{fig:mmtgrammar}.
\begin{figure}[ht]\centering\vspace*{-1em}
\begin{mdframed}
\begin{tabular}{rl@{\quad}l|l}
\cn{Thy}$::=$&$T[:T]=\{(\cn{Inc})^\ast\ (\cn{Const})^\ast\}$& Theory &\multirow{2}{*}{Modules}\\
\cn{View}$::=$&$T : T \to T =\{(\cn{Ass})^\ast\}$& View &\\\hline
\item Theories have a module name, an optional \emph{meta-theory} and a body consisting of \emph{includes} of other theories
and a list of \emph{constant declarations}.
\item Constant declarations have a name and two optional term components; a \emph{type} ($[:t]$), and a \emph{definition} ($[=t]$).
\item Views $V : T_1\to T_2$ have a module name, a domain theory $T_1$, a codomain theory $T_2$ and a body consisting of assignments
$C = t$.
\item Terms are either
\begin{itemize}
\item variables $x$,
\item symbol references $T?C$ (referencing the constant $C$ in theory $T$),
\item applications $\oma{f}{a_1,\ldots,a_n}$ of a term $f$ to a list of arguments $a_1,\ldots,a_n$ or
\item binding application $\ombind{f}{x_1[:t_1][=d_1],\ldots,x_n[:t_n][=d_n]}{b}$, where $f$\emph{binds} the variables
$x_1,\ldots,x_n$ in the body $b$ (representing binders such as quantifiers, lambdas, dependent type constructors etc.).
\end{itemize}
\end{itemize}
The term components of a constant in a theory $T$ may only contain symbol references to constants declared previously in $T$, or that are declared in some theory $T'$ (recursively) included in $T$ (or its meta-theory, which we consider an \emph{include} as well).
We can eliminate all includes in a theory $T$ by simply copying over the constant declarations in the included theories; we call this process \emph{flattening}. We will often and without loss of generality assume a theory to be \emph{flat} for convenience.
An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any assignment $C=t$ contained, $C$ is a constant declared in the flattened domain $T_1$ and $t$ is a syntactically well-formed term in the codomain $T_2$. We call a view \emph{total} if all \emph{undefined} constants in the domain have a corresponding assignment and \emph{partial} otherwise.
\end{oldpart}
%\begin{oldpart}{FR: replaced with the above}
%For the purposes of this paper, we will work with the (only slightly simplified) grammar given in Figure \ref{fig:mmtgrammar}.
% \item Theories have a module name, an optional \emph{meta-theory} and a body consisting of \emph{includes} of other theories
% and a list of \emph{constant declarations}.
% \item Constant declarations have a name and two optional term components; a \emph{type} ($[:t]$), and a \emph{definition} ($[=t]$).
% \item Views $V : T_1 \to T_2$ have a module name, a domain theory $T_1$, a codomain theory $T_2$ and a body consisting of assignments
% $C = t$.
% \item Terms are either
% \begin{itemize}
% \item variables $x$,
% \item symbol references $T?C$ (referencing the constant $C$ in theory $T$),
% \item applications $\oma{f}{a_1,\ldots,a_n}$ of a term $f$ to a list of arguments $a_1,\ldots,a_n$ or
% \item binding application $\ombind{f}{x_1[:t_1][=d_1],\ldots,x_n[:t_n][=d_n]}{b}$, where $f$ \emph{binds} the variables
% $x_1,\ldots,x_n$ in the body $b$ (representing binders such as quantifiers, lambdas, dependent type constructors etc.).
% \end{itemize}
%\end{itemize}
%The term components of a constant in a theory $T$ may only contain symbol references to constants declared previously in $T$, or that are declared in some theory $T'$ (recursively) included in $T$ (or its meta-theory, which we consider an \emph{include} as well).
%We can eliminate all includes in a theory $T$ by simply copying over the constant declarations in the included theories; we call this process \emph{flattening}. We will often and without loss of generality assume a theory to be \emph{flat} for convenience.
%
%An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any assignment $C=t$ contained, $C$ is a constant declared in the flattened domain $T_1$ and $t$ is a syntactically well-formed term in the codomain $T_2$. We call a view \emph{total} if all \emph{undefined} constants in the domain have a corresponding assignment and \emph{partial} otherwise.
%
%\end{oldpart}
\subsection{Proof Assistant Libraries in MMT}\label{sec:oaf}
As part of the OAF project~\cite{OAFproject:on}, 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~\cite{lf} (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}.
When elaborating definitions, it is important to consider that this may also reduce the number of results, 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''.
Similarly, certain idiosyncracies -- such as PVS's common usage of theory parameters -- 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, which may be unified with any other symbol or hole, but are not recursed into. The subterms that are to be considered holes can be marked as such during preprocessing.