From a17f29d12b25d0847bbf5a7653c16f4f23d8a5f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de>
Date: Fri, 20 Apr 2018 14:05:42 +0200
Subject: [PATCH] update
---
tex/viewfinder.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tex/viewfinder.tex b/tex/viewfinder.tex
index f071809..32f010a 100644
--- a/tex/viewfinder.tex
+++ b/tex/viewfinder.tex
@@ -30,7 +30,7 @@ In these situations, we can consider the \emph{common} symbols as a fixed part o
Especially when looking for views between theories in different libraries (and built on different foundations), various differences in available foundational primitives and library-specific best practices and idiosyncracies can prevent the algorithm from finding desired matches. There are two approaches to increasing the number of results in these cases:
\begin{itemize}
\item We can preprocess theories, by e.g. normalizing expressions, eliminating higher-order abstract syntax encodings or encoding-related redundant information (such as the type of a typed equality, which in the presence of subtyping can be different from the types of both sides of an equation), or elaborating abbreviations/definitions.
- \item In many instances, the translations between two foundations is too complex to be discovered purely syntactically. In these cases we can provide arbitrary translations between theories, which are applied before computing the encoding.\ednote{Mention/cite alignment paper}
+ \item In many instances, the translations between two foundations is too complex to be discovered purely syntactically. In these cases we can provide arbitrary translations between theories, which are applied before computing the encoding.\ednote{Mention/cite alignment-translation paper}
\end{itemize}
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 several encodings for the same constant during preprocessing, such as one with definitions expanded and one ``as is''.
--
GitLab