\documentclass[a4j]{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}}

\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 �����_�v�Z�ɂ�����2�i���v�Z}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����17�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 ��ƍK�q}
\end{center}

\setcounter{page}{0}

\newpage

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

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�͂��߂�}

�����_�v�Z�ɂ����鐔�̕\���Ƃ��Ă͗Ⴆ�Ύ��̂悤�Ȃ��̂��m���Ă���B

\bigskip

\begin{itemize}
\item (�`���[�`��) \\
���R�� n (n $\ge$ 0) �ɑ΂��ă����_�� $\bar{n}$ ���ȉ��̂悤�ɒ�߂�B
\begin{equation*}
\bar{n} \defeq \lambda f x . f^nx
\end{equation*}
������ $M^nN$ �͈ȉ��̒ʂ�B
\begin{equation*}
\begin{array}{rcll}
X^n Y & \equiv & \underbrace{X(X(\dots(X}_{n��X}Y)\dots)) \\
X^0 Y & \equiv & Y
\end{array}
\end{equation*}

\item
���R�� n (n $\ge$ 0) �ɑ΂��ă����_�� $^\lceil n ^\rceil$ ���ȉ��̂悤�ɒ�߂�B
\begin{equation*}
\begin{array}{rcll}
T & \defeq & \lambda x y . x \\
F & \defeq & \lambda x y . y \\
M . N & \defeq & \lambda x . x M N \\
{[ M_1, \dotsc, M_n ]} & \defeq & \begin{cases}
                                    I & n = 0 \\
                                    M_1 . [ M_2, \dotsc, M_n ] & n > 0
                                  \end{cases} \\
^\lceil n ^\rceil & \defeq & [\underbrace{F, \dotsc, F}_{n��F}]
\end{array}
\end{equation*}

