\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}