\documentclass{jarticle}
\usepackage{latexsym,amssymb,amsmath,amsthm,proof}
\pagestyle{plain}

\newtheorem{df}{��`}[section]
\newtheorem{thm}[df]{�藝}
\newtheorem{cor}[df]{�n}
\newtheorem{lemma}[df]{���}
\newtheorem{ex}[df]{��}

\def\equivdef{\equiv_{def}}
\def\equalbe{\ \ =_{\beta \eta}\ \ }
\def\BCKbe{BCK\beta \eta}
\def\Eqbe{\beta \eta}
\def\verifyonnj{\ \ \vdash_{NJ}\ \ }
\def\verifyonbck{\ \ \vdash_{\beta \eta}\ \ }
\def\Lra{\ \ \Longrightarrow\ \ }
\def\Lla{\ \ \Longleftarrow\ \ }
\def\Llra{\ \ \Longleftrightarrow\ \ }
\def\fvsets#1#2#3{j#1_{#2}, \dots, j#1_{#3}}
\def\varsets#1#2#3{#1_{#2}, \dots, #1_{#3}}
\def\triquad{\qquad\qquad\qquad}
\def\circed#1{#1^{\circ}}

\def\betaeq{=_\beta}
\def\defeq{\stackrel{\mathrm{def}}{=}}
\def\num#1{\widetilde{#1}}
\def\nnum#1{{\num{#1}}^*}
\def\q{\hspace*{1em}}
\def\tif{\textbf{if}}
\def\tthen{\textbf{then}}
\def\telse{\textbf{else}}
\def\tendif{\textbf{endif}}

\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% �\��
\thispagestyle{empty}
\vspace*{1cm}
\begin{center}
{\Large\gt ��t��w��w�@�@���R�Ȋw�����ȁ@\\[3mm]�C�m�_��}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf �����_���̃����K�`�����߂�v���O�����̍������ɂ���}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large 2008�N3��}
\end{center}

\vspace*{5.7cm}
\begin{center}
{\Large\gt ���w�E��񐔗��w ��U \\[2mm]��񐔗��w �u��}
\end{center}

\vspace*{5mm}
\begin{center}
{\Large\gt ���с@���R�M}
\end{center}

\setcounter{page}{0}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% �ڎ�
\tableofcontents

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�͂��߂�}
�����_���� $ \beta $ ���K�`�����߂���ɂ��ē����̏C�m�_���ŁA�����_���������q��p���ă����_�������������ɕϊ����ϊ��K����p���Ă���ȏ�ό`�ł��Ȃ��`�ɂ�����A
���炽�߂ă����_���ɕϊ��� $ \beta $ ���K�`�����߂�Ƃ�����@���Ă����\�����B

�����̏C�m�_���ł́A�����̃v���O������p���ă����_���� $ \beta $ ���K�`���v�Z�@�ŋ��߂�ƃ����_���̂܂܌v�Z������̂�������������Ƃ������_���o����Ă���B

�������A���̓����̃v���O�����ł̍������̗��R�ɂ��Ắu�����q�̒u�������̍ۂɍœK�����s���Ă��邽�߂ƍl������v�Ƃ����\�z�݂̂��Ȃ���Ă��āA���ۂɌ��؂͍s���Ă��Ȃ��B


�{�_���ł́A�����q�̒u���������s���ۂɍœK�����s���v���O�����ƍs��Ȃ��v���O�����̗������쐬���A���s���Ԍv���Ɣ�r���s�����̖��ƃ����_���� $ \beta $ ���K�`�����߂�v���O�����̍������ɂ��čl�@���s�����B

�Ȃ��A���̘_���͌ÐX�Y��搶���ڍׂȕ��j��^�����A�����̌����E���؂����т��s�����B

\section{�����_�v�Z}

\subsection{�����_��}