\end{itemize} 
�����͂���������R�� n �ɑ΂��āA1�߂̏ꍇ�� n �� f�A2�߂̏ꍇ�� n �� F
�Ƃ����悤�ɁA���R���������_�v�Z��ł�1�i���Ƃ݂Ȃ��Čv�Z���s�����̂ł���B
������1�i���Ƃ݂Ȃ��ꍇ�A�\�L�������I�łȂ������艉�Z�̃R�X�g�������ȂǁA
�l�X�ȏ�ʂɂ����Č������グ�邱�Ƃ��ł��Ȃ��B \\
�����Ŗ{�_���ł́A���R���������_�v�Z���2�i���Ƃ݂Ȃ��Đ��̒�`��l�����Z�̒�`���s���A
���R����̔C�ӂ̊֐�������2�i���Ƃ݂Ȃ��������_�v�Z��Œ�`�\�ł��邱�Ƃ��������B

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{��{�I�ȃ����_��}

\begin{df} �����_�� $K , I$ �����̂悤�ɒ�`����B

\begin{equation*}
\begin{array}{rcll}
K & \equiv & \lambda x y . x \\
I & \equiv & \lambda x . x
\end{array}
\end{equation*}

\end{df}

\begin{df} �����_�� $Pair$ �����̂悤�ɒ�߂�B

\begin{equation*}
Pair \defeq \lambda x . x M N \quad M, N �̓����_��
\end{equation*}

���̂Ƃ� $M, N$ �� $\textbf{��}$ �ł���Ƃ����A�ȉ��ł͏󋵂ɉ����ĊȒP�̂��߂�

\begin{equation*}
<M, N>
\end{equation*}

�Ə����B

\end{df}

\begin{df}
i, j �����R�� ���� $i \ge 1$ ���� $1 \le j \le i$ �̂Ƃ��A�����_�� $K^i_j$ ��
���̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
K^i_j & \equiv & \lambda x_1 \dots x_i . x_j & i,j : ���R�� ���� i \ge 1 ���� 1 \le j \le i
\end{array}
\end{equation*}

\end{df}

\begin{df} (�^�U�l) \\
�����_�� $T, F$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
T & \equiv & \lambda x y . x \\
F & \equiv & \lambda x y . y \\
\end{array}
\end{equation*}

$T, F$ �����̂悤�ɒ�߂邱�ƂŁA�����_�� $LMN$ �ɑ΂��āA$L$ �� $T$ �̏ꍇ�� $M$�A$L$ ��$F$ �̏ꍇ�� $N$ �Ƃ��邱�Ƃ��ł���B

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{���̒�`}
\begin{df} (1���̐�) \\
���� $1, 0, -1$ �ɑΉ����郉���_��
$\nnum{1}, \nnum{0}, \nnum{-1}$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
\nnum{1} & \equiv & \lambda x y z . x \\
\nnum{0} & \equiv & \lambda x y z . y \\
\nnum{-1} & \equiv & \lambda x y z . z \\
\end{array}
\end{equation*}

\end{df}

\begin{df} (���̕\��) \\
���� n �����̂悤�ɕ\����Ƃ���B

\begin{center}
$n$ = $2^i * x_i$ + $2^{i-1} * x_{i-1}$ + $2^{i-2} * x_{i-2}$ + \dots + $2^0 * x_0$ \quad $i \ge 0$ \\
$x_j$ ($0 \le j \le i$) �� 1 �܂��� 0 �܂��� -1
\end{center}

���̐��� n �ɑΉ����郉���_�� $\num{n}$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
\num{n} & \equiv & <\dots<<<\num{0}, \num{x_i}>, \num{x_{i-1}}>, \num{x_{i-2}}>, \dots >, \num{x_0}>
\end{array}
\end{equation*}

�������A$x_k$ ($0 \le k \le i$) ���� $x_i$ �ɂ͘A������ $\num{0}$ ������Ȃ����ƁA�܂�
$x_k$ �ɂ� $\num{1}$ �� $\num{-1}$ �������ɂ͌���Ȃ����ƂƂ���B
\end{df}

\begin{ex}
���� $5$ �ɑΉ����郉���_�� $\num{5}$ ���l����B
\begin{equation*}
5 = 2^2*1 + 2^1*0 + 2^0*1
\end{equation*}
�ł���̂ŁA$\num{5}$ ��
\begin{equation*}
\num{5} = <<<\nnum{0}, \nnum{1}>, \nnum{0}>, \nnum{1}>
\end{equation*}
�ƕ\�����Ƃ��ł���B \\
�܂�
\begin{equation*}
5 = 2^4*0 + 2^3*0 + 2^2*1 + 2^1*0 + 2^0*1
\end{equation*}
�ł��邪�A
\begin{equation*}
\num{5} = <<<<<\nnum{0}, \nnum{0}>, \nnum{0}>, \nnum{1}>, \nnum{0}>, \nnum{1}>
\end{equation*}
�ƕ\�����Ƃ͂ł��Ȃ��B(�A������ $\num{0}$)

���l�ɁA
\begin{equation*}
5 = 2^3*1 + 2^2*(-1) + 2^1*0 + 2^0*1
\end{equation*}
�ł��邪�A
\begin{equation*}
\num{5} = <<<<\nnum{0}, \nnum{1}>, \nnum{-1}>, \nnum{0}>, \nnum{1}>
\end{equation*}
�ƕ\�����Ƃ͂ł��Ȃ��B($\num{1}$ �� $\num{0}$ �������Ɍ����)
\end{ex}

���̕\���Ƃ��āA��̕��@�Ƃ͕ʂɃ��X�g���g�������@���l���邱�Ƃ��ł���B
���������X�g���g���ꍇ�Anil �萔�����X�g�̏I�_�Ƃ݂Ȃ��킯�����A
�Ⴆ�� $nil \defeq F$ �Ƃ��Ă��A��ʂ̃����_���� nil �Ɠ��������ǂ�����
�������Ƃ͔��ɍ���ł��邽�߁A�����ł̓��X�g���g�������@��I�����Ȃ������B

�Ȃ��A�ȍ~�̃����_���ɂ����ẮA���͂���郉���_���Ɉ��̐������ۂ��Ă���A
���̐������ł̓��͂ɑ΂��Ă͊��҂���ϊ����s������̂Ƃ���B
�������͂��ꂽ���͂ɑ΂��ẮA�����炩�̕ϊ��͐i�ނ��̂́A���҂����ϊ���
�s����ۏ؂͂Ȃ��B���̊��҂��Ȃ����ʂ��Ԃ邱�Ƃ� \textbf{����`} �ƌ����B

�ȉ��ł͖�������Ȃ����͂ɑ΂���ϊ��͖���`�Ƃ���B
����������������͂��e�Ղɐ��������ꍇ��
�����Ă����͖͂������Ȃ����ƂƂ���B

\begin{thm}
$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�ɂ� $T$�A
�΂̏ꍇ�ɂ� $F$ ��Ԃ��悤�ȃ����_�� $Isn$ ��
���̂悤�ɒ�߂���B
\begin{equation*}
\begin{array}{l}
Isn = \lambda x . x K^3_3 K K I F T \\
 x �ɂ͔C�ӂ̃����_������́B
\end{array}
\end{equation*}
\end{thm}

\begin{proof}
���̃����_�� $M$ ���l����B
\begin{equation*}
\begin{array}{rcll}
M & = & \lambda x . x \alpha_1 \alpha_2 \alpha_3 \alpha_4 \alpha_5 \alpha_6 &
\alpha_i (1 \le i \le 6) �̓����_��
\end{array}
\end{equation*}
���̃����_�� $M$ �ɑ΂��Ď��̂悤�ɂȂ� $\alpha_i (1 \le i \le 6)$ ���߂����B
\begin{align}
M \nnum{1}  & \betaeq T & \\
M \nnum{0}  & \betaeq T & \\
M \nnum{-1} & \betaeq T & \\
M <U, V>   & \betaeq F & \text{U, V �̓����_��}
\end{align}
(1)����(4)�̍��ӂ��x�[�^�ϊ�����Ǝ��̂悤�ɂȂ�B
\begin{align}
M \nnum{1}  & \betaeq \alpha_1 \alpha_4 \alpha_5 \alpha_6 \\
M \nnum{0}  & \betaeq \alpha_2 \alpha_4 \alpha_5 \alpha_6 \\
M \nnum{-1} & \betaeq \alpha_3 \alpha_4 \alpha_5 \alpha_6 \\
M <U, V>   & \betaeq \alpha_1 U V \alpha_2 \alpha_3 \alpha_4 \alpha_5 \alpha_6
\end{align}
(8)���
\begin{align}
\alpha_1 & = K^3_3
\end{align}
�Ƃ��邱�ƂŁA$U, V$ �Ɉˑ����Ȃ��`�ɂł���B \\
�܂��A(5)�����(9)���
\begin{align}
M \nnum{1}  & \betaeq \alpha_6
\end{align}
�ł��邩��
\begin{align}
\alpha_6 & = T
\end{align}
����܂�B \\
�Ȃ�(8)��(9)�ɂ��
\begin{align}
M <U, V>   & \betaeq \alpha_2 \alpha_3 \alpha_4 \alpha_5 \alpha_6
\end{align}
�ƃx�[�^�ϊ��ł���B \\
������ $\alpha_2 = I$ �Ƃ���ƁA(12)��� $M \num{0} \betaeq \alpha_3 \alpha_4 \alpha_5 \alpha_6$ �ƂȂ邪�A
(12) ��� $M \num{-1} \betaeq M <U, V>$ �ƂȂ�s�K���B \\
������
\begin{align}
\alpha_2 & = K
\end{align}
�Ƃ���ƁA(6) (7) (12) �� (9) (11) (13) ��肻�ꂼ��
\begin{align}
M \nnum{0}  & \betaeq \alpha_4 T \\
M \nnum{-1} & \betaeq \alpha_3 \alpha_4 \alpha_5 T \\
M <U, V>   & \betaeq \alpha_3 \alpha_5 T
\end{align}
�ƂȂ�B \\
(16) ���
\begin{align}
\alpha_3 = K \\
\alpha_5 = F
\end{align}
�܂� (14) (15) ���
\begin{align}
\alpha_4 = I
\end{align}
�ƒ�߂�΂悢���Ƃ��킩��B \\
�ȏ� (9) (11) (13) (17) (18) (19) ���
\begin{equation*}
Isn = \lambda x . x K^3_3 K K I F T
\end{equation*}
�Ƃ���Α�ӂ𖞂����B
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{��{�I�ȎZ�p�̒�`}

\begin{df}
$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�� $\nnum{0}$�A
$\num{n} = <M, N>$ �̏ꍇ�� $M$ ��Ԃ��悤�ȃ����_�� $Hdr$ �����̂悤�ɒ�߂�B
\begin{equation*}
\begin{array}{rcll}
Hdr & \defeq & \lambda x . (Isn \, x) \quad \nnum{0} \quad (x K)
\end{array}
\end{equation*}
�܂��A$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�͂��̂܂܁A$\num{n} = <M, N>$ �̏ꍇ�� $N$ ��Ԃ��悤�ȃ����_�� $Ftr$ ��
���̂悤�ɒ�߂�B
\begin{equation*}
\begin{array}{rcll}
Ftr & \defeq & \lambda x . (Isn \, x) \quad x \quad (x(K I))
\end{array}
\end{equation*}
\end{df}

\begin{df}
�����_�� $\num{n}$

\begin{center}
$
\begin{array}{l}
\num{n} \equiv <\dots<<\num{x_i} , \num{x_{i-1}}>, \dots >, \num{x_j}>, \dots >, \num{x_0}>
\quad i \ge 0 \quad 0 \le j \le i \\
\num{x_k} = \num{0} \quad (j \le k \le i)
\end{array}
$
\end{center}
�ɑ΂���
\begin{center}
$
<\dots<<\num{x_{j-1}}, \num{x_{j-2}}>, \dots>, \num{x_0}>
$
\end{center}
��Ԃ������_�� $Tr$ �����̂悤�ɒ�߂�B
\begin{quote}
$Tr$ $\defeq$ $\lambda x .$ ($Isn$ ($Hdr$ $x$)) \\
\q\q\q\q\q\q (($Hdr$ $x$) $x$ ($Ftr$ $x$) $x$) \\
\q\q\q\q\q\q (($Iz$ ($Tr$ ($Hdr$ $x$))) \\
\q\q\q\q\q\q\q ($Ftr$ $x$) \\
\q\q\q\q\q\q\q ($Pair$ ($Tr$ ($Hdr$ $x$)) ($Ftr$ $x$))) \\
x �ɂ� $\num{n}$����́B
\end{quote}
�����Ń����_�� $Iz$ �́A���郉���_���� $\nnum{0}$ �̏ꍇ�� T�A
�����łȂ���� F ��Ԃ����̂ŁA���̂悤�ɒ�߂�B
\begin{quote}
$Iz \defeq \lambda x .$ ($Isn$ $x$) ($x$ $F$ $T$ $F$) $F$ \\
x �ɂ͔C�ӂ̃����_������́B
\end{quote}

\end{df}

\begin{df}
�����_�� $\num{n}$
\begin{center}
$
\begin{array}{l}
\num{n} \equiv <\dots<<\num{x_i} , \num{x_{i-1}}>, \dots >, \num{x_0}>
\quad i \ge 0 \\
\num{x_i} = \nnum{1} \quad \num{x_j} \, (0 \le j \le i) �� \nnum{1}, \nnum{0}, \nnum{-1} �̂����ꂩ
\end{array}
$
\end{center}
�ɑ΂��āA
\begin{center}
$
\begin{array}{l}
<\dots<<\num{x_k} , \num{x_{k-1}}>, \dots >, \num{k_0}>
\quad k \ge 0 \\
\num{x_k} = \nnum{1} \quad \num{x_l} \, (0 \le l \le i) �� \nnum{1}, \nnum{0} �̂����ꂩ
\end{array}
$
\end{center}
�ƕϊ����郉���_�� $Std$  �����̂悤�ɒ�߂�B
\begin{quote}
$Std$ $\defeq$ $Std^*$ $\nnum{0}$ \\
\\
$Std^*$ $\defeq$ $\lambda x y .$ ($Isn$ $y$) \\
\q\q\q\q\q\q\q (($Iz$ $x$) $y$ $\nnum{0}$) \\
\q\q\q\q\q\q\q (($Iz$ $x$) \\
\q\q\q\q\q\q\q\q (($Ftr$ $y$) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{0}$ ($Hdr$ $y$)) ($Ftr$ $y$)) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{0}$ ($Hdr$ $y$)) ($Ftr$ $y$)) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{-1}$ ($Hdr$ $y$)) $\nnum{1}$)) \\
\q\q\q\q\q\q\q\q (($Ftr$ $y$) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{0}$ ($Hdr$ $y$)) $\nnum{0}$) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{-1}$ ($Hdr$ $y$)) $\nnum{1}$) \\
\q\q\q\q\q\q\q\q\q (($Ftr$ ($Hdr$ $y$)) \\
\q\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{0}$ ($Hdr$ $y$)) $\nnum{1}$) \\
\q\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{-1}$ ($Hdr$ $y$)) $\nnum{0}$) \\
\q\q\q\q\q\q\q\q\q\q ($Pair$ ($Std^*$ $\nnum{-1}$ ($Hdr$ $y$)) $\nnum{1}$)))) \\
$x$ �� $\nnum{-1}$ ��ϊ����邽�߂̌��؂�ŁA$y$ �ɕϊ��Ώۂ̃����_�� $\num{n}$ ����́B \\
\end{quote}
\end{df}

\begin{df}
���R�� $n$ �� $m$ ���傫���Ƃ��A�����_�� $\num{n}$ �� $\num{m}$ ���傫���Ƃ����B \\
�����_�� $\num{n}$ �� $\num{0}$ ���傫���ꍇ�� $T$ �����łȂ���� $F$ ��Ԃ�
�����_�� $Gt$ �����̂悤�ɒ�߂�B

\begin{quote}
$Gt$ $\defeq$ $\lambda x .$ ($Isn$ ($Hdr$ $x$)) (($Ftr$ $x$) $T$ $F$ $F$) $T$ \\
$x$ �ɂ̓����_�� $\num{n}$ ����́B
\end{quote}

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{���Z�̒�`}

\begin{df}
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

\end{df}

�����̒�`��p���āA�����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�����ċA�I�ɒ�`����B

\begin{df}
�J��オ�肨���2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z�������ʂ�Ԃ������_�� $Add^*$ �����̂悤�ɒ�߂�B

\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$)))

