Index: doc/working/.gitignore
===================================================================
--- doc/working/.gitignore	(revision a64644c8182e47ed436d2d8d7dd8ea0e08ce8362)
+++ doc/working/.gitignore	(revision a64644c8182e47ed436d2d8d7dd8ea0e08ce8362)
@@ -0,0 +1,4 @@
+.declarative_resolver.tex.swp
+declarative_resolver.aux
+declarative_resolver.log
+declarative_resolver.pdf
Index: doc/working/declarative_resolver.tex
===================================================================
--- doc/working/declarative_resolver.tex	(revision a64644c8182e47ed436d2d8d7dd8ea0e08ce8362)
+++ doc/working/declarative_resolver.tex	(revision a64644c8182e47ed436d2d8d7dd8ea0e08ce8362)
@@ -0,0 +1,172 @@
+\documentclass{article}
+
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+\usepackage{listings}
+\lstset{
+  basicstyle=\ttfamily,
+  mathescape
+}
+
+\newcommand{\TODO}{\textbf{TODO:}~}
+\newcommand{\NOTE}{\textit{NOTE:}~}
+
+\newcommand{\Z}{\mathbb{Z}}
+\newcommand{\Znn}{\Z^{\oplus}}
+
+\newcommand{\conv}[2]{#1 \rightarrow #2}
+\newcommand{\C}[1]{\mathtt{#1}}
+
+\newcommand{\ls}[1]{\left[ #1 \right]}
+\newcommand{\rng}[2]{\left\{#1, \cdots #2\right\}}
+\title{Declarative Description of Expression Resolution Problem}
+\author{Aaron Moss}
+
+\begin{document}
+\maketitle
+
+\section{Inputs}
+\begin{itemize}
+\item A set of types $T$.
+\item A set of conversions $C \subset \{ \conv{from}{to} : from, to \in T \}$.
+  \begin{itemize}
+  \item $C$ is a directed acyclic graph (DAG).
+  \item \TODO There should be two of these, to separate the safe and unsafe conversions.
+  \end{itemize}
+\item A set of names $N$
+\item A set of declarations $F$. Each declaration $f \in F$ has the following properties:
+  \begin{itemize}
+  \item A name $f.name \in N$, not guaranteed to be unqiue in $F$.
+  \item A return type $f.type \in T$
+  \item A number of parameters $f.n \in \Znn$.
+  \item A list of parameter types $params = \ls{f_1, \cdots f_{f.n}}$, where each $f_i \in T$. 
+    \begin{itemize}
+    \item \TODO This should be a list of elements from $T$ to account for tuples and void-returning functions.
+    \end{itemize}
+  \item \TODO This model needs to account for polymorphic functions.
+  \end{itemize}
+\item A tree of expressions $E$, rooted at an expression $root$. Each expression $e \in E$ has the following properties:
+  \begin{itemize}
+  \item A name $e.name \in N$, not guaranteed to be unique in $E$
+  \item A number of arguments $e.n \in \Znn$
+  \item A list of arguments $args = \ls{e_1, \cdots e_{e.n}}$, where each $e_i \in E$; these arguments $e_i$ are considered the children of $e$ in the tree.
+  \end{itemize}
+\end{itemize}
+
+\section{Problem}
+An interpretation $x \in I$ has the following properties:
+\begin{itemize}
+\item An interpreted expression $x.expr \in E$.
+\item A base declaration $x.decl \in F$.
+\item A type $x.type \in T$
+\item A cost $x.cost \in \Znn$.
+  \begin{itemize}
+  \item \TODO Make this cost a tuple containing unsafe and polymorphic conversion costs later.
+  \end{itemize}
+\item A number of sub-interpretations $x.n \in \Znn$.
+\item A list of sub-interpretations $subs = \ls{x_1, \cdots x_{x.n}}$, where each $x_i \in I$.
+\end{itemize}
+
+Starting from $I = \{\}$, iteratively generate interpretations according to the following rules until a fixed point is reached:
+\begin{itemize}
+\item \textbf{Generate all interpretations, given subexpression interpretations.} \\
+      $\forall e \in E, f \in F$ such that $e.name = f.name$ and $e.n = f.n$, let $n = e.n$. \\
+      If $\forall i \in \rng{1}{n}, \exists x_i \in I$ such that $x_i.expr = e_i \land x_i.type = f_i$, \\
+      For each combination of $x_i$, generate a new interpretation $x$ as follows:
+      \begin{itemize}
+      \item $x.expr = e$.
+      \item $x.decl = f$.
+      \item $x.type = f.type$.
+      \item $x.cost = \sum_{i \in \rng{1}{n}} x_i.cost$.
+      \item $x.n = n$.
+      \end{itemize}
+
+\item \textbf{Generate conversions.} \\
+      $\forall x \in I, \forall t \in T, \exists (x.type, t) \in C$, \\
+      generate a new interpretation $x'$ as follows:
+      \begin{itemize}
+      \item $x'.type = t$.
+      \item $x'.cost = x.cost + 1$.
+      \item All other properties of $x'$ are identical to those of $x$.
+      \end{itemize}
+\end{itemize}
+
+
+Once $I$ has been completely generated, let $I' = { x \in I : x.expr = root }$.
+\begin{itemize}
+\item If $I' = \{\}$, report failure (no valid interpretation).
+\item If there exists a unqiue $x^* \in I'$ such that $x^*.cost$ is minimal in $I'$, report $x^*$ (success).
+\item Otherwise report failure (ambiguous).
+\end{itemize}
+
+\section{Example}
+
+Here is a worked example for the following C code block:
+\begin{lstlisting}
+int x;  // $x$
+void* x;  // $x'$
+
+long f(int, void*);  // $f$
+void* f(void*, int);  // $f'$
+void* f(void*, long);  // $f''$
+
+f( f( x, x ), x );  // $root:$f( $\gamma:$f( $\alpha:$x, $\beta:$x ), $\delta:$x )
+\end{lstlisting}
+
+Using the following subset of the C type system, this example includes the following set of declarations and expressions\footnote{$n$ can be inferred from the length of the appropriate list in the elements of $F$, $E$, and $I$, and has been ommitted for brevity.}:
+\begin{align*}
+  T = \{ &\C{int}, \C{long}, \C{void*} \} \\
+  C = \{ &\conv{\C{int}}{\C{long}} \} \\
+  N = \{ &\C{x}, \C{f} \} \\
+  F = \{ &x = \{ name: \C{x}, type: \C{int}, params: \ls{} \}, \\
+         &x' = \{ name: \C{x}, type: \C{void*}, params: \ls{} \}, \\
+         &f = \{ name: \C{f}, type: \C{long}, params: \ls{\C{int}, \C{void*}} \}, \\
+         &f' = \{ name: \C{f}, type: \C{void*}, params: \ls{\C{void*}, \C{int}} \}, \\
+         &f'' = \{ name: \C{f}, type: \C{void*}, params: \ls{\C{void*}, \C{long}} \} \} \\
+  E = \{ &\alpha = \{ name: \C{x}, args: \ls{} \}, \\
+         &\beta = \{ name: \C{x}, args: \ls{} \}, \\
+         &\gamma = \{ name: \C{f}, args: \ls{\alpha, \beta} \}, \\
+         &\delta = \{ name: \C{x}, args: \ls{} \}, \\
+         &root = \{ name: \C{f}, args: \ls{\gamma, \delta} \} \}
+\end{align*}
+
+Given these initial facts, the initial interpretations for the leaf expressions $\alpha$, $\beta$ \& $\delta$ can be generated from the subexpression rule:
+\begin{align}
+ \{ &expr: \alpha, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
+ \{ &expr: \alpha, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \} \\
+ \{ &expr: \beta, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
+ \{ &expr: \beta, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \} \\
+ \{ &expr: \delta, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
+ \{ &expr: \delta, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \}
+\end{align}
+
+These new interpretations allow generation of further interpretations by the conversion rule and the $\conv{\C{int}}{\C{long}}$ conversion:
+\begin{align}
+\{ &expr: \alpha, decl: x, type: \C{long}, cost: 1, subs: \ls{} \} \\
+\{ &expr: \beta, decl: x, type: \C{long}, cost: 1, subs: \ls{} \} \\
+\{ &expr: \delta, decl: x, type: \C{long}, cost: 1, subs: \ls{} \}
+\end{align}
+
+Applying the subexpression rule again to this set of interpretations, we can generate interpretations for $\gamma$ [$\C{f( x, x )}$]:
+\begin{align}
+\{ &expr: \gamma, decl: f, type: \C{long}, cost: 0, subs: \ls{ (1), (4) } \} \\
+\{ &expr: \gamma, decl: f', type: \C{void*}, cost: 0, subs: \ls{ (2), (3) } \} \\
+\{ &expr: \gamma, decl: f'', type: \C{void*}, cost: 1, subs: \ls{ (2), (8) } \}
+\end{align}
+
+Since all of the new interpretations have types for which no conversions are applicable ($\C{void*}$ and $\C{long}$), the conversion rule generates no new interpretations.
+If $\C{f(x, x)}$ was the root expression, the set of candidate interpretations $I'$ would equal $\{ (10), (11), (12) \}$. Since both $(10)$ and $(11)$ have cost $0$, there is no unique minimal-cost element of this set, and the resolver would report failure due to this ambiguity.
+
+However, having generated all the interpretations of $\C{f( x, x )}$, the subexpression rule can now be applied again to generate interpretations of the $root$ expression:
+\begin{align}
+\{ &expr: root, decl: f', type: \C{void*}, cost: 0, subs: \ls{ (11), (5) } \} \\
+\{ &expr: root, decl: f'', type: \C{void*}, cost: 1, subs: \ls{ (11), (9) } \} \\
+\{ &expr: root, decl: f', type: \C{void*}, cost: 1, subs: \ls{ (12), (5) } \} \\
+\{ &expr: root, decl: f'', type: \C{void*}, cost: 2, subs: \ls{ (12), (9) } \}
+\end{align}
+
+Since again none of these new interpretations are of types with conversions defined, the conversion rule cannot be applied again; since the root expression has been resolved, no further applications of the subexpression rule are applicable either, therefore a fixed point has been reached and we have found the complete set of interpretations. If this fixed point had been reached before finding any valid interpretations of $root$ (e.g.~as would have happened if $f$ was the only declaration of $\C{f}$ in the program), the algorithm would have reported a failure with no valid interpretations.
+
+At the termination of this process, the set $I'$ of valid root interpretations is $\{ (13), (14), (15), (16)\}$; since $(13)$ has the unique minimal cost, it is the accepted interpretation of the root expression, and in this case the source $\C{f( f( x, x ), x )}$ is interpreted as $f'( f'( x', x ), x )$.
+\end{document}