\documentclass{jarticle}
\usepackage{fullpage}
\usepackage{min-caml}

\begin{document}


\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{lll}
\lefteqn{\s : \texttt{SparcAsm.prog} \to \texttt{string}} \\
\s((\{D_1, \dots, D_n\}, E)) & = & \verb|.section ".text"| \\
& & \s(D_1) \\
& & \dots \\
& & \s(D_n) \\
& & \verb|.global min_caml_start| \\
& & \verb|min_caml_start:| \\
& & \verb|save %sp, -112, %sp| \\
& & \s(E, \verb|%g0|) \\
& & \verb|ret| \\
& & \verb|restore| \\
\\
\lefteqn{\s : \texttt{SparcAsm.fundef} \to \texttt{string}} \\
\s(\lab_x (y_1, \dots, y_n) = E) & = & x\verb|:| \\
& & \s(E, \reg{0}) \\
& & \verb|retl| \\
& & \verb|nop| \\
\\
\lefteqn{\s : \texttt{SparcAsm.t} \times \texttt{Id.t} \to \texttt{string}} \\
\s((x \leftarrow e; E), z_\dest) & = & \s(e, x); \s(E, z_\dest) \\
\s(e, z_\dest) & = & \s(e, z_\dest) \\
\end{array}
\]
\caption{ñ��ʥ�����֥�����$\s(P)$, $\s(D)$�����$\s(E, z_\dest)$}
}\fbox{\box0}
\end{figure*}