$x$ �͌J��オ���\�������_�� $\nnum{1}, \nnum{0}, \nnum{-1}$ �ŁA$y, z$ ��
�����_�� $\num{n_1}, \num{n_2}$�B

\end{quote}
\end{df}

���̂悤�ɍċA�I��`�\�ł��邱�Ƃ́A���̒藝��莦�����B

\begin{thm} (�ċA�藝)

�C�ӂ̃����_�� M �ƕϐ� x �ɑ΂��� $fx =_\beta Mfx$ �ƂȂ郉���_�� f ����߂���B

\end{thm}

\begin{proof}
�ȉ��̃����_��

\begin{center}
$
Y =_\beta \lambda f.(\lambda x.f(x x))(\lambda x.f(x x))
$
\end{center}

�ɑ΂��� $f = Y M$ �Ƃ����

\begin{center}
$
\begin{array}{rcll}
YMx & \equiv & (\lambda f.(\lambda x.f(x x))(\lambda x.f(x x)))Mx \\
    & \to_\beta & (\lambda x.M(x x))(\lambda x.M(x x)))x \\
    & \to_\beta & M((\lambda x.M(x x))(\lambda x.M(x x)))x \\
M(Y M)x & \equiv & M((\lambda f.(\lambda x.f(x x))(\lambda x.f(x x)))M)x \\
        & \to_\beta & M((\lambda x.M(x x))(\lambda x.M(x x)))x
\end{array}
$
\end{center}
��� $YMx =_\beta M(Y M)x$
\end{proof}

�ȏ���A2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�����`���邱�Ƃ��ł���B

