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

Parent Directory | 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