From f0d0b46e75da8dcb83ba061d59643f5414d25a9c 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:06:24 +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 32f010a..d71c357 100644
--- a/tex/viewfinder.tex
+++ b/tex/viewfinder.tex
@@ -1,4 +1,4 @@
-\subsection{The General Algorithm} 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.
+\subsection{The General Algorithm} 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.
 
-- 
GitLab