\begin{df}
2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�� $Add$ �����̂悤�ɒ�߂�B

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

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{���Z�̒�`}
���Z�͉��Z����2�̃����_���̂����A�Е��̃����_��
$
\num{n} = <\dots<<\num{x_i} , \num{x_{i-1}}>, \dots >, \num{x_0}>
\quad (i \ge 1)
$ 
�̊e $\num{x_j} \quad (1 \le j \le i)$ �𐳕��t�]���������̂Ƃ̉��Z�Ƃ��Ē�`�ł���B

\begin{df}
$\nnum{1}, \nnum{0}, \nnum{-1}$ �����ꂼ�� $\nnum{-1}, \nnum{0}, \nnum{1}$ �ɕϊ�����
�����_�� $Inv^*$ �����̂悤�ɒ�߂�B

\begin{equation*}
Inv^* \defeq \lambda x . x \, \nnum{-1} \, \nnum{0} \, \nnum{1}
\end{equation*}

\end{df}

\begin{df}
$\num{n}$ �̐������t�]�����郉���_�� $Inv$ �����̂悤�ɒ�߂�B

\begin{quote}
Inv $\defeq$ $\lambda x.$ (Isn x) \\
\q\q\q\q\q\q ($Inv^*$ x) \\
\q\q\q\q\q\q ($Pair$ ($Inv$ ($Hdr$ x)) ($Inv$ ($Ftr$ x))) \\
\end{quote}

