Let $C$ be a corpus of theories with the same fixed meta-theory $M$.
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}.
\rmoi[id=viewfinding]{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}.}
Note that a view finder is sufficient to solve the theory classification use case from the introduction:
Jane provides a $M$-theory $Q$ of beautiful sets, the view finder computes all (total) views from $Q$ into $C$.
...
...
@@ -60,10 +60,11 @@ Above multiple normalization steps make use of a total order on abstract syntax
We omit the details and only remark that we try to avoid using the names of constants in the definition of the order --- otherwise, declarations that could be matched by a view would be normalized differently.
Even when breaking ties between requires comparing two constants, we can first try to recursively compare the syntax trees of their types.
\paragraph{Abstract Syntax Trees}
We define \textbf{abstract syntax trees} as pairs $(t,s)$ where $t$ is subject to the grammar
\begin{rmoienv}[id=abstractsyntaxtree]
\paragraph{Abstract Syntax Trees}We define \textbf{abstract syntax trees} as pairs $(t,s)$ where $t$ is subject to the grammar
(where $Nat$ is a non-terminal for natural numbers) and $s$ is a list of constant names.
\end{rmoienv}
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$.
Abstract syntax trees have the nice property that they commute with the application of simple views $\sigma$:
...
...
@@ -129,7 +130,7 @@ Then the core algorithm will only find views that map at most one axiom.
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.
\rmoi[id=amalgamatingviews]{We call two partial views \textbf{compatible} if they agree on all constants for which both provide an assignment.}
The union of compatible well-typed views is again well-typed.