Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] Diff of /trunk/doc/typing/typing.tex
ViewVC logotype

Diff of /trunk/doc/typing/typing.tex

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 66, Thu May 13 23:12:28 2010 UTC revision 67, Fri May 14 14:11:21 2010 UTC
# Line 28  Line 28 
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}

Legend:
Removed from v.66  
changed lines
  Added in v.67

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0