prolog.tex

@@ -121,8 +121,8 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
-%\newcommand{\ntv}[1]{\tv{#1}}
+\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

unify.tex

@@ -146,28 +146,21 @@ The \unify{} algorithm internally uses the following data types:
 The algorithm is split into multiple parts:
 \begin{description}
 \item[Step 1:]
-Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
+Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively.
-starting with the \rulename{circle} rule.
+Starting with the \rulename{circle} rule.
 
 \item[Step 2:]
 %If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
 %resume with step 4.
 
-The second step is nondeterministic.
+The rules in figure \ref{fig:step2-rules} offer multiple possibilities to deal with constraints of the form $\type{N} \lessdot \tv{a}$.
-%\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
+This builds a search tree over multiple possible solutions.
-%The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
+\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
-For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
-The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
-%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
-If atleast one transformation was applied in this step revert to step 1.
-Otherwise proceed with step 3.
-%This builds a search tree over multiple possible solutions.
-%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
 
-%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
+$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
 
 \item[Step 3:]
-Apply the rules in figure \ref{fig:cleanup-rules} exhaustively and move on with step 4.
+We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 4.
 
 \item[Step 4:] \textit{(Generating Result)} 
 Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
@@ -270,12 +263,6 @@ To only rename the respective wildcards the reduce rule renames wildcards up to
 \item[Free Variables:]
 The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
 % TODO: describe a function which determines free variables? or do an example?
-\begin{align*}
-\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
-\text{fv}(\ntv{a}) &= \emptyset \\
-\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
-\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
-\end{align*}
 
 \item[Fresh Wildcards:]
 $\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
@@ -458,11 +445,11 @@ $
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \vdash C 
-    \end{array} 
+    \end{array}
     $
-    \quad
+    \\\\
     \rulename{Pit}
-    $
+    & $
     \begin{array}[c]{l}
     \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ 
     \hline
@@ -543,7 +530,10 @@ $
         \vspace*{-0.4cm}\\
         \wildcardEnv \vdash C
     \end{array}
-    \quad
+    $
+    \\\\
+    \rulename{Erase}
+    & $
     \begin{array}[c]{l}
         \wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\ 
         \hline
@@ -980,7 +970,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
 }
     \end{center}
   \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
-  \label{fig:step2-rules2}
+  \label{fig:step2-rules}
   \end{figure}
 
 \begin{figure}