\end{df}

\begin{df}
2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�� $Sub$ �����̂悤�ɒ�߂�B

\begin{equation*}
Sub \defeq \lambda x y . Add \, x \, (Inv \, y)
\end{equation*}

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{��Z�̒�`}

\begin{df}
2�̃����_�� $\num{n_1}, \num{n_2}$ ����Z���郉���_�� $Mul$ �����̂悤�ɒ�߂�B

\begin{quote}
$Mul$ $\defeq$ $\lambda x y .$ ($Isn$ y) \\
\q\q\q\q\q\q\q (y $x$ $\nnum{0}$ ($Inv$ x)) \\
\q\q\q\q\q\q\q ($Add$ ($Mul$ $x$ ($Ftr$ $y$)) ($Pair$ ($Mul$ $x$ ($Hdr$ $y$)) $\nnum{0}$) \\
\end{quote}

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{���Z�̒�`}

\begin{df}
�����_�� $\num{n}$

\begin{center}
$
\begin{array}{ll}
\num{n} \equiv <\dots<<\num{x_i} , \num{x_{i-1}}>, \dots >, \num{x_0}> & i \ge 0
\end{array}
$
\end{center}

�ɑ΂��āA

\begin{center}
$
<\num{x_i}, <\num{x_{i-1}}, \dots <\num{x_1}, \num{x_0}> \dots >
$
\end{center}

