source: doc/working/declarative_resolver.tex @ 37e9c1d

ADTast-experimentalenumpthread-emulationqualifiedEnum
Last change on this file since 37e9c1d was 40744af8, checked in by Aaron Moss <a3moss@…>, 8 years ago

Add working doc with start of declarative description of resolver

  • Property mode set to 100644
File size: 8.3 KB
Line 
1\documentclass{article}
2
3\usepackage{amsmath}
4\usepackage{amssymb}
5
6\usepackage{listings}
7\lstset{
8  basicstyle=\ttfamily,
9  mathescape
10}
11
12\newcommand{\TODO}{\textbf{TODO:}~}
13\newcommand{\NOTE}{\textit{NOTE:}~}
14
15\newcommand{\Z}{\mathbb{Z}}
16\newcommand{\Znn}{\Z^{\oplus}}
17
18\newcommand{\conv}[2]{#1 \rightarrow #2}
19\newcommand{\C}[1]{\mathtt{#1}}
20
21\newcommand{\ls}[1]{\left[ #1 \right]}
22\newcommand{\rng}[2]{\left\{#1, \cdots #2\right\}}
23\title{Declarative Description of Expression Resolution Problem}
24\author{Aaron Moss}
25
26\begin{document}
27\maketitle
28
29\section{Inputs}
30\begin{itemize}
31\item A set of types $T$.
32\item A set of conversions $C \subset \{ \conv{from}{to} : from, to \in T \}$.
33  \begin{itemize}
34  \item $C$ is a directed acyclic graph (DAG).
35  \item \TODO There should be two of these, to separate the safe and unsafe conversions.
36  \end{itemize}
37\item A set of names $N$
38\item A set of declarations $F$. Each declaration $f \in F$ has the following properties:
39  \begin{itemize}
40  \item A name $f.name \in N$, not guaranteed to be unqiue in $F$.
41  \item A return type $f.type \in T$
42  \item A number of parameters $f.n \in \Znn$.
43  \item A list of parameter types $params = \ls{f_1, \cdots f_{f.n}}$, where each $f_i \in T$.
44    \begin{itemize}
45    \item \TODO This should be a list of elements from $T$ to account for tuples and void-returning functions.
46    \end{itemize}
47  \item \TODO This model needs to account for polymorphic functions.
48  \end{itemize}
49\item A tree of expressions $E$, rooted at an expression $root$. Each expression $e \in E$ has the following properties:
50  \begin{itemize}
51  \item A name $e.name \in N$, not guaranteed to be unique in $E$
52  \item A number of arguments $e.n \in \Znn$
53  \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.
54  \end{itemize}
55\end{itemize}
56
57\section{Problem}
58An interpretation $x \in I$ has the following properties:
59\begin{itemize}
60\item An interpreted expression $x.expr \in E$.
61\item A base declaration $x.decl \in F$.
62\item A type $x.type \in T$
63\item A cost $x.cost \in \Znn$.
64  \begin{itemize}
65  \item \TODO Make this cost a tuple containing unsafe and polymorphic conversion costs later.
66  \end{itemize}
67\item A number of sub-interpretations $x.n \in \Znn$.
68\item A list of sub-interpretations $subs = \ls{x_1, \cdots x_{x.n}}$, where each $x_i \in I$.
69\end{itemize}
70
71Starting from $I = \{\}$, iteratively generate interpretations according to the following rules until a fixed point is reached:
72\begin{itemize}
73\item \textbf{Generate all interpretations, given subexpression interpretations.} \\
74      $\forall e \in E, f \in F$ such that $e.name = f.name$ and $e.n = f.n$, let $n = e.n$. \\
75      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$, \\
76      For each combination of $x_i$, generate a new interpretation $x$ as follows:
77      \begin{itemize}
78      \item $x.expr = e$.
79      \item $x.decl = f$.
80      \item $x.type = f.type$.
81      \item $x.cost = \sum_{i \in \rng{1}{n}} x_i.cost$.
82      \item $x.n = n$.
83      \end{itemize}
84
85\item \textbf{Generate conversions.} \\
86      $\forall x \in I, \forall t \in T, \exists (x.type, t) \in C$, \\
87      generate a new interpretation $x'$ as follows:
88      \begin{itemize}
89      \item $x'.type = t$.
90      \item $x'.cost = x.cost + 1$.
91      \item All other properties of $x'$ are identical to those of $x$.
92      \end{itemize}
93\end{itemize}
94
95
96Once $I$ has been completely generated, let $I' = { x \in I : x.expr = root }$.
97\begin{itemize}
98\item If $I' = \{\}$, report failure (no valid interpretation).
99\item If there exists a unqiue $x^* \in I'$ such that $x^*.cost$ is minimal in $I'$, report $x^*$ (success).
100\item Otherwise report failure (ambiguous).
101\end{itemize}
102
103\section{Example}
104
105Here is a worked example for the following C code block:
106\begin{lstlisting}
107int x;  // $x$
108void* x;  // $x'$
109
110long f(int, void*);  // $f$
111void* f(void*, int);  // $f'$
112void* f(void*, long);  // $f''$
113
114f( f( x, x ), x );  // $root:$f( $\gamma:$f( $\alpha:$x, $\beta:$x ), $\delta:$x )
115\end{lstlisting}
116
117Using 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.}:
118\begin{align*}
119  T = \{ &\C{int}, \C{long}, \C{void*} \} \\
120  C = \{ &\conv{\C{int}}{\C{long}} \} \\
121  N = \{ &\C{x}, \C{f} \} \\
122  F = \{ &x = \{ name: \C{x}, type: \C{int}, params: \ls{} \}, \\
123         &x' = \{ name: \C{x}, type: \C{void*}, params: \ls{} \}, \\
124         &f = \{ name: \C{f}, type: \C{long}, params: \ls{\C{int}, \C{void*}} \}, \\
125         &f' = \{ name: \C{f}, type: \C{void*}, params: \ls{\C{void*}, \C{int}} \}, \\
126         &f'' = \{ name: \C{f}, type: \C{void*}, params: \ls{\C{void*}, \C{long}} \} \} \\
127  E = \{ &\alpha = \{ name: \C{x}, args: \ls{} \}, \\
128         &\beta = \{ name: \C{x}, args: \ls{} \}, \\
129         &\gamma = \{ name: \C{f}, args: \ls{\alpha, \beta} \}, \\
130         &\delta = \{ name: \C{x}, args: \ls{} \}, \\
131         &root = \{ name: \C{f}, args: \ls{\gamma, \delta} \} \}
132\end{align*}
133
134Given these initial facts, the initial interpretations for the leaf expressions $\alpha$, $\beta$ \& $\delta$ can be generated from the subexpression rule:
135\begin{align}
136 \{ &expr: \alpha, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
137 \{ &expr: \alpha, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \} \\
138 \{ &expr: \beta, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
139 \{ &expr: \beta, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \} \\
140 \{ &expr: \delta, decl: x, type: \C{int}, cost: 0, subs: \ls{} \} \\
141 \{ &expr: \delta, decl: x', type: \C{void*}, cost: 0, subs: \ls{} \}
142\end{align}
143
144These new interpretations allow generation of further interpretations by the conversion rule and the $\conv{\C{int}}{\C{long}}$ conversion:
145\begin{align}
146\{ &expr: \alpha, decl: x, type: \C{long}, cost: 1, subs: \ls{} \} \\
147\{ &expr: \beta, decl: x, type: \C{long}, cost: 1, subs: \ls{} \} \\
148\{ &expr: \delta, decl: x, type: \C{long}, cost: 1, subs: \ls{} \}
149\end{align}
150
151Applying the subexpression rule again to this set of interpretations, we can generate interpretations for $\gamma$ [$\C{f( x, x )}$]:
152\begin{align}
153\{ &expr: \gamma, decl: f, type: \C{long}, cost: 0, subs: \ls{ (1), (4) } \} \\
154\{ &expr: \gamma, decl: f', type: \C{void*}, cost: 0, subs: \ls{ (2), (3) } \} \\
155\{ &expr: \gamma, decl: f'', type: \C{void*}, cost: 1, subs: \ls{ (2), (8) } \}
156\end{align}
157
158Since 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.
159If $\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.
160
161However, 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:
162\begin{align}
163\{ &expr: root, decl: f', type: \C{void*}, cost: 0, subs: \ls{ (11), (5) } \} \\
164\{ &expr: root, decl: f'', type: \C{void*}, cost: 1, subs: \ls{ (11), (9) } \} \\
165\{ &expr: root, decl: f', type: \C{void*}, cost: 1, subs: \ls{ (12), (5) } \} \\
166\{ &expr: root, decl: f'', type: \C{void*}, cost: 2, subs: \ls{ (12), (9) } \}
167\end{align}
168
169Since 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.
170
171At 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 )$.
172\end{document}
Note: See TracBrowser for help on using the repository browser.