28 |
This document looks at the rules for typechecking Diderot. |
This document looks at the rules for typechecking Diderot. |
29 |
|
|
30 |
\section{Types} |
\section{Types} |
|
\begin{displaymath} |
|
|
\begin{array}{rclr} |
|
|
\nu & ::= & n & \text{dimension ($n > 0$)} \\ |
|
|
& \mid & \phi & \text{dimension variable} \\ |
|
|
\sigma & ::= & \epsilon & \text{empty sequence of dimensions} \\[1em] |
|
|
& \mid & \rho & \text{shape variable} \\ |
|
|
& \mid & \sigma,\nu & \text{shape extension} \\[1em] |
|
|
\kappa & ::= & n & \text{$n$ levels of differentiation ($n \geq 0$)} \\ |
|
|
& \mid & \kappa-n & \text{} |
|
|
\end{array} |
|
|
\end{displaymath}% |
|
31 |
|
|
32 |
The syntax of Diderot types is given in \figref{fig:types}. |
The syntax of Diderot types is given in \figref{fig:types}. |
33 |
\begin{figure}[t] |
\begin{figure}[t] |
34 |
\begin{displaymath} |
\begin{displaymath} |
35 |
\begin{array}{rclr} |
\begin{array}{rclr} |
36 |
\tau & ::= & \TYconst & \text{type constants} \\ |
\tau & ::= & \TYconst & \text{type constants} \\ |
37 |
& \mid & \theta \\ |
& \mid & \TYtensor{\sigma} \\ |
38 |
% & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\ |
% & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\ |
39 |
& \mid & \TYimage{\nu}{\sigma} & \text{$d$-dimension image of $\mu$ values}\\ |
& \mid & \TYimage{d}{s} & \text{$d$-dimension image of $s$-shaped values}\\ |
40 |
& \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\ |
& \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\ |
41 |
& \mid & \TYfield{k}{\nu}{\sigma} & \text{field} \\ |
& \mid & \TYfield{k}{d}{s} & \text{field} \\[1em] |
42 |
\sigma & ::= \ |
d & ::= & n & \text{dimension ($n > 0$)} \\ |
43 |
|
& \mid & \phi & \text{dimension variable} \\[1em] |
44 |
|
s & ::= & \epsilon & \text{empty sequence of dimensions} \\ |
45 |
|
& \mid & \rho & \text{shape variable} \\ |
46 |
|
& \mid & sd & \text{shape extension} \\[1em] |
47 |
|
k & ::= & n & \text{$n$ levels of differentiation ($n \geq 0$)} \\ |
48 |
|
& \mid & \kappa-n & \text{$\kappa-n$ levels of differentiation ($\kappa \geq n$ and $n \geq 0$)} |
49 |
\end{array}% |
\end{array}% |
50 |
\end{displaymath}% |
\end{displaymath}% |
|
where $o\in\Nat$ is the tensor order, $d,n,m\in\SET{2,3}$ are dimensions, |
|
|
and $k\in\Nat$ is the differentiability of a field. |
|
51 |
\caption{Diderot types} |
\caption{Diderot types} |
52 |
\label{fig:types} |
\label{fig:types} |
53 |
\end{figure}% |
\end{figure}% |
54 |
|
|
55 |
|
\section{Unification} |
56 |
|
Unification of dimensions: |
57 |
|
\begin{eqnarray*} |
58 |
|
\U{n}{n} & = & \emptyset \\ |
59 |
|
\U{\phi}{\phi'} & = & \MAP{\phi}{\phi'} \\ |
60 |
|
\U{\phi}{n} & = & \MAP{\phi}{n} \\ |
61 |
|
\U{n}{\phi} & = & \MAP{\phi}{n} |
62 |
|
\end{eqnarray*}% |
63 |
|
|
64 |
|
\noindent |
65 |
|
Unification of shapes: |
66 |
|
\begin{eqnarray*} |
67 |
|
\U{\epsilon}{\epsilon} & = & \emptyset \\ |
68 |
|
\U{\rho}{\rho'} & = & \MAP{\rho}{\rho'} \\ |
69 |
|
\U{sd}{s'd'} & = & \text{$\U{S(s)}{S(s')}\cup{}S$, where $S = \U{d}{d'}$} \\ |
70 |
|
\U{\rho}{s} & = & \text{$\MAP{\rho}{s}$, where $\rho\not\in{}s$} \\ |
71 |
|
\U{s}{\rho} & = & \text{$\MAP{\rho}{s}$, where $\rho\not\in{}s$} |
72 |
|
\end{eqnarray*}% |
73 |
|
|
74 |
|
\noindent |
75 |
|
Unification of differentiation levels: |
76 |
|
\begin{eqnarray*} |
77 |
|
\U{n}{n} & = & \emptyset \\ |
78 |
|
\U{\kappa}{\kappa'} & = & \MAP{\kappa}{\kappa'} \\ |
79 |
|
\U{\kappa-n}{\kappa'-n'} & = & \left\{\begin{array}{ll} |
80 |
|
\MAP{\kappa}{\kappa'-(n'-n)} & \text{if $n < n'$} \\ |
81 |
|
\MAP{\kappa}{\kappa'} & \text{if $n = n'$} \\ |
82 |
|
\MAP{\kappa}{\kappa-(n-n')} & \text{if $n > n'$} |
83 |
|
\end{array}\right. |
84 |
|
\end{eqnarray*}% |
85 |
|
|
86 |
\end{document} |
\end{document} |