��Ԃ������_�� $Rev_a$ �����̂悤�ɒ�߂�B

\begin{quote}
$Rev_a$ $x$ $\defeq$ $\lambda$ x . ($Isn$ ($Hdr$ $x$)) $x$ ($Con$ ($Rev_a$ ($Hdr$ $x$)) ($Ftr$ $x$))
\end{quote}

�����Ń����_�� $Con$ �́A�����_�� $\num{x}$ �� $\nnum{1}, \nnum{0}, \nnum{-1}$ �̂����ꂩ�ł���Ƃ��A

\begin{center}
$
\begin{array}{l}
Con <\num{x_k}, <\num{x_{k-1}}, \dots <\num{x_1}, \num{x_0}> \dots > \num{x} \quad (k \ge 0) \\
\quad \betaeq <\num{x_k}, <\num{x_{k-1}}, \dots <\num{x_1}, <\num{x_0}, \num{x}> \dots >
\end{array}
$
\end{center}

�ƕϊ����郉���_���ŁA���̂悤�ɒ�߂�B

\begin{quote}
$Con$ $\defeq$ $\lambda x y .$ ($Isn$ ($Ftr$ $x$)) \\
\q\q\q\q\q\q ($Pair$ ($Hdr$ $x$) ($Pair$ ($Ftr$ $x$) $y$)) \\
\q\q\q\q\q\q ($Pair$ ($Hdr$ $x$) ($Con$ ($Ftr$ $x$) $y$)) \\
$x$ �ɂ� $\num{n}$ ����́A$y$ �ɂ� $\nnum{1}, \nnum{0}, \nnum{-1}$ �̂����ꂩ����́B
\end{quote}

�܂��t��

\begin{center}
$
<\num{x_i}, <\num{x_{i-1}}, \dots <\num{x_1}, \num{x_0}> \dots >
$
\end{center}

�ɑ΂���

\begin{center}
$
\num{n} \equiv <\dots<<\num{x_i} , \num{x_{i-1}}>, \dots >, \num{x_0}>
$
\end{center}

�ƕϊ����郉���_�� $Rev_d$ �����̂悤�ɒ�߂�B

\begin{quote}
$Rev_d$ $\defeq$ $\lambda x .$ ($Isn$ $x$) $x$ ($Pair$ ($Hdr$ $x$) ($Rev_d$ ($Ftr$ $x$))) \\
$x$ �ɂ� $Rev_a$ �ŕϊ����ꂽ�����_������́B
\end{quote}

\end{df}

\begin{df}
�����_�� $\num{n_1}, \num{n_2}$ ���珤�Ɨ]��̑΂�Ԃ��悤�ȃ����_�� $Div$ �����̂悤�ɒ�߂�B