\begin{df}[�����_��] 
�����_�����ȉ��Œ�`����B

\vspace{5mm}

\begin{enumerate}
  \item �ϐ��̓����_���ł���B
  \item $ M $ �� $ M $ �������_���ł���΁A$ (MN) $ �̓����_���ł���B�i�K�p�j
  \item $ x $ �ƕϐ� $ M $ �������_���̂Ƃ��A $ ( \lambda x.M) $ �̓����_���ł���B�i���ہj
\end{enumerate}

\end{df}

\vspace{8mm}

\begin{df}[���]
$ M , N $ �������_���A $ x $ ��ϐ��Ƃ���B
$ M $ �̒��̎��R�ϐ� $ x $ �� $ N $ �����������ʁ@$ [N/x]M $ �����̂悤�ɋA�[�I�ɒ�`����B

\vspace{4mm}

\begin{enumerate}
  \item $ [N/x]x \equiv N ,$
  \item $ [N/x]M \equiv M $ \hspace{2mm} $( x\notin FV(M) )$ ,
  \item $ [N/x](QR) \equiv ([N/x]Q \hspace{1mm} [N/x]R) $ \hspace{2mm} �i $ x \in FV(QR) $ �̂Ƃ��j,
  \item $ [N/x]( \lambda y.Q) \equiv \lambda y.[N/x]Q $ \hspace{2mm} �i $ x \in FV(Q) $ ���� $ y \notin FV(N) $ �̂Ƃ��j,
  \item $ [N/x]( \lambda y.Q) \equiv \lambda z.[N/x][z/y]Q $ \hspace{2mm} �i $ x \in FV(Q) $ ���� $ y \in FV(N) $ �̂Ƃ��j.
\end{enumerate}

������ $ y \not \equiv x $ �͉��肳��Ă���B�܂��A $ z $ �� $NQ$ �ɏo�����Ă��Ȃ��ŏ��̕ϐ��ł���B

\end{df}


\subsection{���ϊ�}
�����_���� $ \beta $ �ϊ����ȉ��̂悤�ɒ�`����B\\

1. $ \hspace{1mm} ( \lambda x.M)N {\rhd}_{1 \beta} [N/x]M $ 

2. $ \hspace{1mm} M {\rhd}_{1 \beta} N $ �Ȃ�΁A $ \lambda x.M {\rhd}_{1 \beta} \lambda x.N, \hspace{3mm} MP {\rhd}_{1 \beta} NP, \hspace{3mm} PM {\rhd}_{1 \beta} PN $ 


\section{CLt-��}

CLt-�����ȉ��̂悤�ɒ�`����B

\begin{df}[CLt-��]

\vspace{4mm}

1. \hspace{1mm} �ϐ��� 5 �萔�L�� $\mathsb{I}, \mathsb{K'}, \mathsb{B'}, \mathsb{C'}, \mathsb{S'}$ ��CLt-���ł���B

2. \hspace{1mm} $ M $ �� $ N $ ��CLt-���Ȃ�΁A $ (MN) $ ��CLt-���ł���B

\end{df}

\vspace{6mm}

\begin{df}[�ϊ��K��]

\vspace{4mm}

