
\documentstyle[12pt]{article}
\input mssymb                                 
\input /jj/kt/tex/fixqmsfonts
\input /jj/kt/tex/laktex
\input /jj/kt/tex/illustrations
\input /var/arvind/idcompiler/macros/prelude


\pagestyle{empty}

\begin{document}



\subsection*{$\delta$ rules}
{\large
\[ \begin{array}{lcl}
+ \; (\underline{m}, \;  \underline{n}) & \reduce{\delta}{}
& \underline{+ (m,\;  n)} \\
& \vdots & 
\end{array} \]
}

\newpage

\subsection*{Conditional rule}
{\large
\[ \begin{array}{lll}
\hspace{0.5cm}{\sf Dispatch_{n,m}} \; (\underline{i} , \;
\mv{E_{i-1}} , \; E_i, \; \mv{E_{i+1,n}})   &
\reduce{}{} & E_i 
\end{array} \]
}

\newpage

\subsection*{I\_structure rules }
{\large
\[\begin{array}{lll}
{\sf Allocate} \;\;(\underline{n}) & \reduce{}{} & L
\end{array} \]
}

{\large
\[ \begin{array}{l}
\frag{{\sf P\_store} \; (L, \; \underline{i},\; V)}
{ {\sf P\_select} \;(L, \; \underline{i}) \;\;\;
\reduce{}{}\;\;\; V }
\end{array} \]
}

{\large
\[ \begin{array}{l}
\frag{{\sf P\_store} \; (L, \; \underline{i},\; V)}
{ {\sf P\_store} \; (L,\;\underline{i}, \;V^{'})  \;\;
\reduce{}{}\;\; {\sf \top_s} }
\end{array} \]
}

\newpage

\subsection*{Application rule}
{\large
\[\begin{array}{l}
\frag{F = {\sf \lambda_{n,m}} \; (\mv{Z_n}) \; . \;  (E) }
{{\sf Ap_{n,m}} \; (F, \; \mv{X_n}) \;\; \reduce{}{} \;\; 
({\tt RB}[\![E]\!]) \; [\mv{X_n}/\mv{Z_n} ] }\\
\end{array}\]
}

\newpage
 
\subsection*{Loop rules} 
{\large
\[\begin{array}{lll}
{\sf WLoop_n} \; (P, \; B, \; \mv{X_n}, \; {\sf True}) & \reduce{}{} & \{_{\sf n} \begin{array}[t]{lll}
 \mv{t_n} & = & {\sf Ap_{n,n}} \; (B, \;  \mv{X_n}) ;\\
 t_{p} & = & {\sf Ap_n} \; (P, \; \mv{t_n});\\
\mv{t_n'} & = & {\sf WLoop_n} \;(P,  \; B,   \; \mv{t_n},\; t_{p})  \\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; \mv{t_n'} \} }
\end{array}
\\
\\
{\sf WLoop_n} \; (P, \; B, \;  \mv{X_n}, \; {\sf False}) & \reduce{}{} &
\mv{X_n}
\end{array} \]  
}
{\large
\[\begin{array}{lll}
{\sf FLoop_n} \; ( U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf True}) & \reduce{}{} & \{_{\sf n} \begin{array}[t]{lll}
 \mv{t_{2,n}} & = & {\sf Ap_{n,{n-1}}} \; (B, \;   \mv{X_{n}}) ;\\
t_1 & = & {\sf +} \; ( X_1, \; D); \\
 t_{p} & = & {\sf <} \; (t_1, \; U);\\
\mv{t_n'} & = & {\sf FLoop_n} \;(U, \; D, \; B, \;  \mv{t_{n}},\; t_{p})  \\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; \mv{t_n'} \} }
\end{array}
\\
\\
{\sf FLoop_n} \; (U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf False}) & \reduce{}{} &  \mv{X_{n}}  
\end{array} \]
}

\newpage

\subsection*{Multivariable rule}
{\large
\[\begin{array}{lll}
\mv{X_n} \;= \;\mv{Y_n} \;\;\reduce{}{} \;\; (X_1 = Y_1; \cdots X_n = Y_n) 
\end{array}\]
}

\subsection*{Substitution rules}
{\large
\[ \begin{array}{lll}
\frag{X = Y}{ X \reduce{}{} Y}\\ 
\frag{X = V}{ X \reduce{}{} V}
\end{array}\]
}

\subsection*{Block Flattening rule}
{\large
\[ \begin{array}{lll}
\begin{array}{lll}
\{_{\sf m} \;\mv{X_n} \; = \;  \{_{\sf n} \; SS_1;\;SS_2;\;\cdots & & \;
\{_{\sf m} \; \mv{X_n}  \; = \; \mv{Y_n};\\
\hspace{1.8cm}\;\;\;\;{\sf In}\;\; \mv{Y_n} \} &
\reduce{}{} & \;\;\;\;\;\;\; {SS_1};\;{SS_2};\;\cdots \;  \\
\;\;\;\;\;\; S_1;\;\cdots \;\; S_n\;  & & \;\;\;\;\;\;\; S_1; \; \cdots \;  \; S_n\; \\
\hspace{0.9cm}{\sf In} \;\mv{Z_m}\}  & & \hspace{0.9cm}{\sf In} \;\mv{Z_m}\} 
\end{array} 
\end{array} \]
} 


\subsection*{Propagation of $\top$}
{\large
\[ \begin{array}{lll}
\begin{array}{lll}
\{_{\sf m} \; X = \top; \; S_1; \cdots S_n \; {\sf In} \; \mv{Z_m}  \; \} &
\reduce{}{} & \;\;\;  \top 
\\
\\
\{_{\sf m} \;  \top_s; \; S_1; \cdots S_n \; {\sf In} \; \mv{Z_m} \; \} &
\reduce{}{} & \;\;\;  \top 
\end{array} 
\end{array}\]
} 

\end{document}