\begin{quote}
$Div$ $\defeq$ $\lambda x y .$ $Pair$ ($Rev_d$ (($Div^*$ $\nnum{0}$ $x$ $y$) $K$)) ($Rev_d$ (($Div^*$ $\nnum{0}$ $x$ $y$) ($K I$))))  \\
$x, y$ �͂��ꂼ�ꃉ���_�� $\num{n_1}, \num{n_2}$ ����́B \\
\\
$Div^*$ $\defeq$ $\lambda x y z .$ ($Isn$ $z$) \\
\q\q\q\q\q\q\q\q (($Gt$ ($Sub$ ($Rev_d$ ($Pair$ $x$ $z$)) $y$))\\
\q\q\q\q\q\q\q\q\q ($Pair$ $\num{1}$ ($Sub$ ($Rev_d$ ($Pair$ $x$ $z$)) $y$)) \\
\q\q\q\q\q\q\q\q\q ($Pair$ $\num{0}$ ($Pair$ $x$ $z$))) \\
\q\q\q\q\q\q\q\q (($Gt$ ($Sub$ ($Rev_d$ ($Pair$ $x$ ($z$ $K$))) $y$)) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Pair$ $\num{1}$ ($A$ $K$)) ($A$ ($K$ $I$))) \\
\q\q\q\q\q\q\q\q\q ($Pair$ ($Pair$ $\num{0}$ ($B$ $K$)) ($B$ ($K$ $I$)))) \\
\\
$x, y$ �͂��ꂼ�� $Rev_a$ �ŕϊ��ς݂� $\num{n_1}, \num{n_2}$�A$z$ �ɂ͌v�Z�r���̗]�����́B \\
�o�͂͑΂ł���A�܂� $Rev_a$ �ŕϊ����ꂽ�`�ɂȂ邱�Ƃɒ��ӁB \\
\\
�Ȃ� A, B �͈ȉ��B \\
$A$ $\equiv$ ($Div^*$ ($Std$ ($Sub$ ($Rev_d$ ($Pair$ $x$ ($z$ $K$))) $y$)) $y$ ($z$ ($K$ $I$)) ) \\
$B$ $\equiv$ ($Div^*$ ($Std$ ($Rev_d$ ($Pair$ $x$ ($z$ $K$)))) $y$ ($z$ ($K$ $I$)) ) \\
\end{quote}

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�v�Z�\��}
\begin{thm}
���R����̌v�Z�\�Ȋ֐����A�C�ӂ̎��R�� $n \, (n \ge 0)$ �ɑ΂��ă����_�� $\num{n}$ ���l���邱�Ƃɂ��
��`�\�ł���B
\end{thm}

