| 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 |
\begin{displaymath}
|
| 32 : |
|
|
\begin{array}{rclr}
|
| 33 : |
|
|
\nu & ::= & n & \text{dimension ($n > 0$)} \\
|
| 34 : |
|
|
& \mid & \phi & \text{dimension variable} \\
|
| 35 : |
|
|
\sigma & ::= & \epsilon & \text{empty sequence of dimensions} \\[1em]
|
| 36 : |
|
|
& \mid & \rho & \text{shape variable} \\
|
| 37 : |
|
|
& \mid & \sigma,\nu & \text{shape extension} \\[1em]
|
| 38 : |
|
|
\kappa & ::= & n & \text{$n$ levels of differentiation ($n \geq 0$)} \\
|
| 39 : |
|
|
& \mid & \kappa-n & \text{}
|
| 40 : |
|
|
\end{array}
|
| 41 : |
|
|
\end{displaymath}%
|
| 42 : |
|
|
|
| 43 : |
jhr |
64 |
The syntax of Diderot types is given in \figref{fig:types}.
|
| 44 : |
|
|
\begin{figure}[t]
|
| 45 : |
|
|
\begin{displaymath}
|
| 46 : |
|
|
\begin{array}{rclr}
|
| 47 : |
jhr |
66 |
\tau & ::= & \TYconst & \text{type constants} \\
|
| 48 : |
jhr |
64 |
& \mid & \theta \\
|
| 49 : |
jhr |
66 |
% & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\
|
| 50 : |
|
|
& \mid & \TYimage{\nu}{\sigma} & \text{$d$-dimension image of $\mu$ values}\\
|
| 51 : |
jhr |
64 |
& \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\
|
| 52 : |
jhr |
66 |
& \mid & \TYfield{k}{\nu}{\sigma} & \text{field} \\
|
| 53 : |
jhr |
64 |
\sigma & ::= \
|
| 54 : |
|
|
\end{array}%
|
| 55 : |
|
|
\end{displaymath}%
|
| 56 : |
|
|
where $o\in\Nat$ is the tensor order, $d,n,m\in\SET{2,3}$ are dimensions,
|
| 57 : |
|
|
and $k\in\Nat$ is the differentiability of a field.
|
| 58 : |
|
|
\caption{Diderot types}
|
| 59 : |
|
|
\label{fig:types}
|
| 60 : |
|
|
\end{figure}%
|
| 61 : |
|
|
|
| 62 : |
|
|
\end{document}
|
Parent Directory
| 
Revision Log
