@@ -20,8 +20,8 @@ In these situations, we can consider the \emph{common} symbols as a fixed part o

\paragraph{Picking starting pairs:} Note, that we will still find many spurious matches if executed in its general form. The reason being that (for example) all atomic types match each other, as will all binary operators etc. Most of these results will not be interesting. Furthermore, since the algorithm needs to recurse into the lists $\cn{syms}(C)$, many potential matches will need to be checked repeatedly. Both problems can be massively reduced by selecting specific pairs of encodings as \emph{starting pairs} for the algorithm, so that the majority of matching constants will only be considered if the algorithm runs into them during recursing. Potential useful starting points are:

\begin{itemize}

\item\emph{Axioms:} Since we are mostly interested in matching constants that share the same mathematical properties, by using axioms as starting point we can ensure that the algorithm only matches constants that have at least one (axiomatic) property in common (e.g. only commutative, or associative) operators.

\item\emph{The length of $\cn{syms}(C)$:} This way we can guarantee, that only matches will be produced that relate at least two constant to each other -- if e.g. we are interested in structures that have a distributive property, this will make sure that we only find those views, where both operators are matched as intended.

\item\emph{Axioms:} Since we are mostly interested in matching constants that share the same mathematical properties, by using axioms as starting point we can ensure that the algorithm only matches constants that have at least one (axiomatic) property in common (e.g. only commutative, or associative operators).

\item\emph{The length of $\cn{syms}(C)$:} This way we can guarantee, that only matches will be produced that relate at least two (or more) constant to each other -- if e.g. we are interested in structures that have a distributive property, this will make sure that we only find those views, where both operators are matched as intended.

\end{itemize}

\paragraph{Picking starting theories:} If we try to find views between whole collections of theories, we can obviously disregard all theories that are included in some other theory in our collections, since we need to work with the flat theories anyway. Consequently, by only using maximal theories we do not find any fewer views but speed up the search significantly.