Changeset 47ed726

Timestamp:

Dec 8, 2018, 4:06:25 PM (6 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, deferred_resn, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, no_list, persistent-indexer, pthread-emulation, qualifiedEnum

Children:

29207bf

Parents:

df43791

Message:

Added asymptotic analysis to type environment chapter of thesis

File:

• doc/theses/aaron_moss_PhD/phd/type-environment.tex (modified) (3 diffs)

doc/theses/aaron_moss_PhD/phd/type-environment.tex

@@ -49 +49 @@
 For instance, unifying !R*! with !S*! for type variables !R! and !S! will result in a call to $unify(T, find($!R!$), find($!S!$))$, while unifying !R*! with !int*! will result in a call to $unifyBound$ on !int! and the bound type of the class containing !R!.
 As such, a call to $unify(T, T_i, T_j)$ may touch every type class in $T$, not just $T_i$ and $T_j$, collapsing the entirety of $T$ into a single type class in extreme cases. 
+For more information on \CFA{} unification, see \cite{Bilson03}.
 The inverse of $unify$ is $split(T, T_i)$, which produces a new environment $T'$ which is the same as $T$ except that $T_i$ has been replaced by two classes corresponding to the arguments to the previous call to $unify$ on $T_i$. 
 If there has been no call to $unify$ on $T_i$ (\ie{} $T_i$ is a single-element class) $T_i$ is absent in $T'$.
@@ -58 +59 @@
 The invalid state of $T$ on failure is not important, given that a combination failure will result in the resolution algorithm backtracking to a different environment. 
 $combine$ proceeds by calls to $insert$, $add$, and $unify$ as needed, and can be roughly thought of as calling $unify$ on every pair of classes in $T$ that have variables $v'_{i,j}$ and $v'_{i,k}$ in the same class $T'_i$ in $T'$. 
-Like in $unify$, $combine$ can always find a mutually-consistent partition of type variables into classes (in the extreme case, all type variables from $T$ and $T'$ in a single type class), but may fail due to inconsistent bounds on merged type classes. 
+Like $unify$, $combine$ can always find a mutually-consistent partition of type variables into classes (in the extreme case, all type variables from $T$ and $T'$ in a single type class), but may fail due to inconsistent bounds on merged type classes. 
 
 Finally, the backtracking access patterns of the compiler can be exploited to reduce memory usage or runtime through use of an appropriately designed data structure. 
@@ -183 +184 @@
 In this section I present asymptotic analyses of the various approaches to a type environment data structure discussed in the previous section. 
 
+\begin{table}
+\caption[Type environment operation bounds]{Worst-case analysis of type environment operations. $n$ is the number of type classes, $m$ the maximum size of a type class, and $p$ the edit distance between two environments or a single environment and the empty environment; $u(n)$ captures the recursive cost of class unification.}
+\label{env-bounds-table}
+\centering
+\begin{tabular}{rllll}
+        \hline
+                                & \textbf{Na\"{\i}ve}   & \textbf{Incremental}  & \textbf{Union-Find}           & \textbf{U-F with Classes}             \\
+        \hline
+        $find$          & $O(n)$                                & $O(p)$                                & $O(\alpha(m))$                        & $O(\log m)$                                   \\
+        $report$        & $O(m)$                                & $O(m)$                                & $O(n \log m)$                         & $O(m)$                                                \\
+        $bound$         & $O(1)$                                & $O(1)$                                & $O(1)$                                        & $O(1)$                                                \\
+        $insert$        & $O(1)$                                & $O(1)$                                & $O(1)$                                        & $O(1)$                                                \\
+        $add$           & $O(1)$                                & $O(1)$                                & $O(1)$                                        & $O(1)$                                                \\
+        $bind$          & $O(1)$                                & $O(1)$                                & $O(1)$                                        & $O(1)$                                                \\
+        $unify$         & $O(m + u(n))$                 & $O(m + u(n))$                 & $O(\log m + u(n))$            & $O(\log m + u(n))$                    \\
+        $split$         & ---                                   & ---                                   & ---                                           & $O(\log m)$                                   \\
+        $combine$       & $O(nm \cdot u(n))$    & $O(pm \cdot u(n))$    & $O(n \log m \cdot u(n))$      & $O(p \log m \cdot u(n))$              \\
+        $save$          & $O(nm)$                               & $O(1)$                                & $O(nm)$                                       & $O(1)$                                                \\
+        $backtrack$     & $O(nm)$                               & $O(pm)$                               & $O(nm)$                                       & $O(p)$                                                \\
+        \hline
+\end{tabular}
+\end{table}
+
 % Future work: design multi-threaded version of C&F persistent map --- core idea is some sort of thread-boundary edit node