\begin{proof}
���R����̌v�Z�\�Ȋ֐����A�{�_���̖`���ŏЉ���`���[�`���ɂ���Ē�`�\�ł��邱�Ƃ͊��ɒm���Ă���B \\
�����ŁA�C�ӂ̎��R�� $n$ �ɑ΂���`���[�`�� $\overline{n}$ �ƃ����_�� $\num{n}$ �Ƃ̑��ݕϊ���^���邱�Ƃɂ����
���R����̌v�Z�\�Ȋ֐�����`�\�ł��邱�Ƃ������B
���A$\overline{n}$ ���� $\num{n}$ �ւ̕ϊ����s�������_���� $T_{12}$�A�t�� $\num{n}$ ���� $\overline{n}$ �ւ̕ϊ���
�s�������_���� $T_{21}$ �Ƃ���B \\
����� $T_{12}$ ����� $T_{21}$ �͎��̂悤�ɒ�߂���B

\begin{quote}
$T_{12}$ = $\lambda x .$ ($x$ ($T$ $F$) $T$) $\nnum{0}$ ($Add$ $\nnum{1}$ ($T_{12}$ ($Pred$ $x$)) \\
\\
$T_{21}$ = $\lambda x .$ ($Isn$ $x$) \\
\q\q\q\q\q\q ($x$ $\nnum{1}$ $\nnum{0}$ $\nnum{1}$) \\
\q\q\q\q\q\q ($+_1$ ($*_1$ ($T_{21}$ ($Hdr$ $x$)) $\overline{2}$) ($T_{21}$ ($Ftr$ $x$)))
\end{quote}

�����ŁA$+_1, *_1, Pred$ �͂��ꂼ��`���[�`���ɑ΂��鉉�Z�ŁA$+_1$ ��2�̃`���[�`���̉��Z�A
$*_1$ ��2�̃`���[�`���̏�Z�A$Pred$ �̓`���[�`�� $\overline{n}$ �ɑ΂��� $\overline{n-1}$ ��Ԃ������_���ł���B \\
�����̃����_���ɂ��`���[�`���Ƃ̑��ݕϊ����s�����ƂŁA
���R����̔C�ӂ̊֐�����`�\�ł��邱�Ƃ��������Ƃ��ł���B
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�t�^}
�`���[�`��

\begin{itemize}
\item ���̕\�� \\
���R�� $n (n \ge 0)$ �ɑ΂��ă����_�� $\overline{n}$ �� $\overline{n} \defeq \lambda f x . f^n (x)$ �ƒ�߂�B
������ $M^n (N)$ �� $\underbrace{M (M ( \dots (M}_{n��} N) \dots ))$ �̗��B

\item ���Z \\
$\overline{n}$ �ɑ΂��� $\overline{n+1}$ ��Ԃ������_�� $Succ$�A
2�̃`���[�`���̉��Z���s�������_�� $+_1$�A
2�̃`���[�`���̏�Z���s�������_�� $*_1$�A
2�̃`���[�`���̐ώZ���s�������_�� $Pow$�����ꂼ�ꎟ�̂悤�ɒ�߂�

\begin{center}
$
\begin{array}{rcl}
Succ & \defeq & \lambda y f x . f (y f x) \\
+_1  & \defeq & \lambda y z f x . y f (z f x) \\
*_1  & \defeq & \lambda y z f . y (z f) \\
Pow  & \defeq & \lambda y z . z y
\end{array}
$
\end{center}

2�̃`���[�`�� $\overline{m}, \overline{n}$ �ɑ΂��āA
$<\overline{m}, \overline{n}> \xrightarrow{f} <\overline{n}, \overline{n+1}>$
�ƕϊ����郉���_�� $f$ �����̂悤�ɒ�߂�B

\begin{center}
$
\begin{array}{rcl}
f & \defeq & \lambda p . <(\pi^2_2 \, p), (Succ \, (\pi^2_2 \, p))> \\
\pi^2_2 & \defeq & \lambda p . p (\lambda a b . b)
\end{array}
$
\end{center}

�Ȃ� $\pi^2_2$ �̓����_�� $A, B$ �ɑ΂��Ď��̂悤�ȕϊ����s�������_���ł���B

\begin{center}
$
\pi^2_2 <A, B> \betaeq B
$
\end{center}

�`���[�`�� $\overline{n}$ �ɑ΂��āAn ��0���傫���Ƃ��� $\overline{n-1}$�An��0�̂Ƃ���$\overline{0}$ ��
�Ԃ������_�� $Pred$ ����� $f$ ��p���Ď��̂悤�ɒ�߂�B

\begin{center}
$
Pred \defeq \lambda n . (\pi^2_1 (n f <\overline{0}, \overline{0}>))
$
\end{center}

�Ȃ� $\pi^2_2$ �̓����_�� $A, B$ �ɑ΂��Ď��̂悤�ȕϊ����s�������_���ł���B

\begin{center}
$
\pi^2_2 <A, B> \betaeq B
$
\end{center}

\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{������}

����A�ȏ�̒�`�����؂��邽�߂�Lamal\footnote{�ÐX�Y�� ��} ���g�p�����B������Lamal�ł͎��̂悤��
�����_���ɑ΂���ϊ��̏o�͂������Ƃ�������\footnote{��ҞH���A�d�l�Ƃ̂��ƁB} �𔭌������B

\begin{align}
& THIS \, IS \, NLAMGAR2 \, ************************* \\
& SIZE \, OF \, node \, = \, 16 \, *** \, PLEASE \, WAIT \, A \, MOMENT. \\
& FreeNodes \, = \, 6006 \\
& K \, = \, lambda \, x \, y \, x; \\
& K \, = \, lambda \, x \, y \, x; \\
& A \, = \, lambda \, x (x \, K \, K); \\
& A \, = \, lambda \, x (x \, K \, K); \\
& A \, K; \\
& A \, K; \\
& A \, K \\
& ( \, lambda \, x \, \, ( \, x \, ( \, co880 \, : \, lambda \, x \, y \, x \, ) \, co880 \, ) \, ) \, co880 \\
& sub \, ( \, co880 \, : \, lambda \, x \, y \, x \, ) \, ( \, cons \, x \, co880 \, 0 \, ) \\
& newnodes \, = \, 10
\end{align}

(23) (25) (27) �����͂ŁA����ȊO��Lamal�ɂ��o�͂ł���B

�����Ŋ��҂���o�͂� $K$ ���Ȃ킿 $lambda$ $x$ $y$ $x$ �ł��邪�A���̂Ƃ���o�͂�����Ă��܂��Ă���B
�����lamal���x�[�^�ϊ����s��Ȃ����ƂɋN�����邱�Ƃ����Ƃ߂����A
���ǂ�����ł��������߁A�{�_���ł�Lamal�ɂ��R�[�h���ȗ������B
������Lamal�ɂ�錟�؃R�[�h�͈ȉ��̃y�[�W�Ō��J����\��ł���B \\
\\
http://www.math.s.chiba-u.ac.jp/$\tilde{\,\,\,}$03um0302/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage

\section{�ӎ�}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{9}
\item J.R.Hindley and J.P.Seldin: Introduction to combinators and lambda-calculus \\
      (Cambridge University Press, 1986)
\item ��t��w ���w�� 2000�N�x��� �v�Z���_ �z�z����
\item Mayer Goldberg: One-Point Bases For $\lambda$-Calculi With Constants \\
      http://www.cs.bgu.ac.il/$\tilde{\,\,\,}$gmayer/talks/files/one-point-bases.pdf
\end{thebibliography}

\end{document}
