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


\subsubsection*{TE: Id$^{-}$ Expression $\longrightarrow$ Kid Expression}  
{\large
$\begin{array}{l}
{\tt TE}[\![X]\!] = X 
\end{array}$ \\
}


{\large
\blank
\noindent
$\begin{array}{l}
{\tt TE}[\![{\sf Next} \; X]\!] = next(X)
\end{array}$ \\
}


{\large
\blank
\noindent
$\begin{array}{ll}
{\tt TE}[\![C]\!] = C 
\end{array}$ \\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![(U\!O\!P \; E)]\!] & = &  \{ \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![E]\!];\\
t & = & {\tt TO}[\![U\!O\!P]\!]\;(t_1) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t   \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![(E_1 \; B\!O\!P \; E_2)]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!]; \\
t & = & {\tt TO}[\![B\!O\!P]\!]\; (t_1, \;t_2) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![(E_1\; E_2)]\!] & = &  \{ \begin{array}[t]{lll} 
t_1 & =  & {\tt TE}[\![E_1]\!]; \\
t_2 & = &  {\tt TE}[\![E_2]\!]; \\
t & = &  {\sf Apply} \;(t_1,\;t_2)\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\newpage

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ E_1[E_2] ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t_2 & = & {\tt TE}[\![E_2]\!]; \\
t & = &  {\sf Ap_2} \; ({\sf Select}, \; t_1, \; t_2) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}\\$
}


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ E.{\sf cons\_1} ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E]\!];\\
t & = & {\sf List\_case} \;(t_1,\; {\sf Error}, \; {\sf Cons\_1}\;(t_1) )\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}\\$
}

\newpage

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![(E_1, \cdots, E_n) ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
\multicolumn{3}{l}{ \;\;\;\;\vdots} \\
t_n & = &  {\tt TE}[\![E_n]\!]; \\
t & = &  {\sf Make\_tuple_n} \;(\mv{t_n})\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\newpage

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ ({\sf If}\; E_1\; {\sf then}\; E_2\; {\sf else}\; E_3)]\!] & = & 
\{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t & = &  {\sf Bool\_case} \; (t_1, \; {\tt TE}[\![E_2]\!], \;
{\tt TE}[\![E_3]\!] )\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$\\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{ \begin{array}[t]{lll}
\multicolumn{3}{l}{ {\sf Case} \; E \; {\sf of}} \\
\;\; \mid \; \;\;\;P_1  & = &  E_1 \\
\multicolumn{3}{c}{ \vdots}\\
\;\; \mid \;\;\;P_n  & = &  E_n \; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![ E ]\!]; \\
t & = & {\tt PM}[\![ \{ \begin{array}[t]{lll}
\multicolumn{3}{l}{ {\sf Case} \; (t_1) \; {\sf of}} \\
\;\; \mid \;\;\; P_1 & = & {\tt TE}[\![E_1]\!]\\
\multicolumn{3}{c}{ \vdots}\\
\;\; \mid \;\;\; P_n & = & {\tt TE}[\![E_n]\!] \; \} ]\!]
\end{array}   \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array} $ \\
}

