Home My Page Projects Code Snippets Project Openings diderot

SCM Repository

[diderot] View of /trunk/doc/typing/typing.tex
 [diderot] / trunk / doc / typing / typing.tex

View of /trunk/doc/typing/typing.tex

Fri May 14 14:11:21 2010 UTC (11 years, 6 months ago) by jhr
File size: 2683 byte(s)
Working on Diderot typing note
\documentclass[11pt]{article}

\input{defs}

\setlength{\textwidth}{6in}
\setlength{\oddsidemargin}{0.25in}
\setlength{\evensidemargin}{0.25in}
\setlength{\parskip}{5pt}

\title{Typechecking Diderot}
\author{
Gordon Kindlmann \\
University of Chicago \\
{\small\tt{}glk@cs.uchicago.edu} \\
\and
John Reppy \\
University of Chicago \\
{\small\tt{}jhr@cs.uchicago.edu} \\
}
\date{\today}

\begin{document}

\maketitle
\thispagestyle{empty}

\section{Introduction}
This document looks at the rules for typechecking Diderot.

\section{Types}

The syntax of Diderot types is given in \figref{fig:types}.
\begin{figure}[t]
\begin{displaymath}
\begin{array}{rclr}
\tau & ::= & \TYconst & \text{type constants} \\
& \mid & \TYtensor{\sigma} \\
%           & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\
& \mid & \TYimage{d}{s} & \text{$d$-dimension image of $s$-shaped values}\\
& \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\
& \mid & \TYfield{k}{d}{s} & \text{field} \\[1em]
d    & ::=  & n & \text{dimension ($n > 0$)} \\
& \mid & \phi & \text{dimension variable} \\[1em]
s    & ::=  & \epsilon & \text{empty sequence of dimensions} \\
& \mid & \rho & \text{shape variable} \\
& \mid & sd & \text{shape extension} \\[1em]
k    & ::=  & n & \text{$n$ levels of differentiation ($n \geq 0$)} \\
& \mid & \kappa-n & \text{$\kappa-n$ levels of differentiation ($\kappa \geq n$ and $n \geq 0$)}
\end{array}%
\end{displaymath}%
\caption{Diderot types}
\label{fig:types}
\end{figure}%

\section{Unification}
Unification of dimensions:
\begin{eqnarray*}
\U{n}{n} & = & \emptyset \\
\U{\phi}{\phi'} & = & \MAP{\phi}{\phi'} \\
\U{\phi}{n} & = & \MAP{\phi}{n} \\
\U{n}{\phi} & = & \MAP{\phi}{n}
\end{eqnarray*}%

\noindent
Unification of shapes:
\begin{eqnarray*}
\U{\epsilon}{\epsilon} & = & \emptyset \\
\U{\rho}{\rho'} & = & \MAP{\rho}{\rho'} \\
\U{sd}{s'd'} & = & \text{$\U{S(s)}{S(s')}\cup{}S$, where $S = \U{d}{d'}$} \\
\U{\rho}{s} & = & \text{$\MAP{\rho}{s}$, where $\rho\not\in{}s$} \\
\U{s}{\rho} & = & \text{$\MAP{\rho}{s}$, where $\rho\not\in{}s$}
\end{eqnarray*}%

\noindent
Unification of differentiation levels:
\begin{eqnarray*}
\U{n}{n} & = & \emptyset \\
\U{\kappa}{\kappa'} & = & \MAP{\kappa}{\kappa'} \\
\U{\kappa-n}{\kappa'-n'} & = & \left\{\begin{array}{ll}
\MAP{\kappa}{\kappa'-(n'-n)} & \text{if $n < n'$} \\
\MAP{\kappa}{\kappa'} & \text{if $n = n'$} \\
\MAP{\kappa}{\kappa-(n-n')} & \text{if $n > n'$}
\end{array}\right.
\end{eqnarray*}%

\end{document}