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

SCM Repository

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

Annotation of /trunk/doc/typing/typing.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 67 - (view) (download) (as text)

1 : jhr 64 \documentclass[11pt]{article}
2 :    
3 :     \input{defs}
4 :    
5 :     \setlength{\textwidth}{6in}
6 :     \setlength{\oddsidemargin}{0.25in}
7 :     \setlength{\evensidemargin}{0.25in}
8 :     \setlength{\parskip}{5pt}
9 :    
10 :     \title{Typechecking Diderot}
11 :     \author{
12 :     Gordon Kindlmann \\
13 :     University of Chicago \\
14 :     {\small\tt{}glk@cs.uchicago.edu} \\
15 :     \and
16 :     John Reppy \\
17 :     University of Chicago \\
18 :     {\small\tt{}jhr@cs.uchicago.edu} \\
19 :     }
20 :     \date{\today}
21 :    
22 :     \begin{document}
23 :    
24 :     \maketitle
25 :     \thispagestyle{empty}
26 :    
27 :     \section{Introduction}
28 :     This document looks at the rules for typechecking Diderot.
29 :    
30 :     \section{Types}
31 : jhr 66
32 : jhr 64 The syntax of Diderot types is given in \figref{fig:types}.
33 :     \begin{figure}[t]
34 :     \begin{displaymath}
35 :     \begin{array}{rclr}
36 : jhr 66 \tau & ::= & \TYconst & \text{type constants} \\
37 : jhr 67 & \mid & \TYtensor{\sigma} \\
38 : jhr 66 % & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\
39 : jhr 67 & \mid & \TYimage{d}{s} & \text{$d$-dimension image of $s$-shaped values}\\
40 : jhr 64 & \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\
41 : jhr 67 & \mid & \TYfield{k}{d}{s} & \text{field} \\[1em]
42 :     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 : jhr 64 \end{array}%
50 :     \end{displaymath}%
51 :     \caption{Diderot types}
52 :     \label{fig:types}
53 :     \end{figure}%
54 :    
55 : jhr 67 \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 : jhr 64 \end{document}

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