\newpage


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{  \begin{array}[t]{l}
 {\sf While} \; E \; {\sf do}\\
\;\; S_1; \\
\;\;\;\; \vdots \\
\;\; S_n; \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} &  = &
\begin{array}[t]{l}
{\tt TSLE}[\![ \{ \begin{array}[t]{l}
  {\sf While} \; {\tt TE}[\![E]\!] \; {\sf do}\\
\;\; {\tt TS}[\![S_1]\!]; \\
\;\;\;\; \vdots \\
\;\; {\tt TS}[\![S_n]\!]; \\
\;\;\;\;{\sf Finally}\;{\tt TE}[\![E_f]\!]\; \}]\!]
\end{array} 
\end{array}
\end{array}$\\
}


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TSLE}[\![ \{  \begin{array}[t]{l}
 {\sf While} \; E \; {\sf do}\\
\;\; next(X_1)  = E_1;\\
\;\;\;\; \vdots \\
\;\; next(X_n)  = E_n;\\
\;\; Y_1 = E_{y_1};\\
\;\;\;\; \vdots \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
p & = &  \underline{\lambda_{n}} \; ( \mv{X_n}) \; . \;   (E);\\
b & = & \underline{\lambda_{n,n}} \; ( \mv{X_n} )  \;\; . \;\;  
( \{_{\sf n} \begin{array}[t]{l}
next(X_1)   =  E_1  ;\\
\;\;\; \vdots\\
next(X_n)  = E_n ;\\
Y_1 =  E_{y_1};\\
\;\;\; \vdots \\
\;\;\;\; \;{\sf In} \; next(X_1), \cdots, next(X_n) \; \} ); 
\end{array} \\
\blank
t_p & = &  {\sf Ap_n} \; (p,\; \mv{X_n});\\
\mv{t_{n}} &  = & {\sf WLoop_n} \; (p, \; b, \;  \mv{X_n}, \; t_p); \\
t_f & = &  E_f \;[\mv{t_n}/\mv{X_n}]_B \\
\multicolumn{3}{l}{ \;\;\;\;{\sf In} \; t_f \} }
\end{array}
\end{array} $
}\\

\newpage

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{  \begin{array}[t]{l}
 {\sf For} \; X \; \leftarrow \; E_i \; {\sf to} \; E_b \; {\sf step} \;
Es \; {\sf do}\\
\;\; S_1; \\
\;\;\;\; \vdots \\
\;\; S_n; \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} &  = &
\begin{array}[t]{l}
{\tt TSLE}[\![ \{\begin{array}[t]{l}
  {\sf For} \; X \; \leftarrow \; {\tt TE}[\![ E_i ]\!] \; {\sf to}\; {\tt TE}[\![ E_b ]\!] \; {\sf step} \; {\tt TE}[\![ E_s ]\!] \;  {\sf do} \\
\;\; {\tt TS}[\![S_1]\!]; \\
\;\;\;\; \vdots \\
\;\; {\tt TS}[\![S_n]\!]; \\
\;\;\;\;{\sf Finally}\;{\tt TE}[\![E_f]\!]\; \}]\!]
\end{array} 
\end{array} \\
\end{array}$ 
}\\

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TSLE}[\![  \begin{array}[t]{l}
\{ {\sf For} \; X_1 \; \leftarrow \; E_i \; {\sf to} \; E_b \;
{\sf step} \; E_s \; {\sf do}\\
\;\; next(X_2)  = E_2;\\
\;\;\;\; \vdots \\
\;\; next(X_{n})  = E_n;\\
\;\; Y_1 = E_{y_1};\\
\;\;\;\; \vdots \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
b & = & \begin{array}[t]{l}
\underline{\lambda_{n,{n-1}}} \; ( \mv{X_{n}} )\;  . \\
\hspace{0.4cm}{
( \{_{\sf n-1} \begin{array}[t]{l}
next(X_2)   =  E_2  ;\\
\;\;\; \vdots\\
next(X_{n})  = E_{n} ;\\
Y_1 =  E_{y_1};\\
\;\;\; \vdots \\
\;\;\; \;{\sf In} \; next(X_2), \cdots, next(X_{n}) \; \} ); 
\end{array} }
\end{array} \\
\blank
t_i & = &  E_i;\\
t_b & = &  E_b;\\
t_s & = &  E_s;\\
t_p & = &  {\sf \leq} \; (t_i,\; t_b);\\
\mv{t_{n}} &  = & {\sf FLoop_n} \; (t_b, \; t_s,\; b,\; t_i,\;
\mv{X_{2,n}}, \; t_p); \\
t_f & = &  E_f \;[\mv{t_n}/\mv{X_n}]_B \\
\multicolumn{3}{l}{ \;\;\;\;{\sf In} \; t_f \} }
\end{array}
\end{array} $
}\\

\newpage

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{ {\sf Fun} \;\mv{X_n} \; =   \; E \} ]\!] & = &    
 {\sf \lambda_n} \;(\mv{X_n}) \; .   \; ({\tt TE}[\![ E]\!] )
