
\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 & \\
{\sf Equal?}\;(\underline{n}, \; \underline{n})
& \reduce{\delta}{} & {\sf True} \\
{\sf Equal?}\;(\underline{m}, \; \underline{n} ) 
& \reduce{\delta}{} & {\sf False}
\hspace{2cm} \mbox{(if m $\neq$ $n$)}
\end{array} \]
}
\newpage

\subsection*{Case rules}
{\large
\[\begin{array}{lll}
{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) & \reduce{}{} & E_1 \\
\\
{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) & \reduce{}{} & E_2 \\
\end{array} \]
}

{\large
\[\begin{array}{l}
\frag{X = {\sf Nil}}  
{{\sf List\_case_m} \; (X,\; E_1, \; E_2) \; \; \reduce\;\;E_1 }
\end{array} \]
}

{\large
\[\begin{array}{l}
\frag{X = {\sf Open\_cons} \;() }
{{\sf List\_case_m} \; (X,\; E_1, \; E_2) \; \; \reduce\;\;E_2 }
\end{array}\]
}
\newpage

\subsection*{Arity Detection rule}
{\large
\[\frag{ \begin{array}{llll}
F & = & {\sf \lambda_n}\; (\mv{Z_n}) \; . \;  (E) & \mid \\
F_1  & = &  {\sf Apply}\;(F, \; X_1) & \mid  \\
F_2  & = &  {\sf Apply}\;(F_1, \; X_2) & \mid  \\
\multicolumn{4}{l}{ \; \vdots} \\
F_{n-1}  & = & {\sf Apply}\;(F_{n-2},\; X_{n-1}) &
\end{array}}
{ {\sf Apply}\;(F_{n-1}, \; X_n )\;\; \reduce{}{} \;\; 
{\sf Ap_n}\; (F, \; \mv{X_n}) 
}\]
} \\


\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*{Tuple rule}
{\large
\[\begin{array}{l}
\frag{ X = {\sf Make\_tuple_n} \; (\mv{X_n})}
{{\sf Detuple_n} \; (X) \; \; \reduce{}{} \;\; \mv{X_n}}
\end{array} \]
} 

\subsection*{List rules}
{\large
\[\begin{array}{lll}
{\sf Cons} \; (X, \; Y) & \reduce{}{} & \{
\begin{array}[t]{lll}
t & = & {\sf Open\_cons} \;(); \\
\multicolumn{3}{l}{ {\sf Cons\_store\_1 } \; (t,\;X); }\\
\multicolumn{3}{l}{ {\sf Cons\_store\_2 } \; (t,\;Y) }\\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; t \} }
\end{array}
\end{array}\]
}

{\large
\[ \frag{{\sf Cons\_store\_1} \; (X, \; Y) }
{{\sf Cons\_1} \;(X  )\;\;\; \reduce{}{}\;\;\;  Y  } \]
}

\blank
\noindent
{\large
\[\frag{{\sf Cons\_store\_2} \; (X, \; Y) }
{{\sf Cons\_2} \;(X  )\;\;\; \reduce{}{}\;\;\;  Y  } \]
}

{\large
\[ \frag{{\sf Cons\_store\_1} \; (X, \; Y) }
{{\sf Cons\_store\_1} \;(X,  \;Y') \;\;\; \reduce{}{}\;\;\;  \top_s  } \]
}

{\large
\[ \frag{{\sf Cons\_store\_2} \; (X, \; Y) }
{{\sf Cons\_store\_2} \;(X,  \;Y') \;\;\; \reduce{}{}\;\;\;  \top_s  } \]
}

\newpage

\subsection*{Array rules}
{\large 
\[\begin{array}{l}
\frag{X={\sf I\_nD\_array} \; (X_b)}
{{\sf nD\_Bounds}\; (X) \;\; \reduce{}{}\;\;X_b}
\end{array} \]
}

\blank
\noindent
{\large
\[\frag{{\sf P\_nD\_store} \; (X, \; Y,\; Z) }
{{\sf P\_nD\_select} \;(X, \; Y)\;\;
\reduce{}{}\;\;\;  Z } \]
}

{\large
\[\frag{{\sf P\_nD\_store} \; (X, \; Y,\; Z) }
{{\sf P\_nD\_store} \;(X, \; Y,\; Z')\;\; \reduce{}{}\;\;\;  \top_s } \]
}

\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}\]
}

\newpage

\subsection*{Substitution rules}
{\large
\[ \begin{array}{lll}
\frag{X = Y}{ X \reduce{}{} Y}\\ 
\frag{X = C}{ X \reduce{}{} C}
\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} 
