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} |
---|
58 | An 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 | |
---|
71 | Starting 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 | |
---|
96 | Once $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 | |
---|
105 | Here is a worked example for the following C code block: |
---|
106 | \begin{lstlisting} |
---|
107 | int x; // $x$ |
---|
108 | void* x; // $x'$ |
---|
109 | |
---|
110 | long f(int, void*); // $f$ |
---|
111 | void* f(void*, int); // $f'$ |
---|
112 | void* f(void*, long); // $f''$ |
---|
113 | |
---|
114 | f( f( x, x ), x ); // $root:$f( $\gamma:$f( $\alpha:$x, $\beta:$x ), $\delta:$x ) |
---|
115 | \end{lstlisting} |
---|
116 | |
---|
117 | 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.}: |
---|
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 | |
---|
134 | Given 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 | |
---|
144 | These 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 | |
---|
151 | Applying 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 | |
---|
158 | 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. |
---|
159 | 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. |
---|
160 | |
---|
161 | 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: |
---|
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 | |
---|
169 | 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. |
---|
170 | |
---|
171 | 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 )$. |
---|
172 | \end{document} |
---|