\[ ( \mathsb{I} ) \hspace{1mm} \mathsb{I} M {\rhd}_{1wt} M , \hspace{2mm} ( \mathsb{K'} ) \hspace{1mm} \mathsb{K'} MNRU {\rhd}_{1wt} MNR , \hspace{2mm} ( \mathsb{B'} ) \hspace{1mm} \mathsb{B'} MNRU {\rhd}_{1wt} MN(RU) , \]

\[ ( \mathsb{C'} ) \hspace{1mm} \mathsb{C'} MNRU {\rhd}_{1wt} M(NR)U, \hspace{2mm} ( \mathsb{S'} ) \hspace{1mm} \mathsb{S'} MNRU {\rhd}_{1wt} M(NU)(RU). \]

\end{df}


\section{�����_������CLt-���ւ̕ϊ�}

������ CLt-�� $M$�A�ϐ� $x$ �ɑ΂���, �ϐ� $x$ ���܂܂Ȃ� CLt-�� $( {\lambda}^t x.M) $ ���A�[�I�ɒ�`��
��B���̒�`�̂ɂ�����, �K�p�ł����`����ȏ゠��Ƃ��͏��Ȃ��ԍ��̒�`��K�p����B
�{�_���ł͋A�[�I��`�ɂ����Ă�, �K�p�ł����`����ȏ゠��Ƃ��͏��Ȃ��ԍ��̒�`��K�p���邱�ƂƂ���B
\begin{df}[�ϊ� $t$]\em  \ 
	\begin{enumerate}
		\item $(\lambda^t x.x) \equiv \mathsb{I}$,
		\item $(\lambda^t x. MUV) \equiv \mathsb{K'}MUV$ \ \ $(M$ �������� $x\notin FV(UV)$ �̎� $ ) $,
		\item $(\lambda^t x. MUV) \equiv \mathsb{B'}MU(\lambda^t x.V)$ \ \ $(M$ �������� $x\notin FV(U)$ �̎� $)$,
		\item $(\lambda^t. MUV) \equiv \mathsb{C'}M((\lambda^t x.U)V)$ \ \ $(M$ �������� $x\notin FV(V)$ �̎� $)$,
		\item $(\lambda^t x. MUV) \equiv \mathsb{S'}M(\lambda^t x.U)(\lambda^t x.V)$ \ \ $ ( M$ ���� $ ) $,
		\item $(\lambda^t x. MN) \equiv (\lambda^t x. \mathsb{I} MN)$,
		\item $(\lambda^t x.M) \equiv (\lambda^t x. \mathsb{II} M)$ .
	\end{enumerate}
\end{df}

\begin{ex}

$M$ �������� $x\notin FV(U)$ ���� $x \notin FV(V)$ �ł��� $(\lambda^t x. MUV) $ �̏ꍇ�A3�ł͂Ȃ�2���K�p����A
\[ (\lambda^t x. MUV) \equiv \mathsb{K'}MUV \]
�ƂȂ�B

\end{ex}

��L�̕ϊ��ł͍œK�����s����B\\
�{�_���ō쐬�����v���O�����ł͈ȉ��̕ϊ���p���A�œK�����s��Ȃ������B\\

\begin{df}[�ϊ� $t$]\em  \
	\begin{enumerate}
		\item $(\lambda^t x.x) \equiv \mathsb{I}$,
		\item $(\lambda^t x. MUV) \equiv \mathsb{S'}M(\lambda^t x.U)(\lambda^t x.V)$ \ \ $ ( M$ ���� $ ) $,
		\item $(\lambda^t x. MN) \equiv (\lambda^t x. \mathsb{I} MN)$,
		\item $(\lambda^t x. M) \equiv \mathsb{K'II}M$ .
	\end{enumerate}

\end{df}

�܂����̂悤�Ȏア�œK���̃v���O�������쐬�����B
\begin{df}[�ϊ� $t$]\em  \ 
	\begin{enumerate}
		\item $(\lambda^t x.x) \equiv \mathsb{I}$,
		\item $(\lambda^t x. M) \equiv \mathsb{K'II}M \ \ (x \notin FV(M))$ ,
		\item $(\lambda^t x. MUV) \equiv \mathsb{S'}M(\lambda^t x.U)(\lambda^t x.V)$ \ \ $ ( M$ ���� $ ) $,
		\item $(\lambda^t x. MN) \equiv (\lambda^t x. \mathsb{I} MN)$.
	\end{enumerate}

\end{df}

\begin{df}[�ϊ� $ \circed{} $] 

�����_������CLt-���ւ̕ϊ� $ \circed{} $ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B

\begin{enumerate}
  \item $\circed{x} \equiv x$
  \item $\circed{(MN)} \equiv \circed{M}\circed{N}$
  \item $\circed{(\lambda x . M)} \equiv \lambda x^t . \circed{M}$
\end{enumerate}

\end{df}



\section{CLt-�����烉���_���ւ̕ϊ�}

CLt-�����烉���_���ւ̕ϊ����ȉ��Œ�`����B

\begin{enumerate}
\item $x^{\star} \equiv x $
\item ${\mathsb{I}}^{\star} \equiv \lambda x . x$
\item ${\mathsb{K'}}^{\star} \equiv \lambda xyzu.xyz$
\item ${\mathsb{B'}}^{\star} \equiv \lambda xyzu.xy(zu)$
\item ${\mathsb{C'}}^{\star} \equiv \lambda xyzu.x(yu)z$
\item ${\mathsb{S'}}^{\star} \equiv \lambda xyzu.x(yu)(zu)$
\item ${(MN)}^{\star} \equiv MN $
\end{enumerate}

\section{�����l�ł��邱�Ƃ̏ؖ�}

�����_�� $ M $ �ɂ��̕��@��p���ċ��߂�ꂽ���̂��A $ M $ �� $ \beta $ ���K�` M* �� $ \alpha $ ���l�ł��邱�Ƃ͓����̏C�m�_���ŏؖ�����Ă���B
�œK���Ȃ��̏ꍇ�����l�ɍl���邱�Ƃ��ł���B

\section{�œK��}

�������쐬���������_���� CLt-���ɕϊ����� $ \beta $ ���K�`�����߂�v���O�����ł́A
�����_������CLt-���ւ̕ϊ��̍� $\mathsb{K', B', C'}$ ��p����Ƃ��Ƀ����_���ɂ���ϐ���
���R�Ɋ܂܂�Ă��邩�ǂ����Ƃ����O���[�o���ȏ������p�����œK�����s���Ă���B
���̂��߂ɍ��������s��ꂽ�̂ł͂Ȃ����Ɨ\�z����Ă���B\\

�����̃v���O�����ł́A��`4.1 �̕ϊ���p�����B\\

�{�_���ō쐬�����v���O�����ł́A�œK�����s��Ȃ��v���O�����Œ�`4.3�A�ア�œK�����s���v���O�����Œ�`4.4��p�����B�@\\


\section{�v���O�����ƍl�@}

�{�����ł́A�œK�����s���v���O�����ƍs��Ȃ��v���O�������쐬���A���s���Ԃ̔�r�ƍl�@���s�����B\\
�{�͂ł͂��̌��ʂɂ��ďq�ׂ�B

\subsection{��i���̌v�Z}

���͂̕��@�ƕ\���͓������쐬�����v���O�����Ƃ̔�r��e�Ղɂ��邽�߂ɓ����ɂ����B

�܂��A�e���͂̒�`�ɂ��Ă�$2005$�N�̑�Ƃ̏C�m�_���ł̒�`���Q�l�ɂ����B
����ɂ��ďq�ׂ�B


\subsubsection{��i���̒�`}
��i���\���ŗp����A$ \nnum{1} $ �A $ \nnum{0} $ �A$ \nnum{-1} $ ���ȉ��̃����_���Œ�`����B\\
\[ \nnum{1}= \lambda xyz . x =N1 \]
\[ \nnum{0}= \lambda xyz . y =N0 \]
\[ \nnum{-1}= \lambda xyz . z =Nm1 \]


\subsubsection{�����_�v�Z�ɂ���i���\���̂��߂̒�`}

\df{Pair}
$ <M,N> $ �͑΂�\���B
���̑΂��ȉ��̂悤�ɒ�`����B

\[ Pair \defeq \lambda \hspace{1mm} x.x \hspace{1mm} M \hspace{1mm} N \]

\df
$ 1,0,-1 $ �̏ꍇ�� $ 0 $ �A�� $ <M,N> $ �̏ꍇ�� $ M $ ��Ԃ������_�� $ Hdr $ ���ȉ��Œ�`����B

\[ Hdr \defeq \lambda x.(Isn \hspace{1mm} x) \hspace{2mm} 0 \hspace{2mm} (xK) \]

�܂��A$1,0,-1$�̏ꍇ�͂��̂܂܁A�� $ <M,N> $ �̏ꍇ��N��Ԃ������_��Ftr���ȉ��Œ�`����B

\[ Ftr \defeq \lambda x.(Isn \hspace{1mm} x) \hspace{2mm} x \hspace{2mm} (x(KI)) \]

$ T $ �� $ F $ ���`����B\\
�܂��A$ 1,0,-1 $ �̏ꍇ�� $ T $ �A�� $ <M,N> $ �̏ꍇ�� $ F $ ��Ԃ������_�� $ Isn $ ���ȉ��Œ�`����B

\[ T \defeq \lambda xy.x \]

\[ F \defeq \lambda xy.y \]

\[ Isn \defeq \lambda x.x K^3_3 KKIFT \]

�������A$ K^3_3 \equiv \lambda xyz.z $ �ł���B

\df{�J��オ��}

$ 1 $ ���̐����m�����Z�����Ƃ��A�J��オ��̒l��Ԃ������_�� $ Add_1 $ �ƁA�J��オ���؂�̂Ă��l��Ԃ������_�� $ Add_2 $ ���ȉ��Œ�`����B

\begin{equation*}
\begin{array}{rcrccc}
Add_1 & \defeq & \lambda x y z. x \, (y & (z \, \nnum{1} \, \nnum{1} \, \nnum{0}) & (z \, \nnum{1} \, \nnum{0} \, \nnum{0})  & \nnum{0}                              )   \\
      &        &                     (y & (z \, \nnum{1} \, \nnum{0} \, \nnum{0}) & \nnum{0}                               & (z \, \nnum{0} \, \nnum{0} \, \nnum{-1} ))  \\
      &        &                     (y & \nnum{0}                              & (z \, \nnum{0} \, \nnum{0} \, \nnum{-1}) & (z \, \nnum{0} \, \nnum{-1} \, \nnum{-1})) \\
\\
Add_2 & \defeq & \lambda x y z. x \, (y & (z \, \nnum{1} \, \nnum{0} \, \nnum{1}) & (z \, \nnum{0} \, \nnum{1} \, \nnum{0})  & z                                    )   \\
      &        &                     (y & (z \, \nnum{0} \, \nnum{1} \, \nnum{0}) & z                                     & (z \, \nnum{0} \, \nnum{-1} \, \nnum{0} ))  \\
      &        &                     (y & z                                    & (z \, \nnum{0} \, \nnum{-1} \, \nnum{0}) & (z \, \nnum{-1} \, \nnum{0} \, \nnum{-1})) \\
\end{array}
\end{equation*}

�Ȃ��A$ x $ �͌J��オ��A$ y,z $ �͉��Z���鐔��\���A���ꂼ�� $ \nnum{1} , \nnum{0} , \nnum{-1} $ ����́B

\df{���Z�̒�`}

\begin{quote}
$Add^* = \lambda x y z .$ \\
\q ($Isn$ $y$) \\
\q\q (($Isn$ $z$) \\
\q\q\q ($Pair$ ($Add_1$ $x$ $y$ $z$) ($Add_2$ $x$ $y$ $z$)) \\
\q\q\q ($Pair$ ($Add^*$ ($Add_1$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)) ($Hdr$ $y$) ($Hdr$ $z$)) \\
\q\q\q\q ($Add_2$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)))) \\
\q\q ($Pair$ ($Add^*$ ($Add_1$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)) ($Hdr$ $y$) ($Hdr$ $z$)) \\
\q\q\q ($Add_2$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)))
\end{quote}

�����p���ē�̃����_�������Z���郉���_�� $ Add $ ���ȉ��Œ�`����B

\begin{equation*}
Add \defeq Add^* \, \nnum{0}
\end{equation*}


���̃v���O�����ƃ}�j���A���Ɠ��̓t�@�C���ɂ��ẮA\\
http://www.math.s.chiba-u.ac.jp/$\tilde{\,\,\,}$05um0303/ \\
�ɍڂ���\��ł���B\\


�܂��A�e�v���O�����̎��s��͈ȉ��ł���B\\
���͂̌v�Z�����̂݌f�ڂ���B

\ex{�œK�����s���v���O�����̎��s��}

\begin{enumerate}

\item

$>$ Add N1 N1; 
-------------------kekka----------------------\\
(lambda x . x (lambda x y z . x) (lambda x y z . y))\\
0 SEC\\
----------------------------------------------\\
$>$ \\


\item
$>$ Add (lambda x . x N1 N1)(lambda x . x (lambda x . x N1 N0)N0); 
-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x))\\
0 SEC\\
----------------------------------------------\\
$>$ \\

\item
$>$ Add\\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x \\
(lambda x.x N1 N0)Nm1)N1)N0)N0)Nm1)N1) \\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x \\
(lambda x.x N1 Nm1)N0)Nm1)N1)N1)N1)N0)Nm1)Nm1)N0); \\