\end{array}$\\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{ \underline{{\sf Fun}} \;\mv{X_n} \; =   \; E \} ]\!] & = &    
 \underline{{\sf \lambda_n}} \;(\mv{X_n}) \; .   \; ({\tt TE}[\![ E]\!] )
\end{array}$\\
}


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TE}[\![ \{ S_1; \cdots S_n;\; {\sf In} \;E\}]\!] & = &
\{ \; {\tt TS}[\![S_1]\!];\\
& &\;\;\;\;\vdots\\
& & \;\;\;  {\tt TS}[\![S_n]\!];\\
& &  \;\;\; t = {\tt TE}[\![E]\!]\\
& & \;\;\;\;{\sf In}\;\;t \; \}
\end{array}$ \\
}

\newpage


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TS}[\![ P=E  ]\!] & = &
(t = {\tt TE}[\![ E ]\!];\;  {\tt TB}[\![ P=t  ]\!] ) 
\end{array}$\\
}


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TS}[\![ E_1[E_2] = E_3 ]\!] & = &
( \begin{array}[t]{lll}
 t_1 & = & {\tt TE}[\![ E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!];\\
t_3 & = & {\tt TE}[\![E_3]\!];\\
t &  = &  {\sf Ap_3} \; ({\sf Store},\;t_1,\;t_2,\;t_3) )
\end{array}
\end{array}$ \\
}


\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TS}[\![ E_1.{\sf cons\_1} = E_2 ]\!] & = &
( \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![ E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!];\\
t & = & {\sf List\_case}\;(t_1, \; \{\; {\sf Store\_error} \; {\sf In} \; () \},
\{ \; {\sf Cons\_store\_1} \; (t_1, \; t_2) \; {\sf In} \; () \; \} \; )\;) 
\end{array}
\end{array}$ \\
}



\subsubsection*{TB: Id$^{-}$ Bindings $\longrightarrow$ list (Kid Binding)}  

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TB}[\![ (P_1,\cdots, P_n)= X  ]\!] & = &
( \mv{t_n} = {\sf Detuple_n} \; (X);\\
 & &\;\;{\tt TB}[\![ P_1 = t_1 ]\!];\\
& & \;\;\;\;\vdots\\
& &\;\;{\tt TB}[\![ P_n = t_n ]\!] \; )\\
\end{array}$\\
}

\blank
\noindent
{\large
$\begin{array}{lll}
{\tt TB}[\![ (P_1 \; : \; P_2) = X ]\!] & = & (
t_1,\;t_2  =  {\sf List\_case_2}\;(X, \; (\;{\sf Error}, \; {\sf Error}\;) 
,\;( {\sf Cons\_1} \;(X),\; {\sf Cons\_2}\;(X) )\;);\\
& &\;\;{\tt TB}[\![P_1 = t_1 ]\!];\\
& &\;\;{\tt TB}[\![P_2 = t_2 ]\!] )
\end{array}\\$
}

\blank
\noindent
{\large
$ \begin{array}{lll}
{\tt TB}[\![ Y = X ]\!] & = & (Y = X)
\end{array}$
}\\

\blank
\noindent
{\large
$ \begin{array}{lll}
{\tt TB}[\![ {\sf Next} \; Y = X ]\!] & = & (next(Y)  = X)
\end{array}$
}

\newpage


\blank
\noindent
{\large
${\tt TO}[\![ U\!O\!P ]\!]= \mbox{ the corresponding  Kid } P\!F1   $
}

\blank
\noindent
{\large
${\tt TO}[\![ B\!O\!P]\!]= \mbox{ the corresponding  Kid } P\!F2  $\\
}

\noindent
The Kid operator corresponding to Id$^-$ ``{\sf :}" is {\sf Cons} and for ``{\sf ==}''
is {\sf Equal?}.



\end{document}
