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

Parent Directory | Revision Log | 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}

---

Colored Diff Long Colored Diff Unidiff Context Diff Side by Side

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