-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x y z . y) (lambda x y z . x)) (lambda x y z . z)) (lambda x y z . y)) \\
(lambda x y z . y)) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . y)) \\
(lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x))\\
0 SEC\\
----------------------------------------------\\
$>$ \\

\item
$>$ Add\\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x N0 N1) N1)N1)N0)N0)N1)N0)N0)N1)N0)N1)N1)N1) \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x N0 N1) N0)N0)N1)N0)N1)N1)N0)N1)N0)N1)N1)N0)N0); \\

-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x y z . y) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y)) \\
(lambda x y z . y)) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x)) \\
(lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y))(lambda x y z . x)) (lambda x y z . x)) \\
62 SEC\\
----------------------------------------------\\
$>$ \\


\end{enumerate}

\ex{�œK�����s��Ȃ��v���O�����̎��s��}

\begin{enumerate}

\item

$>$ Add N1 N1; 
-------------------kekka----------------------\\
(lambda x . x (lambda x y z . x) (lambda x y z . y))\\
0 SEC\\
----------------------------------------------\\
$>$ \\


\item
$>$ Add (lambda x . x N1 N1)(lambda x . x (lambda x . x N1 N0)N0); 
-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x))\\
0 SEC\\
----------------------------------------------\\
$>$ \\

\item
$>$ Add\\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x \\
(lambda x.x N1 N0)Nm1)N1)N0)N0)Nm1)N1) \\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x \\
(lambda x.x N1 Nm1)N0)Nm1)N1)N1)N1)N0)Nm1)Nm1)N0); \\