\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{lll}
\lefteqn{\s : \texttt{SparcAsm.exp} \times \texttt{Id.t} \to \texttt{string}} \\
\s(c, z_\dest) & = & \verb|set|~c, z_\dest \\
\s(\lab_x, z_\dest) & = & \verb|set|~\lab_x, z_\dest \\
\s(\OP(x_1, \dots, x_n), z_\dest) & = & \OP~x_1, \dots, x_n, z_\dest \\
\s(\IF~x = y~\THEN~E_1~\ELSE~E_2, z_\dest) & = & \verb|cmp|~x, y \\
& & \verb|bne|~b_1 \\
& & \verb|nop| \\
& & \s(E_1, z_\dest) \\
& & \verb|b|~b_2 \\
& & \verb|nop| \\
& & b_1\verb|:| \\
& & \s(E_2, z_\dest) \\
& & b_2\verb|:| \\
\s(\IF~x \le y~\THEN~E_1~\ELSE~E_2, z_\dest) & = & \mbox{Ʊ��} \\
\s(x, z_\dest) & = & \verb|mov|~x, z_\dest \\
\s(\apcls(x, y_1, \dots, y_n), z_\dest) & = & \mathit{shuffle}((x, y_1, \dots, y_n), (\reg{0}, \reg{1}, \dots, \reg{n})) \\
& & \verb|st|~\ra, [\st + 4\#\e] \\
& & \verb|ld|~[\reg{0}], \reg{n+1} \\
& & \verb|call|~\reg{n+1} \\
& & \verb|add|~\st, 4(\#\e+1), \st~\verb|!|~\mbox{\textit{delay slot}} \\
& & \verb|sub|~\st, 4(\#\e+1), \st \\
& & \verb|ld|~[\st + 4\#\e], \ra \\
& & \verb|mov|~\reg{0}, z_\dest \\
\s(\apdir(\lab_x, y_1, \dots, y_n), z_\dest) & = & \mathit{shuffle}((y_1, \dots, y_n), (\reg{1}, \dots, \reg{n})) \\
& & \verb|st|~\ra, [\st + 4\#\e] \\
& & \verb|call|~x \\
& & \verb|add|~\st, 4(\#\e+1), \st~\verb|!|~\mbox{\textit{delay slot}} \\
& & \verb|sub|~\st, 4(\#\e+1), \st \\
& & \verb|ld|~[\st + 4\#\e], \ra \\
& & \verb|mov|~\reg{0}, z_\dest \\
\s(x.(y), z_\dest) & = & \verb|ld|~[x + y], z_\dest \\
\s(x.(y) \leftarrow z, z_\dest) & = & \verb|st|~z, [x + y] \\
\s(\SAVE(x, y), z_\dest) & = & \mbox{�⤷$y \not\in \dom(\e)$�ʤ�$\e \leftarrow (\e, y \mapsto 4\#\e)$�Ȥ���} \\
& & \verb|st|~x, [\st + \e(y)] \\
\s(\REST(y), z_\dest) & = & \verb|ld|~[\st + \e(y)], z_\dest \\
\end{array}
\]
\caption{ñ��ʥ�����֥�����$\s(e, z_\dest)$��$\e$�ϥ����å����֤򵭲����륰�����Х��ѿ���$\#\e$��$\e$�����ǤθĿ���$\mathit{shuffle}((x_1, \dots, x_n), (r_1, \dots, r_n))$��$x_1$, \dots, $x_n$��$r_1$, \dots, $r_n$��Ŭ�ڤʽ���ǰ�ư����̿�ᡣ}
}\fbox{\box0}
\end{figure*}

\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{lll}
\lefteqn{\s : \texttt{S.t} \to \texttt{SparcAsm.t} \times \texttt{Id.t} \to \texttt{S.t} \times \texttt{string}} \\
\s_s((x \leftarrow e; E), z_\dest) & = & \s_s(e, x) = (s', S), \\
& & \s_{s'}(E, z_\dest) = (s'', S') \mbox{�Ȥ���} \\
& & (s'', S S') \\
\s_s(e, z_\dest) & = & \s_s(e, z_\dest) \\
\\
\lefteqn{\s : \texttt{S.t} \to \texttt{SparcAsm.exp} \times \texttt{Id.t} \to \texttt{S.t} \times \texttt{string}} \\
\s_s(\IF~x = y~\THEN~E_1~\ELSE~E_2, z_\dest) & = & \s_s(E_1, z_\dest) = (s_1, S_1), \\
& & \s_s(E_2, z_\dest) = (s_2, S_2) \mbox{�Ȥ���} \\
& & (s_1 \cap s_2, \\
& & \phantom{(}\verb|cmp|~x, y \\
& & \phantom{(}\verb|bne|~b_1 \\
& & \phantom{(}\verb|nop| \\
& & \phantom{(}S_1 \\
& & \phantom{(}\verb|b|~b_2 \\
& & \phantom{(}\verb|nop| \\
& & \phantom{(}b_1\verb|:| \\
& & \phantom{(}S_2 \\
& & \phantom{(}b_2\verb|:|) \\
\s_s(\IF~x \le y~\THEN~E_1~\ELSE~E_2, z_\dest) & = & \mbox{Ʊ��} \\
\s_s(\SAVE(x, y), z_\dest) & = & (s, \verb|nop|) \hfill \mbox{$y \in s$�ξ��} \\
\s_s(\SAVE(x, y), z_\dest) & = & \mbox{�⤷$y \not\in \dom(\e)$�ʤ�$\e \leftarrow (\e, y \mapsto 4\#\e)$�Ȥ���} \\
& & (s \cup \{y\}, \verb|st|~x, [\st + \e(y)]) \hfill \mbox{$y \not\in s$�ξ��} \\
\s_s(e, z_\dest) & = & (s, \mbox{������Ʊ��}) \hfill \mbox{��Ұʳ��ξ��} \\
\end{array}
\]
\caption{̵�̤�$\SAVE$���ά���륢����֥�����$\s_s(E, z_\dest)$�����$\s_s(e, z_\dest)$��$s$�Ϥ��Ǥ�$\SAVE$���줿�ѿ���̾���ν��硣������$\s(E, z_\dest)$��$\s_\emptyset(E, z_\dest) = (s, S)$�Ȥ���$S$��ά���Ȥ��롣}
}\fbox{\box0}
\end{figure*}

\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{lll}
\lefteqn{\s : \texttt{SparcAsm.fundef} \to \texttt{string}} \\
\s(\lab_x (y_1, \dots, y_n) = E) & = & \s_\emptyset(E, \tail) = (s, S) \mbox{�Ȥ���} \\
& & x\verb|:| \\
& & S \\
\\
\lefteqn{\s : \texttt{S.t} \to \texttt{SparcAsm.exp} \times \texttt{Id.t} \to \texttt{S.t} \times \texttt{string}} \\
\s_s(\IF~x = y~\THEN~E_1~\ELSE~E_2, \tail) & = & \s_s(E_1, \tail) = (s_1, S_1), \\
& & \s_s(E_2, \tail) = (s_2, S_2) \mbox{�Ȥ���} \\
& & (\emptyset, \\
& & \phantom{(}\verb|cmp|~x, y \\
& & \phantom{(}\verb|bne|~b \\
& & \phantom{(}\verb|nop| \\
& & \phantom{(}S_1 \\
& & \phantom{(}b\verb|:| \\
& & \phantom{(}S_2) \\
\s_s(\IF~x \le y~\THEN~E_1~\ELSE~E_2, \tail) & = & \mbox{Ʊ��} \\
\s_s(\apcls(x, y_1, \dots, y_n), \tail) & = & (\emptyset, \\
& & \phantom{(}\mathit{shuffle}((x, y_1, \dots, y_n), (\reg{0}, \reg{1}, \dots, \reg{n})) \\
& & \phantom{(}\verb|ld|~[\reg{0}], \reg{n+1} \\
& & \phantom{(}\verb|jmp|~\reg{n+1} \\
& & \phantom{(}\verb|nop|) \\
\s_s(\apdir(\lab_x, y_1, \dots, y_n), \tail) & = & (\emptyset, \\
& & \phantom{(}\mathit{shuffle}((y_1, \dots, y_n), (\reg{1}, \dots, \reg{n})) \\
& & \phantom{(}\verb|b|~x \\
& & \phantom{(}\verb|nop|) \\
\s_s(e, \tail) & = & \s_s(e, \reg{0}) = (s', S) \mbox{�Ȥ���} \\
& & (\emptyset, \\
& & \phantom{(}S \\
& & \phantom{(}\verb|retl| \\
& & \phantom{(}\verb|nop|) \hfill \mbox{��Ұʳ��ξ��} \\
\end{array}
\]
\caption{�����ƤӽФ���Ŭ���򤹤륢����֥�����$\s_s(D)$�����$\s_s(e, z_\dest)$��$z_\dest = \tail$�ξ�礬������}
}\fbox{\box0}
\end{figure*}

\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{ll}
\lefteqn{e~::=~} & \\
& c \\
& \OP(x_1, \dots, x_n) \\
& \IF~x = y~\THEN~e_1~\ELSE~e_2 \\
& \IF~x \le y~\THEN~e_1~\ELSE~e_2 \\
& \LET~x = e_1~\IN~e_2 \\
& x \\
& \LET~\REC~x~y_1~\dots~y_n = e_1~\IN~e_2 \\
& x~y_1~\dots~y_n \\
& (x_1, \dots, x_n) \\
& \LET~(x_1, \dots, x_n) = y~\IN~e \\
& x.(y) \\
& x.(y) \leftarrow z \\
\end{array}
\]
\caption{MinCaml��K�������ʳ������󡦳����ؿ�Ŭ�ѤϾ�ά��}
}\fbox{\box0}
\end{figure*}



\begin{figure*}
\setbox0\vbox{
\[
\begin{array}{lll}
\lefteqn{\C : \texttt{Id.t} \to \texttt{KNormal.t} \to \texttt{KNormal.t}} \\
\\
\C_k(\IF~x \le y~\THEN~e_1~\ELSE~e_2) & = & \IF~x \le y~\THEN~\C_k(e_1)~\ELSE~\C_k(e_2) \\
\C_k(\IF~x = y~\THEN~e_1~\ELSE~e_2) & = & \IF~x = y~\THEN~\C_k(e_1)~\ELSE~\C_k(e_2) \\
\C_k(\LET~(x_1,\dots,x_n) = y~\IN~e) & = & \LET~(x_1,\dots,x_n) = y~\IN~\C_k(e) \\
\\
\C_k(\LET~x = (\IF~y \le z~\THEN~e_1~\ELSE~e_2)~\IN~e_3) & = &
\LET~\REC~k'~x = \C_k(e_3)~\IN \\ & &
\IF~y \le z~\THEN~\C_{k'}(e_1)~\ELSE~\C_{k'}(e_2)
\quad \hfill \mbox{��$k'$��fresh��} \\
\C_k(\LET~x = (\IF~y = z~\THEN~e_1~\ELSE~e_2)~\IN~e_3) & = &
\LET~\REC~k'~x = \C_k(e_3)~\IN \\ & &
\IF~y = z~\THEN~\C_{k'}(e_1)~\ELSE~\C_{k'}(e_2)
\quad \hfill \mbox{��$k'$��fresh��} \\
%
\C_k(\LET~x = y~z_1~\dots~z_n~\IN~e) & = &
\LET~\REC~k'~x = \C_k(e)~\IN~y~k'~z_1~\dots~z_n \\ & &
\quad \hfill \mbox{��$k'$��fresh��} \\
%
\C_k(\LET~x = e_1~\IN~e_2) & = & \LET~x = e_1~\IN~\C_k(e_2)
\quad \hfill \mbox{�ʾ�Ұʳ��ξ���} \\
\\


\C_k(\LET~\REC~f~x_1~\dots~x_n = e_1~\IN~e_2) & = &
\LET~\REC~f~c~x_1~\dots~x_n = \C_c(e_1)~\IN~\C_k(e_2) \\ & &
\quad \hfill \mbox{��$c$ ��fresh��} \\
%
\C_k(x~y_1~\dots~y_n) & = & x~k~y_1~\dots~y_n \\
\\

\C_k(e) & = & \LET~x = e~\IN~k~x
\quad \hfill \mbox{�ʾ�Ұʳ��ξ�硣$x$��fresh��} \\
\end{array}
\]
\caption{[����] $\alpha$�Ѵ������A�������δ�λ����K���������Ф���CPS�Ѵ�$\C_k(e)$��������$k$��$e$�η�³����³���ʤ��Ȥ��ϡ�$\LET~\REC~k~x = x~\IN~\C_{k}(e)$�Τ褦�˹����ؿ��Ȥ���ʥᥤ��롼����ʤɡ�}
}\fbox{\box0}
\end{figure*}

\end{document}
