\documentstyle{jarticle}
\title{$ 1999 $$BG/EY(B $B7W;;%b%G%kO@(B $B2]Bj(B}
\author{G96P073-6 $B9bLZM42p(B}
\date{\today}


\newcommand{\rl}[1]{\mbox{$ \; (\rightarrow \cup \leftarrow)^{#1} \; $}}

% Natural Numbers
\newcommand{\N}{\mbox{$ \bf N $}}

% singleton set
\newcommand{\set}[1]{\mbox{$ \{ #1 \} $}}
\newcommand{\1}{\mbox{$ \set{.} $}}

\newcommand{\seq}{\mbox{$ \1 + A \times L $}}
\newcommand{\$BNs(B}[1]{\mbox{$ \; < #1 > \; $}}

\newcommand{\key}[1]{{ \bf #1 }}
\newcommand{\nop  }{\key{skip}}
\newcommand{\ifStm}[3]{\mbox{ \key{if} $#1$ \key{then} $#2$ \key{else} $#3$ }}
\newcommand{\while}[2]{\mbox{ \key{while} $#1$ \key{do} $#2$ }}
\newcommand{\doStm}[2]{\mbox{ \key{do} $#1$ \key{while} $#2$ }}

\newcommand{\combinator}[1]{\mbox{$ \; \overline{\mbox{#1}} \; $}}
\newcommand{\nil  }{\combinator{nil  }}
\newcommand{\true }{\combinator{true }}
\newcommand{\false}{\combinator{false}}
\newcommand{\pair }{\combinator{pair }}
\newcommand{\cons }{\combinator{cons }}
\newcommand{\head }{\combinator{head'}}
\newcommand{\tail }{\combinator{tail'}}
\newcommand{\nilp }{\combinator{null }}
\newcommand{\car  }{\combinator{car  }}
\newcommand{\cdr  }{\combinator{cdr  }}

\newcommand{\df}{\mbox{$ \; =_{\mbox{def}} \; $}}

\newcommand{\trans}[1]{\mbox{$ ^{\mbox{(#1)}} \; $}}


\begin{document}
\maketitle


\section{$B=89g(B$ X $$B>e$NF1CM4X78(B}

$ \rightarrow $$B$,(B$ X $$B>e$N(B$ 2 $$B9`4X78$G$"$k$H$-!"(B
\rl{*}$B$,!"(B$ \rightarrow $$B$r4^$`:G>.$NF1CM4X78$G$"$k$3$H$r<($;!#(B

$B$^$:!"D>46E*$K<($7!"<!$K!"$b$&>/$787L)$J>ZL@$r;n$_$k!#(B

$BF1CM4X78$N>r7o$O!"H?<MN'!"BP>NN'!"?d0\N'$N(B$ 3 $$B$D$rK~$?$9$3$H$G$"$C$?!#(B
$ \rightarrow $$B$r4^$`:G>.$NF1CM4X78$O!"0J2<$N$h$&$J$b$N$G$"$k!#(B
\\$BBP>NN'$rK~$?$9$?$a$K!"(B$ \leftarrow $$B$r4^$^$J$1$l$P$J$i$J$$!#(B
\\$B?d0\N'$rK~$?$9$?$a$K!"(B$ 1 $$B2s0J>e$N7+$jJV$7$r4^$^$J$1$l$P$J$i$J$$!#(B
\\$BH?<MN'$rK~$?$9$?$a$K!"(B$ 0 $$B2s$N7+$jJV$7$r5v$5$J$1$l$P$J$i$J$$!#(B
\\$B$h$C$F!"5a$a$kF1CM4X78$O!"(B\rl{*}$B$G$"$k!#(B

$B0J2<!"$b$&>/$787L)$J>ZL@!#(B

\rl{*}$B$,!"(B$ \rightarrow $$B$r4^$`$3$H$r<($9!#(B
\begin{eqnarray*}
\rl{*}
  &=& \bigcup_{n \in \N} \rl{n} \\
  &=& \rl{0} \cup              \rl{1}             \cup \cdots \\
  &=& \rl{0} \cup \;\rightarrow \cup \leftarrow\; \cup \cdots \\
  &\supseteq& \;\rightarrow \\
\end{eqnarray*}

$B0J2<$G$O!"4JC1$N$?$a$K!"(B\rl{*}$B$r(B$ = $$B$HCV$/!#(B

$ = $$B$,!"F1CM4X78$G$"$k$3$H$r<($9!#(B
\\
$BH?<MN'!#(B$ X $$B$NMWAG(B$ x $$B$r9M$($k!#(B
$ x $$B$O!"(B$ 0 $$B2s$N4JLs$K$h$C$F(B$ x $$B$KE~C#2DG=$G$"$k!#(B
$B!J0lHLE*$J>l9g$G$b>ZL@$G$-$=$&$G$9$,!"(B
  $B%N!<%H$G$O!"(B$ \lambda $$B<0$N4JLs$N$H$3$m$KF1$8LdBj$,=q$$$F$"$k$N$G!"(B
  $ \rightarrow $$B$O(B$ \lambda $$B<0$N4JLs!"(B
  $ = $$B$O(B$ \lambda $$B<0$NEy2A@-$rI=$9$b$N$H$7$^$9!#!K(B
$B$D$^$j!"(B$ \forall x \in X \; (x \rightarrow^0 x) $$B$G$"$j!"(B
$ \forall x \in X \; (x=x) $$B$G$"$k!#(B
\\
$BBP>NN'!#(B
$ (x \rightarrow^n y) \Leftrightarrow (y \leftarrow^n x) $$B$G$"$k!#(B
$B$^$?!"5"G<E*$K!"(B$ (x=z) \wedge (z \leftarrow^n y) \Leftrightarrow (y \rightarrow^n z) \wedge (z=x) $$B$G$"$k!#(B
$B$h$C$F!"(B$ \forall x \forall y \in X \; (x=y \Rightarrow y=x) $$B$G$"$k!#(B
\\
$B?d0\N'!#(B
$B5"G<E*$K!"(B$ (x \rl{n} y) \wedge (y \rightarrow z) \Rightarrow (x \rl{n+1} z) $$B$G$"$k!#(B
\\$B$^$?!"(B$ (x \rl{n} y) \wedge (y \leftarrow z) \Rightarrow (x \rl{n+1} z) $$B$G$"$k!#(B
\\$B$h$C$F!"(B$ \forall x \forall y \forall z \in X \; (x=y \;\wedge\; y=z \Rightarrow x=z) $$B$G$"$k!#(B

$ = $$B$,!"(B$ \rightarrow $$B$r4^$`F1CM4X78$N$&$A:G>.$N$b$N$G$"$k$3$H$r<($9!#(B
$ R $$B$O!"(B$ \rightarrow $$B$r4^$`!"(B$ = $$B$NItJ,F1CM4X78$G$"$k$H$9$k!#(B
$B!J$D$^$j!"(B$ \rightarrow\; \subseteq R \subseteq \;= $$B$G$"$k$h$&$JF1CM4X78$H$9$k!#!K(B
$B$3$N$H$-!"(B$ =\; \subseteq R $$B$r<($;$P$h$$!#(B
\\
$BH?<MN'!#(B$ (x R x) \wedge (x=x) $$B$G$"$k!#(B
\\
$ x \rightarrow y $$B$H$9$k!#(B
$ \rightarrow\; \subseteq R \subseteq \;= $$B$h$j!"(B$ (x R y) \wedge (x=y) $$B$G$"$k!#(B
$B$^$?!"BP>NN'$h$j!"(B$ (y R x) \wedge (y=x) $$B$G$"$k!#(B
\\
$ x \rl{n} y $$B$H$9$k!#$?$@$7!"(B$ n \in \N $$B$G$"$k!#(B
$B?d0\N'$h$j!"(B$ (x R y) \wedge (x=y) $$B$G$"$k!#(B
$B$^$?!"BP>NN'$h$j!"(B$ (y R x) \wedge (y=x) $$B$G$"$k!#(B
\\
$B$h$C$F!"(B$ (x=y \Rightarrow x R y) $$B$G$"$j!"(B
$ =\; \subseteq R $$B$J$N$G!"(B$ = $$B$O!"(B$ \rightarrow $$B$r4^$`:G>.$NF1CM4X78$G$"$k!#(B


\section{$B%j%9%H(B}

$ A \neq \emptyset $$B$N$H$-!"(B
$ L $$B$N0J2<$NDj5A$,!"(B$ L \cong \seq $$B$rK~$?$9$3$H$r<($;!#(B

$ f: L \rightarrow \seq $$B$G$"$k$h$&$JA4C1<M(B$ f $$B$r8+$D$1$l$P$h$$!#(B

$B0J2<$G$O!"(B$ . \in \1 $$B$G$"$k!#(B
$BD>46E*$K!"(B
\begin{eqnarray*}
\lefteqn{\seq} \\
  &\cong&                \1
    +           A \times \1
    + A \times (A \times \1) + \cdots \\
  &=& \1
    + \set{      \$BNs(B{a,.}  | a   \in A}
    + \set{\$BNs(B{b,\$BNs(B{a,.}} | a,b \in A} + \cdots \\
  &=& \set{\$BNs(B{0,            .  }            } \cup
      \set{\$BNs(B{1,      \$BNs(B{a,.} } | a   \in A} \cup
      \set{\$BNs(B{2,\$BNs(B{b,\$BNs(B{a,.}}} | a,b \in A} \cup \cdots \\
\end{eqnarray*}
$B$G$"$k!#(B


\subsection{$ L = \sum_{n \in \N} A^n $}

\begin{eqnarray*}
L &=& A^0 + A^1 + A^2 + \cdots \\
  &=& \set{\$BNs(B{0, \$BNs(B{   }}            } \cup
      \set{\$BNs(B{1, \$BNs(B{a  }} | a   \in A} \cup
      \set{\$BNs(B{2, \$BNs(B{a,b}} | a,b \in A} \cup \cdots \\
  &=& \bigcup_{n \in \N} \set{\$BNs(B{n,s} | s \in A^n} \\
\end{eqnarray*}

$ L $$B$NMWAG$O!"<+A3?t(B$ n $$B$H!"(B$ A $$B$NNs!JD9$5(B$ n $$B!K$N(B$ 2 $$B$DAH$G$"$k!#(B
$BD9$5(B$ n $$B$N(B$ A $$BNs$O!"<!$N$h$&$K:F5"E*$KDj5A$5$l$F$$$k$b$N$H$9$k!#(B
$ \$BNs(B{a_0, a_1, \ldots, a_{n-1}} = \$BNs(B{a_0, \$BNs(B{a_1, \ldots, a_{n-1}}} $

$B$^$:!"(B$ f( \$BNs(B{0, \$BNs(B{}} ) = . $$B$H$9$k!#(B

$B:F5"E*$K(B$ f( \$BNs(B{n+1, s} ) $$B!J$?$@$7!"(B$ s \in A^{n+1} $$B!K$rDj5A$9$k!#(B
\begin{eqnarray*}
f( \$BNs(B{n+1, \$BNs(B{a_0, a_1, \ldots, a_n}} )
  &=& \$BNs(B{a_0, \$BNs(B{n, \$BNs(B{a_1, \ldots, a_n}}} \\
  &\in& A \times \set{\$BNs(B{n,s} | s \in A^n} \\
  &\subseteq& A \times L \\
\end{eqnarray*}

$B$3$&$7$F!"(B$ L $$B$+$i(B$ \seq $$B$X$NA4C1<M(B$ f $$B$rDj5A$G$-$?!#(B
$B$h$C$F!"(B$ L \cong \seq $$B$G$"$k!#(B


\subsection{$ L = (\sum_{n \in \N} A^n) + A^{\N} $}

\begin{eqnarray*}
L &=& A^0 + A^1 + A^2 + \cdots
    + (\N \rightarrow A) \\
  &=& \set{\$BNs(B{0, \$BNs(B{   }}            } \cup
      \set{\$BNs(B{1, \$BNs(B{a  }} | a   \in A} \cup
      \set{\$BNs(B{2, \$BNs(B{a,b}} | a,b \in A} \cup \cdots
    \cup \set{\set{\$BNs(B{n,a} | (n \in \N) \wedge (a \in A)}} \\
  &=& \bigcup_{n \in \N} \set{\$BNs(B{n,s} | s \in A^n}
    \cup \set{\set{\$BNs(B{n,a} | (n \in \N) \wedge (a \in A)}} \\
\end{eqnarray*}

$BA0Ld$G!"(B$ L $$B$NM-8BD9$NMWAG$+$i(B$ \seq $$B$NM-8BD9$NMWAG$X$NItJ,A4C1<M$ODj5A$G$-$F$$$k$N$G!"(B
$BL58BD9$NMWAG$N4V$NBP1~$r2C$($F!"A4C1<M(B$ f $$B$rDj5A$G$-$l$P$h$$!#(B
\begin{eqnarray*}
f( \set{\$BNs(B{n,a_n} | (n \in \N) \wedge (a_n \in A)} )
  &=& \$BNs(B{a_0, \set{\$BNs(B{n,a_{n+1}} | n \in \N}} \\
  &\in& A \times \set{\set{\$BNs(B{n,a_n} | (n \in \N) \wedge (a_n \in A)}} \\
  &\subseteq& A \times L \\
\end{eqnarray*}

$B$3$&$7$F!"(B$ L $$B$+$i(B$ \seq $$B$X$NA4C1<M(B$ f $$B$rDj5A$G$-$?!#(B
$B$h$C$F!"(B$ L \cong \seq $$B$G$"$k!#(B


\section{$B<jB3$-7?8@8l(BLC$B$N0UL#O@(B}

\subsection{\key{while}$BJ8$NA+0\0UL#O@(B}

LC$B$NA+0\0UL#O@$K(B
\\\begin{tabular}{rl}
$ \$BNs(B{B,s} $
  &$ \rightarrow \$BNs(B{B',s'} $\\
\hline
$ \$BNs(B{\while{B}{C}, s} $
  &$ \rightarrow \$BNs(B{\while{B'}{C}, s'} $\\
\end{tabular}\\
$B$rDI2C$9$k$HH/@8$9$k5sF0$rNc<($;$h!#(B

LC$B$K$*$1$k!"(B\key{while}$BJ8$N@53N$JDj5A$O!"0J2<$N$b$N$G$"$C$?!#(B
\\
$ (\rightarrow_{\mbox{wh1}}) \; \$BNs(B{\while{B}{C}, s} \rightarrow \$BNs(B{\ifStm{B}{(C; \while{B}{C})}{\nop}, s} $

$B>r7oIt(B$ B $$B$,(B\key{true}$B$KA+0\$9$k>l9g!"(B
$ \rightarrow_{wh1} $$B$G$O:F5"E*$KA+0\$,9T$o$l!"(B
$ 1 $$BEY(B$ C $$B$,<B9T$5$l$?8e$K:F$S>r7oIt$NH=Dj$,9T$o$l$k$,!"(B
$B?7$7$/DI2C$7$?Dj5A$K4p$E$$$FA+0\$r9T$&$H!"(B
$ 2 $$BEYL\$K$O>r7oIt$,>C$($F$7$^$C$F$$$k!J(B\key{true}$B$KA+0\:Q$_$G$"$k!K!#(B
$B$D$^$j!"?7$7$$Dj5A$K$h$k$H!"(B\key{while}$BJ8$O!"(B$ 0 $$B2s$+L58B2s$+$N%k!<%W$G$"$k!#(B

$BNc$($P!"(B\while{!i > 0}{i := !i - 1}$B$H$$$&J8$N(B
$B<B9T$,=*$o$k$N$+$OM=B,IT2DG=$G$"$k!#(B
Prolog$B$N$h$&$KA+0\B'$N4V$NM%@h=g0L$rDj$a$l$P!"(B
$B5sF0$NM=B,$O2DG=$@$,!"L58B%k!<%W$N5sF0$OD>46$KH?$9$k!#(B

$ \rightarrow_{wh1} $$B$rM%@h$9$l$P!"?7$7$$Dj5A$O7h$7$F;H$o$l$:!"DI2C$9$k0UL#$,$J$$!#(B
$B?7$7$$Dj5A$rM%@h$9$l$P!">r7oIt$NA+0\$,40A4$K=*$o$j!"(B
\key{true}$B$+(B\key{false}$B$K$J$C$?8e!"$=$NCM$K4p$E$$$F(B
\nop $BJ8$+L58B%k!<%W!J=*N;>uBV$KA+0\IT2DG=!K$$$:$l$+$N5sF0$r<($9!#(B
$B$b$A$m$s!"$3$N5sF0$O4V0c$C$F$$$k$N$G!"?7$7$$Dj5A$O4V0c$C$F$$$k!#(B


\subsection{\doStm{C}{B}$B$NA+0\0UL#O@$HI>2A0UL#O@(B}

$ 1 $$B2s0J>e$N7+$jJV$7$r9T$&(B\doStm{C}{B}$B$N0UL#O@$rM?$($h!#(B

$BA+0\0UL#O@$rM?$($k!#(B
\\
$ (\rightarrow_{\mbox{do}}) \; \$BNs(B{\doStm{C}{B}, s} \rightarrow \$BNs(B{(C; \while{B}{C}), s} $
\\
$ 1 $$B2sL\$N<B9T$rH=Dj$J$7$K9T$&$3$H$r=|$1$P!"(B
\while{B}{C}$B$HF1$8$G$"$k!#(B

$BI>2A0UL#O@$rM?$($k!#(B
\\
$ (\Downarrow_{\mbox{do}}) \; $
\begin{tabular}{rl}
$ \$BNs(B{C,s} $
  &$ \Downarrow \$BNs(B{\nop ,s'} $\\
$ \$BNs(B{\while{B}{C}, s'} $
  &$ \Downarrow \$BNs(B{\nop ,s''} $\\
\hline
$ \$BNs(B{\doStm{C}{B}, s} $
  &$ \Downarrow \$BNs(B{\nop ,s''} $\\
\end{tabular}\\


\section{Lisp$B4X?t$N7k9g;RDj5A(B}

$B<!$N$h$&$KDj5A$5$l$k7k9g;R$,!"(BLisp$B$NF1L>$N4pK\Dj?t$d4pK\4X?t$HF1$8$h$&$K5!G=$9$k$3$H$r3N$+$a$h!#(B
\\\begin{tabular}{rl}
\nil  &\df $ \lambda z. z $\\
\cons &\df $ \lambda xy. \pair \false (\pair x y) $\\
\nilp &\df \head \\
\car  &\df $ \lambda z. \head (\tail z) $\\
\cdr  &\df $ \lambda z. \tail (\tail z) $\\
\end{tabular}\\
$B$3$3$G(B
\\\begin{tabular}{rl}
\true  &\df $ \lambda xy. x $\\
\false &\df $ \lambda xy. y $\\
\pair  &\df $ \lambda xyf. fxy $\\
\head  &\df $ \lambda p. p \true $\\
\tail  &\df $ \lambda p. p \false $\\
\end{tabular}\\
$B$H$9$k!#(B

Lisp$B$K$*$$$F!"(B\nil $B$O6u%j%9%H$G$"$j!"(B
\cons $B$O(B$ 2 $$B$D$N0z?t$rA08eIt$K;}$D%N!<%I$rJV$7!"(B
\nilp $B$O0z?t$,6u%j%9%H$+H]$+$rH=Dj$7!"(B
\car $B$H(B\cdr $B$O%N!<%I$NA0It$H8eIt$r$=$l$>$lJV$9!#(B

\cons $B$N0z?t$K(B\nil $B$=$NB>$rM?$($F!"G$0U$N%j%9%H$r:n$l$k$3$H$r3N$+$a$k!#(B
\\
$BD9$5$,(B$ 0 $$B$N%j%9%H$O6u%j%9%H(B\nil $B$G$"$k!#(B
\\
$BD9$5$,(B$ n $$B$N%j%9%H(B$ y $$B$r:n$l$?$b$N$H$9$k!#(B
$B$=$N@hF,$KMWAG(B$ x $$B$r$D$J$2$F!"D9$5(B$ n+1 $$B$N%j%9%H$r:n$k$K$O!"(B
$ \cons x y = \pair \false (\pair x y) $$B$H$9$l$P$h$$!#(B
$B@hF,MWAG$,(B$ x $$B!";D$j$NItJ,%j%9%H$,(B$ y $$B$N%j%9%H$O0J>e$N$h$&$KI=$5$l$k!#(B

\nilp $B=R8l$N5!G=$r3N$+$a$k!#(B
\newpage
\begin{eqnarray*}
\nilp \nil
  &=& \head \nil \\
  &=& \nil \true \\
  &=& \true \\
\nilp (\cons x y)
  &=& \head (\cons x y) \\
  &=& (\cons x y) \true \\
  &=& (\pair \false (\pair x y)) \true \\
  &=& \true \false (\pair x y) \\
  &=& \false \\
\end{eqnarray*}
$B%j%9%H0J30$N0z?t$K$D$$$F$OL5;k$7$F$b$+$^$o$J$$$@$m$&!#(B

\car $B$H(B\cdr $B$N5!G=$r3N$+$a$k!#(B
\begin{eqnarray*}
\car \nil
  &=& \head (\tail \nil) \\
  &=& (\tail \nil) \true \\
  &=& \nil \false \true \\
  &=& \false \true \\
  &=& \lambda y. y \\
  &=& \nil \\
\car (\cons x y)
  &=& \head (\tail (\cons x y)) \\
  &=& (\tail (\cons x y)) \true \\
  &=& (\cons x y) \false \true \\
  &=& (\pair \false (\pair x y)) \false \true \\
  &=& \false \false (\pair x y) \true \\
  &=& (\pair x y) \true \\
  &=& \true x y \\
  &=& x \\
\cdr \nil
  &=& \tail (\tail \nil) \\
  &=& (\tail \nil) \false \\
  &=& \nil \false \false \\
  &=& \false \false \\
  &=& \lambda y. y \\
  &=& \nil \\
\cdr (\cons x y)
  &=& \tail (\tail (\cons x y)) \\
  &=& (\tail (\cons x y)) \false \\
  &=& (\cons x y) \false \false \\
  &=& (\pair \false (\pair x y)) \false \false \\
  &=& \false \false (\pair x y) \false \\
  &=& (\pair x y) \false \\
  &=& \false x y \\
  &=& y \\
\end{eqnarray*}
$B$3$3$G$b!"%j%9%H0J30$N0z?t$K$D$$$F3N$+$a$kI,MW$O$J$$$@$m$&!#(B


\section{$B4X?t7?8@8l(BFL$B$N7?(B}

$B4X?t7?8@8l(BFL$B$K$*$$$F!"0J2<$N%W%m%0%i%`$N<g7?$r5a$a$h!#(B
well-typed$B$G$J$1$l$P$=$NM}M3$r=R$Y$h!#(B
\\
$B$?$@$7(B
$ I \df \lambda x. x, \;
  K \df \lambda xy. x, \;
  S \df \lambda xyz. xz(yz) $$B$H$9$k!#(B

$B$^$:!"(B$ \lambda $$B<0$r4JLs$7$F$_$F!"(B
$B<!$K>ZL@?^$K$h$k7?:F9=@.$r;n$_$k!#(B
$B$N$@$,!"(B
$B3F%W%m%0%i%`$N<g7?$r5a$a$kA0$K!"(B$ I,K,S $$B$N<g7?$r5a$a$F$*$/!#(B
$B!J8e$+$i9M$($l$P!"(B$ K, S $$B$N<g7?$OITMW$G$7$?!#!K(B

$
\begin{array}{l}
  \\
\hline\trans{var}
  x:Y \vdash x:X \\
\hline\trans{abs}
  \vdash (\lambda x. x):Z \\
\end{array}
$
\\
$B$3$N>ZL@?^$,@5$7$$$?$a$K$O!"(B
$ Z = Y \rightarrow X, \;
  Y = X $$B$G$J$1$l$P$J$i$J$$!#(B
$B$h$C$F!"(B$ I $$B$N<g7?$O(B
\begin{eqnarray*}
Z &= Y \rightarrow X \\
  &= X \rightarrow X \\
\end{eqnarray*}
$B$G$"$k!#(B

$ K $$B$N<g7?$r5a$a$k!#(B
\\
$
\begin{array}{l}
  \\
\hline\trans{var}
  x:Y, y:W \vdash x:V \\
\hline\trans{abs}
  x:Y \vdash (\lambda y. x):X \\
\hline\trans{abs}
  \vdash (\lambda xy. x):Z \\
\end{array}
$
\\
$ Z = Y \rightarrow X, \;
  X = W \rightarrow V, \;
  Y = V $$B$G$J$1$l$P$J$i$J$$!#(B
$B$h$C$F!"(B
\begin{eqnarray*}
K:Z
  &=& Y \rightarrow    X \\
  &=& V \rightarrow (W \rightarrow V) \\
  &=& V \rightarrow  W \rightarrow V \\
\end{eqnarray*}

$ S $$B$N<g7?$r5a$a$k!#(B
\\
$
\begin{array}{l}
  \begin{array}{l}
    \frac{\mbox{(var)}}{ x:Y, y:W, z:U \vdash x:(U \rightarrow S \rightarrow T) } \;
    \frac{\mbox{(var)}}{ x:Y, y:W, z:U \vdash z:U } \\
  \hline\trans{app}
    x:Y, y:W, z:U \vdash xz:(S \rightarrow T) \\
  \end{array} \;
  \begin{array}{l}
    \frac{\mbox{(var)}}{ x:Y, y:W, z:U \vdash y:(U \rightarrow S) } \;
    \frac{\mbox{(var)}}{ x:Y, y:W, z:U \vdash z:U } \\
  \hline\trans{app}
    x:Y, y:W, z:U \vdash yz:S \\
  \end{array} \\
\hline\trans{app}
  x:Y, y:W, z:U \vdash xz(yz):T \\
\hline\trans{abs}
  x:Y, y:W \vdash (\lambda z. xz(yz)):V \\
\hline\trans{abs}
  x:Y \vdash (\lambda yz. xz(yz)):X \\
\hline\trans{abs}
  \vdash (\lambda xyz. xz(yz)):Z \\
\end{array}
$
\\
$ Z = Y \rightarrow X, \;
  X = W \rightarrow V, \;
  V = U \rightarrow T, \;
  W = U \rightarrow S, \;
  Y = U \rightarrow S \rightarrow T $$B$G$J$1$l$P$J$i$J$$!#(B
$B$h$C$F!"(B
\\\begin{tabular}{llclccc}
$ S:Z $
  &$=$&$                Y                $&$\rightarrow$&                     &$ X $& \\
  &$=$&$ (U \rightarrow S \rightarrow T) $&$\rightarrow$&$             (W    $&$\rightarrow$&$    V) $\\
  &$=$&$ (U \rightarrow S \rightarrow T) $&$\rightarrow$&$ (U \rightarrow S) $&$\rightarrow$&$ (U \rightarrow T) $\\
  &$=$&$ (U \rightarrow S \rightarrow T) $&$\rightarrow$&$ (U \rightarrow S) $&$\rightarrow$&$  U \rightarrow T $\\
\end{tabular}\\


\subsection{$ KI $}

$ KI = \lambda y. I $
$B$J$N$G!"(B$ KI $$B$N<g7?$O(B$ Y \rightarrow X \rightarrow X $$B$G$"$k!#(B

$
\begin{array}{l}
  \mbox{$B!J>ZL@:Q$_!K(B} \\
\hline\trans{}
  y:Y \vdash I:(X \rightarrow X) \\
\hline\trans{abs}
  \vdash (\lambda y. I):Z \\
\end{array}
$
\\
$ KI: Z = Y \rightarrow X \rightarrow X $$B$G$"$k$3$H$,3N$+$a$i$l$?!#(B


\newpage
\subsection{$ SS(KI) $}

\begin{eqnarray*}
SS(KI)
  &=& \lambda z. Sz((KI)z) \\
  &=& \lambda z z_1. z z_1((KI)z)z_1 \\
  &=& \lambda z z_1. z z_1   I   z_1 \\
  &=& \lambda z z_1. z z_1       z_1 \\
\end{eqnarray*}

$
\begin{array}{l}
  \begin{array}{l}
    \frac{\mbox{(var)}}{ z:Y, z_1:W \vdash z:(W \rightarrow W \rightarrow V) } \;
    \frac{\mbox{(var)}}{ z:Y, z_1:W \vdash z_1:W } \\
  \hline\trans{app}
    z:Y, z_1:W \vdash (z z_1):(W \rightarrow V) \\
  \end{array} \;
  \frac{\mbox{(var)}}{ z:Y, z_1:W \vdash z_1:W } \\
\hline\trans{app}
  z:Y, z_1:W \vdash (z z_1 z_1):V \\
\hline\trans{abs}
  z:Y \vdash (\lambda z_1. z z_1 z_1):X \\
\hline\trans{abs}
  \vdash (\lambda z z_1. z z_1 z_1):Z \\
\end{array}
$

$ Z = Y \rightarrow X, \;
  Y = W \rightarrow V, \;
  Y = W \rightarrow W \rightarrow V $$B$G$J$1$l$P$J$i$J$$!#(B
$B$3$N$?$a$K$O!"(B$ V = W \rightarrow V $$B$G$J$1$l$P$J$i$J$$!#(B

$B$3$l$O!"<+J,$HF1$87?$N4X?t$rJV$9$h$&$J4X?t$G$"$k!#(B
C$B8@8l$G$O!"<+J,$N%"%I%l%9$rJV$94X?t$,0lNc$G$"$k!#(B

FL$B$N4X?t7?$O!"4pK\7?$dD>@Q7?$N4X?t!J4pK\7?!"D>@Q7?$r0z?t$K$H$C$?$j!"CM$H$7$FJV$7$?$j$9$k!K$+!"(B
$B$=$l$i$rAH$_9g$o$;$F$9$G$KDj5A$5$l$?4X?t7?$N4X?t!JDj5A:Q$_$N4X?t7?$r0z?t$K$H$C$?$j!"CM$H$7$FJV$7$?$j$9$k!K(B
$B$N$$$:$l$+$G$"$j!"<+J,$HF1$87?$rJV$94X?t7?$O$J$$!#(B
$B$7$?$,$C$F!"(B$ SS(KI) $$B$O!"(BFL$B$K$*$$$F7?$r;}$?$J$$!#(B


\subsection{$ S(KS)K $}

\begin{eqnarray*}
S(KS)K
  &= \lambda z. (KS)z(Kz) \\
  &= \lambda z. S(Kz) \\
  &= \lambda z y z_1. (Kz)z_1(y z_1) \\
  &= \lambda z y z_1. z(y z_1) \\
\end{eqnarray*}

$
\begin{array}{l}
  \frac{\mbox{(var)}}{ z:Y, y:W, z_1:U \vdash z:(S \rightarrow T) } \;
  \begin{array}{l}
    \frac{\mbox{(var)}}{ z:Y, y:W, z_1:U \vdash y:(U \rightarrow S) } \;
    \frac{\mbox{(var)}}{ z:Y, y:W, z_1:U \vdash z_1:U } \\
  \hline\trans{app}
    z:Y, y:W, z_1:U \vdash (y z_1):S \\
  \end{array} \\
\hline\trans{app}
  z:Y, y:W, z_1:U \vdash z(y z_1):T \\
\hline\trans{abs}
  z:Y, y:W \vdash (\lambda z_1. z(y z_1)):V \\
\hline\trans{abs}
  z:Y \vdash (\lambda y z_1. z(y z_1)):X \\
\hline\trans{abs}
  \vdash (\lambda z y z_1. z(y z_1)):Z \\
\end{array}
$

$ Z = Y \rightarrow X, \;
  X = W \rightarrow V, \;
  V = U \rightarrow T, \;
  W = U \rightarrow S, \;
  Y = S \rightarrow T $$B$G$J$1$l$P$J$i$J$$!#(B

$B$h$C$F!"(B
\\\begin{tabular}{llclccc}
$ S(KS)K: Z $
  &$=$&$              Y    $&$\rightarrow$&                     &$ X $& \\
  &$=$&$ (S \rightarrow T) $&$\rightarrow$&$             (W    $&$\rightarrow$&$    V) $\\
  &$=$&$ (S \rightarrow T) $&$\rightarrow$&$ (U \rightarrow S) $&$\rightarrow$&$ (U \rightarrow T) $\\
  &$=$&$ (S \rightarrow T) $&$\rightarrow$&$ (U \rightarrow S) $&$\rightarrow$&$  U \rightarrow T $\\
\end{tabular}\\


\section{$B7W;;%b%G%kO@$N8zMQ(B}

$B7W;;%b%G%k$K4X$9$kM}O@$J$$$7$OM}O@E*;W9M$,!"$I$N$h$&$J>l9g$KLrN)$C$?$+!)(B
$BLrN)$C$?$3$H$,$J$1$l$P!"$=$l$O$J$<$+!)(B

$B7?$r=89g!"7?$NCM$r=89g$NMWAG$H8+$J$99M$(J}$O!"(B
$B%W%m%0%i%_%s%08@8l$N;EMM$r$$$/$D$+8+$F$-$?:#$G$O$4$/<+A3$K46$8$i$l$^$9!#(B
$B4D6-$+$iFHN)$7$F!"7A<0E*$K%W%m%0%i%_%s%08@8l$N;EMM$r5-=R$7$h$&$H;n$_$l$P!"(B
$B?t3X$N5-K!$r<Z$j$6$k$rF@$:!"7?BN7O$r=89gO@$K$h$C$F5-=R$9$k$N$O$b$O$d>o<1$J$N$G$7$g$&!#(B

Guy Steele$B$N!V(BCommon Lisp$B!W$d!"(B
Samuel Harbison$B$H(BGuy Steele$B$N!V?7!&>\@b(BC$B8@8l!W$K$b!"$3$N9M$(J}$,8=$l$F$$$^$9!#(B
\\
Wirth$B$N!V%W%m%0%i%_%s%08@8l(BPascal$B!W$K8=$l$F$$$?$+K:$l$^$7$?$,!"(B
Pascal$B$K$OItJ,HO0O7?$,$"$j$^$7$?!#(B
$BItJ,HO0O7?$O!"%*%V%8%'%/%H;X8~$N%5%V%/%i%9$N@h6o$1$H$$$($k$G$7$g$&!#(B
$BItJ,=89g$N9M$(J}$,$J$1$l$P=P$F$-$=$&$b$J$$%"%$%G%"$G$9!#(B
\\
Holt$B$N!V%W%m%0%i%_%s%08@8l(BTuring$B!W$O!"(BPascal$B$N3HD%$G$9!#(B
$B?tCM7?$O!"M}A[E*$K$O?t3X$N?t!J(B$ \N, R $$B!K!"(B
$B<B8=$G$O$=$NItJ,HO0O$G$"$k$H$7!"(B
$B7A<0E*@EE*0UL#O@$N7?8!::$KMxMQ$7$F$$$^$9!#(B

$B;d$,FI$s$@9b5i8@8l$N;EMM=q$O$3$l0L$G$9$,!"(B
Ada$B$NF~Lg=q$d!"%*%V%8%'%/%H;X8~$N%,%$%I$G$b!"(B
$B=89gO@$,N"$K8+$(1#$l$7$F$$$^$7$?!#(B
$B4{$K=R$Y$^$7$?$,!"ItJ,7?$d%5%V%/%i%9$O(B
$BItJ,=89g$N35G0$,$J$1$l$PM}2r$G$-$J$$$G$7$g$&!#(B

C$B8@8l$G%3!<%k%P%C%/4X?t!J4X?t0z?t!K$N35G0$rCN$C$F$+$i!"(B
$B$h$/=q$$$F$$$^$7$?!#$=$N$;$$$G!"4X?t7?$bIaDL$KM}2r$G$-$^$7$?!#(B
C$B8@8l$rCN$i$J$1$l$P!"4X?t7?$H4X?t$N7k2L$N7?$r6hJL$G$-$J$+$C$?$+$b$7$l$^$;$s!#(B
$B!J(BC$B8@8l$G$O!"<B:]$K$O4X?t7?$G$O$J$/!"4X?t$r;X$9%]%$%s%?$G$9$,!#!K(B

$B$3$&$7$F$_$k$H!"9b5i8@8l$N9b5i$5$O!"(B
$B7W;;%b%G%k$K4X$9$kM}O@$KN"IU$1$i$l$F$$$k$h$&$G$9!#(B
$B$7$?$,$C$F!"9b5i8@8l$r9b5i$KM}2r$9$k$N$K$b!"(B
$B7W;;%b%G%k$K4X$9$kM}O@E*AGM\$,I,MW$J$N$@$H;W$o$l$^$9!#(B

$BM}O@$,%W%m%0%i%_%s%0$KD>@\LrN)$D$H$$$&$h$j$b!"(B
$B%W%m%0%i%_%s%0$K;H$o$l$kF;6q$,M}O@$N@.2L$G$"$C$?$j!"(B
$BF;6q$rM}2r$9$k$N$KM}O@$N=u$1$,$"$C$?$j!"(B
$B$"$k$$$O!"(B
$B%3!<%G%#%s%0CJ3,$G$J$/!"%W%m%0%i%`@_7W$J$IAa$$CJ3,!"(B
$B%W%m%0%i%`$N=$@5$J$ICY$$CJ3,$G!"M}O@$,LrN)$A$^$7$?!#(B


\end{document}