-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x y z . y) (lambda x y z . x)) (lambda x y z . z)) (lambda x y z . y)) \\
(lambda x y z . y)) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . y)) \\
(lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x))\\
3 SEC\\
----------------------------------------------\\
$>$ \\

\item
$>$ Add\\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x N0 N1) N1)N1)N0)N0)N1)N0)N0)N1)N0)N1)N1)N1) \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x (lambda x.x \\
(lambda x.x (lambda x.x N0 N1) N0)N0)N1)N0)N1)N1)N0)N1)N0)N1)N1)N0)N0); \\

-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x \\
(lambda x y z . y) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y)) \\
(lambda x y z . y)) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x)) \\
(lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . y))(lambda x y z . x)) (lambda x y z . x)) \\
115 SEC\\
----------------------------------------------\\
$>$ \\


\end{enumerate}

������̃v���O�������v�Z���������s���Ă���B\\


\subsection{���Ԃ̌v��}

�ȉ���3��ނ̃v���O�����̎��Ԍv���Ɣ�r���s�����B

\vspace{5mm}

�v���O����1�F�������쐬������`4.1 �ɂ�胉���_����CLt-���Ɉ�U���� $ \beta $ �ϊ����s���v���O����\\

�v���O����2�F�����_�����`4.4 �ɂ�� CLt-���Ɉ�U���� $ \beta $ �ϊ����ア�œK����p���čs���v���O���� \\

