Commit 8e63904f authored by Dennis Müller's avatar Dennis Müller
Browse files


parent 4e6d5cd5
......@@ -23,7 +23,9 @@ Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEd
screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
beautiful'', which is equivalent via the subset clause, maybe use that in the example:
define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
see what the viewfinder catches.} In the base use case, Jane learns that her
see what the viewfinder catches.\\
DM: It's not going to be a ``proper'' theorem because it will be difficult to construct a proof.
Apart from that it should still match Base, beautiful and the other axioms.} In the base use 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
......@@ -74,7 +76,7 @@ This enables us, for the first time, to apply generic methods --- i.e., methods
Our contribution is twofold.
Firstly, we present such a generic theory morphism finder.\ednote{add 2 sentences about how it works}
Firstly, we present such a generic theory morphism finder. The algorithm tries to match two symbols by unifying their types. This is made efficient by separating the term into a hashed representation of its abstract syntax tree (which serves as a fast plausibility check for pre-selecting matching candidates) and the list of symbol occurences 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}
......@@ -84,4 +86,4 @@ Automatically and systematically searching for new theory morphisms, let alone d
\ednote{FR: I really don't know any related work. Is there anything?}
In Section~\ref{sec:prelim}, we revise the basics of MMT and the PVS and the representations of the HOL Light libraries
In Section~\ref{sec:prelim}, we revise the basics of MMT and the representations of (exemplary) the PVS and HOL Light libraries.
......@@ -103,6 +103,8 @@
\paragraph{Future Work} \ednote{term indexing, normalization, using alignments / translations between libraries}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
......@@ -44,4 +44,4 @@ An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any a
\subsection{Proof Assistant Libraries in MMT}
\ No newline at end of file
OAF: PVS, HOL Light, MitM for use case
\ No newline at end of file
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 unficiation 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 considering the syntax tree of the type $t$ of a constant $C$ and replacing the leaves by an abstract representation $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index. We can take care of symbol references by considering them like a separate set of variables, replacing them by their De Brujin indices 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)$.
\paragraph{} Now given a constant $C\in T_1$, we can find valid matches in $T_2$ by computing the pairs 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.
\ednote{talk about: additional preprocessing/normalization, using alignments/arbitrary translations before hashing, preselecting starting points (e.g. axioms only, length of symbol-list), using multiple representations for the same constant (e.g. with all definitions expanded), hashing fixed symbols (meta-theory) along with the syntax trees, storing/reusing hashes}
\ No newline at end of file
Supports Markdown
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