�v���O����3�F�����_�����`4.3 �ɂ��œK�����Ȃ��� CLt-���Ɉ�U���� $ \beta $ �ϊ��ōs���v���O���� 

�v���O����4�F�������쐬���������_����CLt-���ɕϊ������� $ \beta $ �ϊ����s���v���O���� \\

\vspace{5mm}

�v���O����1�A�v���O����2�ɂ��ẮA�ȉ��̏����œ�i���̉��Z�̎��s���Ԃ̌v�����s�����B

\begin{itemize}
\item ���͗p�t�@�C���̓��e�́A���Z�Ɋւ����`�Ɠ��̓f�[�^�ł���B
\item ���̓f�[�^�͌v�Z�����ɕ��ׂ��B
\item ���̓���� $ 100 $ ��s���A�e�v���O�����ł̎��s���Ԃ̕��ς�������B
\end{itemize} 

���ʁA���ꂼ��̃v���O�����̎��s���Ԃ͈ȉ��̂悤�ɂȂ����B\\
���A���ʓ��̌����͓�i���̌����ł���B\\


�v���O����3�A�v���O����4�ɂ��ẮA�ȉ��̏����œ�i���̉��Z�̎��s���Ԃ̌v�����s�����B

\begin{itemize}
\item ���͗p�t�@�C���̓��e�́A���Z�Ɋւ����`�Ɠ��̓f�[�^�ł���B
\item ���̓f�[�^�͌v�����Ƃɏ����������B
\item ���̓�����v���O����3�ł�$10$��A�v���O����4�ł�$4$��s���A�e�v���O�����ł̎��s���Ԃ̕��ς�������B
\item �\����E�̓������I�[�o�[�ɂ��G���[�̔�����\���A�l�̓G���[�̔����܂łɂ����������Ԃ�\���B
\end{itemize} 


\begin{center}
\begin{tabular}{|l|r|r|r|r|}
\hline
& �v���O����1 & �v���O����2 & �v���O����3  & �v���O����4 \\ \hline
1�{1�i1���{1���j& 0.01 & 0.01  & 0.5 & 4.5 \\ \hline
2�{3�i2���{2���j& 0.09 & 0.01  & 0.7 & 211 \\ \hline
5�{7�i3���{3���j & 0.01 & 0.04 & 1.2 & 261.5 \\ \hline
11�{14�i4���{4���j & 0.02 & 0.20 & 1.0 & 270.5E \\ \hline
21�{27�i5���{5���j & 0.12 & 0.29  & 1.9 & 277.5E \\ \hline
32�{45�i6���{6���j & 0.27 & 0.52 & 2.0 & 278.25E \\ \hline
32�{74�i6���{7���j & 0.01 & 0.31 & 7.4 & 288.25E \\ \hline
64�{74�i7���{7���j & 0.02 & 0.30 & 14.5 & 279E \\ \hline
127�{127�i7���{7���j & 0.03 & 0.99 & 19.4 & 258.5E \\ \hline
127�{136�i7���{8���j & 0.01 & 0.80 & 40.2 & 268E \\ \hline
136�{202�i8���{8���j & 0.42 & 1.59  & 41.4 & 260.75E \\ \hline
202�{262�i8���{9���j & 0.08 & 1.37  & 49.0E & 269E \\ \hline
262�{457�i9���{9���j & 0.45 & 2.34  & 51.2E & 270.25E \\ \hline
457�{602�i9���{10���j & 0.54 & 2.51  & 50.3E & 268E \\ \hline
602�{878�i10���{10���j & 0.66 & 3.37  & 48.6E & 272.25E \\
\hline
\end{tabular}
\end{center}

\subsection{�v�����ʂ̍l�@}

�v���O�����̎��s�ƌv���̌��ʁA\\
�v���O����1�A�v���O����2�A�v���O����3�A�v���O����4�̏��ɍ����Ō��ʂ����߂�ꂽ�B

�v���O����1�ƃv���O����3�̌v�����ʂ̍����A�v���O����3�ƃv���O����4�̌v�����ʂ̍��̕����͂邩�ɑ傫���B
���_�Ƃ��āA�����̃v���O�����̍������͍œK��������ƍl�����邪�A�����_�����璼�ډ������߂�v���O�����Ƃ̎��s���Ԃ̔�r����A�����q�ɕϊ��������Ƃ̕��������Ƃ��đ傫���ƍl������B

\section{�ӎ�}

�{�_���쐬�ɂ�����A�w�������̌ÐX�Y��搶�A�Ȃ�тɌÐX�������̊F�l��
����Ȃ����͂𒸂��܂������Ƃ�S���犴�ӂ������܂��B

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{9}
\bibitem{} ��t��w���w��2005�N�x�@�O����񐔊w1�z�z�����@�ÐX�Y�꒘
\bibitem{} ��t��w���R�Ȋw������2004�N�x�C�m�_���@�u�����_�v�Z�ɂ�����2�i���v�Z�v��ƍK�q��
\bibitem{} ��t��w���R�Ȋw������2004�N�x�C�m�_���@�u�����_���̃����K�`�������q��p���ċ��߂���@�v�������G���@\\
$ http://www.math.s.chiba-u.ac.jp/\tilde{\,\,\,}komori/masters\_thesis/2005/ $

\end{thebibliography}

\end{document}
