\documentclass[11pt, a4j, titlepage]{jsarticle}
\usepackage{proof}
\usepackage{amsthm,amssymb, amsthm, amsbsy ,amscd}
\usepackage{latexsym}
\setcounter{tocdepth}{2}

%\def\and{\wedge}
%\def\or{\vee}

\def\ra{\rightarrow}
\def\Ra{\Rightarrow}
\def\order{\mathit{Order}}
\renewcommand{\to}{\supset}

\def\derivable{�h���K��}
\newtheorem{definition}{��`}[section]
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{corhollary}[definition]{�n}
\newtheorem{prhoposition}[definition]{����}
\newtheorem{example}[definition]{��}
\newtheorem{remark}[definition]{����}
\newtheorem{conjecture}[definition]{�\�z}
\newtheorem{prhoblem}[definition]{���}
\newcommand{\rhomannumeral}[1]{\uppercase\expandafter{\rhomannumeral#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 �ÓT�_���̏ؖ��}�̃��_�N�V�����ɂ��Ă� \\ �㐳�K���藝�ƍ�����}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����16�N2��27��}
\end{center}

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

\vspace*{5mm}
\begin{center}
{\Large\gt �����@�L}
\end{center}

\setcounter{page}{0}


% �T�v
\begin{abstract}
 1930�N��� Alonzo Church �ɂ����ꂽ $\lambda$-calculus �͒��ώ�`�_����
�ؖ��}�Ƃ݂Ȃ����Ƃ��ł���B�����悤�Ȋ֌W���ÓT�_���ɂ܂Ŋg���������̂�
1992�N�� Michel Parigot �����\���� $\lambda\mu$-calculus (\cite{Parigot}) ������B�܂��A
�ÐX �Y��ɂ��2002�N�ɔ��\���ꂽ $\lambda\rho$-calculus (\cite{Komori2002})���ÓT�_���̑̌n
�ł���B�ÐX�̑̌n�� Parigot �̂�������ȒP�ȑ̌n�ɂȂ��Ă���B

 $\lambda\rho$-calculus �́A�ʏ�� $\lambda$-calculus �ŗp������ $\lambda$-variable
�Ƃ��̕ό` $\beta$-reduction �̑��ɁA$\rho$-variable �ƁA���̕ό` a-reduction�A
$\rho$-reduction ��V���ɉ�����Ă���B

 �ÐX--�� �̘_�� (\cite{Komori2003}) �ň����Ă���̌n�͋����K���藝�̏ؖ��͂ł������A
���ڂɂ͎㐳�K���藝�̏ؖ������邱�Ƃ��ł��Ȃ������B���̂��ߌÐX�͎㐳�K���藝�̏ؖ�
���ł���悤�ɕό`�K��������ɉ������̌n��������B�{�_���ł́A���̑̌n�ɂ��Ă̎㐳�K
���藝���ؖ�����B�܂��A���̑̌n�̍������ɂ��Ă��c�_����B
\end{abstract}

% �ڎ�
\tableofcontents
\newpage

% ��1��
\section{The type free $\lambda\rho$-calculus}

\begin{definition} ( $\lambda\rho$-term (\cite{Komori2002}) )
	�Z������ $\lambda$-variable�A$\rho$-variable ���^�����Ă���B
	$\lambda$-variable�A$\rho$-variable ���܂Ƃ߂����̂� term-variable �ƌĂԁB
	$\lambda\rho$-term �͈ȉ��̗l�ɍċA�I�ɒ�߂�B

	\begin{enumerate}
		\item term-variable �� $\lambda\rho$-term�B
		\item $M$�A$N$ �� $\lambda\rho$-term �Ȃ�� $(MN)$ �� $\lambda\rho$-term�B
		\item $M$ �� $\lambda$-term�A$f$ �� term-variable �Ȃ��
			$(\lambda f.M)$ �� $\lambda\rho$-term�B
	\end{enumerate}
\end{definition}

$\lambda$-variable �� $x, y, z, \dots$ �ŕ\����A�Y���t���̂��̂����l�ł���B
$\rho$-variavle �� $a, b, c, \dots$ �ŕ\����A�Y���t���̂��̂����l�ł���B
term-variable �� $f, g, h, \dots$ �ŕ\����A�Y���t���̂��̂����l�ł���B

$\lambda a.M$ �� $\rho a.M$ �ƕ\�L����ꍇ������B�{���ł́A$\lambda x.M$ �� $\rho a.M$ ��
���m�ɋ�ʂ���K�v���L��ׂɕ����ĕ\�L����B

\begin{definition} ( $\rho\beta$-reduction )
	$\rho\beta$-redex �͈ȉ��ŗ^�����鍶�ӂ̌`������ $\lambda\rho$-term �ŁA
	���� contractum �͑Ή�����E�ӂ̌`������ $\lambda\rho$-term �ł���B
	\[
	\begin{array}{rcl}
		(aM)N & \rhd_{1\rho\beta}  & (aM) \\
		(\lambda x.M)N & \rhd_{1\rho\beta} & [N/x]M \\
		(\rho a.M)N & \rhd_{1\rho\beta} & \rho a.(\lambda x.[\lambda y.a(yx)/a](Mx))N \\
		N(\rho a.M) & \rhd_{1\rho\beta} & \rho a.(\lambda x.[\lambda y.a(xy)/a](xM))N \\
		\lambda x.(\rho a.M) & \rhd_{1\rho\beta} &
			\rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a]M) \\
		\rho a.(\rho b.M) & \rhd_{1\rho\beta} & \rho a.[a/b]M
	\end{array}
	\]
\end{definition}
���ӂ� $\lambda\rho$-term : $P$ ���E�ӂ� $\lambda\rho$-term : $Q$ �ɒu�������鎖���A
$P$ ���� $Q$ �ւ� $\rho\beta$-contruction �ƌĂсA
\[ P \rhd_{1\rho\beta} Q \]
�ŕ\���B$P$ ���� $Q$ �։��񂩂� $\rho\beta$-contruction ���s�������A
$P$ ���� $Q$ �ւ� $\rho\beta$-reduction �ƌĂ�
\[ P \rhd_{\rho\beta} Q \]
�ŕ\���B�u$\rhd$�v�̓Y���͕������疾�炩�ȏꍇ�ȗ������

���� contruction ����ʂ���ׂɁA1�Ԗڂ� $a$-contruction�A2�Ԗڂ� $\beta$-contruction�A
3�Ԗڈȍ~�� $\rho$-contruction �ƌĂԁB$\rho$-reduction �͏�Ɠ��l��
$\rho$-contruction �����`����A$a\beta$-reduction �� $a$-contruction�A$\beta$-contruction
�����`�����B

 �ÐX (\cite{Komori2002}) �ň����Ă��� $\rho\beta$-contruction �́A
1�ԖځA2�ԖځA3�Ԗڂ�3�݂̂ł���B4�Ԗڈȍ~�ɂ��ẮA�{�_���Ŏ㐳�K�����ؖ�����ׂ�
�ÐX�����������̂ł���B

\newpage

% ��2��
\section{Assigning types to $\lambda\rho$-term}

\begin{definition} ( Types \cite{Hindley1} )
	�����Z�� type-variable ���^�����Ă���Ƃ���BTypes �͈ȉ��̗l�ɍċA�I�ɒ�߂�B
	\begin{enumerate}
		\item type-variable �� type �ł���B
		\item $\sigma$�A$\tau$ �� type �Ȃ�� $(\sigma \ra \tau)$ �� type �ł���B
	\end{enumerate}
\end{definition}

type �� $\lambda$�A$\rho$ ���������������̃M���V�������ŕ\���B
�֌W���������ʂ͂悭�ȗ������B���̏ꍇ�A�ȉ��̗l�ɉE������₤�B
\[
	\sigma \ra \tau \ra \upsilon \ \equiv \ (\sigma \ra (\tau \ra \upsilon))
\]

\begin{definition} ( Type assignment \cite{Hindley1} )
	$\lambda\rho$-term : $M$ �� type : $\tau$ �����蓖�Ă�\���͈ȉ��̗l�ɕ\���B
\[
	M : \tau
\]
\end{definition}

\begin{definition} ( The system $\textmc{TA}_{\lambda\rho}$ \cite{Komori2002} )
	$\lambda\rho$-term �� type �����蓖�Ă�ׂ̑̌n�� $\textmc{TA}_{\lambda}$ �̊g��ŁA
	$\textmc{TA}_{\lambda\rho}$ �ƌĂ΂��B$\textmc{TA}_{\lambda\rho}$ �̐��_�K���͈ȉ�
	�̒ʂ�ł���B
	\[
	\begin{array}{cccc}
		\infer[\textmc{($\ra$-E)} ]{ MN : \beta }{M : \alpha \ra \beta & N : \alpha}
		&
		\infer[\textmc{($\ra$-I)} ]{ \lambda x.M : \alpha \ra \beta}{
			\deduce[\vdots]{M : \beta}{ [x : \alpha ] }
		}
		&
		\infer[\textmc{(Absurd)}]{ aM : \beta}{ M : \alpha}
		&
		\infer[\textmc{(Rati)}]{ \rho a. M : \alpha}{
			\deduce[\vdots]{ M : \alpha }{
				\infer{ aQ : \beta }{ Q : \alpha }
			}
		}
		\end{array}
	\]	
\end{definition}

���̗l�� type �����蓖�Ă�ꂽ $\lambda\rho$-term ���A�^�t���\�� $\lambda\rho$-term �ƌĂԁB

\begin{example} ( Peirce's Law )
	�p�[�X�̘_���� 
	\[ ((\alpha \ra \beta) \ra \alpha) \ra \alpha \]
	�͌ÓT�_���ŏؖ��ł��邪�A���ώ�`�_���ł͏ؖ��ł��Ȃ��L���Ȏ��ł���B
	���̘_�����̏ؖ��}�͈ȉ��̒ʂ�ł���B
	\[
	\infer{\lambda y. \rho a. y(\lambda x.ax) : ((\alpha \ra \beta) \ra \alpha) \ra \alpha}{
		\infer{\rho a.y(\lambda x.ax) : \alpha}{
			\infer{y(\lambda x.ax) : \alpha}{
				y : (\alpha \ra \beta) \ra \alpha
				&
				\infer{\lambda x.ax : \alpha \ra \beta}{
					\infer{ax : \beta}{x : \alpha}
				}
			}
		}
	}
	\]
\end{example}

�p�[�X�̘_������ $\lambda\rho$-term �� contruction ����ƁA
\[
	\lambda y. \rho a. y(\lambda x.ax) \rhd_{1\rho\beta} \rho a. \lambda y.y(\lambda x.a(\lambda z.x)) 
\]
��������B���� $\lambda\rho$-term �� type �����蓖�Ă�ؖ��}�͈ȉ��̗l�ɂȂ�B
\[
	\infer{\rho a. \lambda y.y(\lambda x.a(\lambda z.x)) : ((\alpha \ra \beta) \ra \alpha) \ra \alpha}{
		\infer{\lambda y.y(\lambda x.a(\lambda z.x)) : ((\alpha \ra \beta) \ra \alpha) \ra \alpha}{
			\infer{y(\lambda x.a(\lambda z.x)) : \alpha}{
				y : (\alpha \ra \beta) \ra \alpha
				&
				\infer{\lambda x.a(\lambda z.x) : \alpha \ra \beta}{
					\infer{a(\lambda z.x) : \beta}{
						\infer{\lambda z.x : ((\alpha \ra \beta) \ra \alpha) \ra \alpha}{x : \alpha}
					}
				}
			}
		}
	}
\]

\begin{example} ( $\lambda\mu$-term, reduction and Typed $\lambda\mu$-calculus (\cite{Parigot}) ) \\

	( $\lambda\mu$-term ) $\lambda\mu$-term �� named term �� unnamed term ���琬�藧���Ă���A
	�ȉ��̗l�ɍċA�I�ɒ�߂�B
	\begin{enumerate}
		\item $\lambda$-variable �� unnamed term�B
		\item $x$ �� $\lambda$-variable�A$M$ �� unnamed term �Ȃ��
			$\lambda x.M$ �� unnamed term�B
		\item $M$�A$N$ �� unnamed term �Ȃ�� $(MN)$ �� unnamed term�B
		\item $A$ �� named term�A$a$ �� $\mu$-variable �Ȃ�� $\mu a.A$ �� unnamed term�B
		\item $M$ �� unnamed term�A$a$ �� $\mu$-variable �Ȃ��
			$[a]M$ �� named term�B
	\end{enumerate}

	( $\lambda\mu$-reduction )
	\[
	\begin{array}{rcl}
		(\lambda x.M)N & \rhd_{1\lambda\mu} & [N/x]M \\
		(\mu a.M)N & \rhd_{1\lambda\mu} & \mu a.[ [a](xy)/[a]x ]M \\
		 \,[a]\mu b.M & \rhd_{1\lambda\mu} & [a/b]M
		\end{array}
	\]

	( Typed $\lambda\mu$-calculus )
	\[
	\begin{array}{cccc}
		\infer{MN : \beta}{M : \alpha \ra \beta & N : \alpha} \ 
		&
		\infer{ \lambda x.M : \alpha \ra \beta}{
				\deduce[\vdots]{M : \beta}{ [x : \alpha ] }
		} \ 
		&
		\infer{ [a]M : \alpha^a}{ M : \alpha} \ 
		&
		\infer{ \mu a. M : \alpha}{A : \alpha^a}
	\end{array}
	\]

	( Peirce's Law for typed $\lambda\mu$-calculus )
	\[
	\infer{\lambda y.\mu a.[a](y(\lambda x.\mu b.[a]x)) : ((\alpha \ra \beta) \ra \alpha) \alpha}{
		\infer{\mu a.[a](y(\lambda x.\mu b.[a]x)) : \alpha}{
			\infer{ [a](y(\lambda x.\mu b.[a]x)) : \alpha^a}{
				\infer{y(\lambda x.\mu b.[a]x) : \alpha}{
					y : (\alpha \ra \beta)\ra \alpha
					&
					\infer{\lambda x.\mu b.[a]x : \alpha \ra \beta}{
						\infer{\mu b.[a]x : \beta}{
							\infer{ [a]x : \alpha^a}{
								x : \alpha
							}
						}
					}
				}
			}
		}
	}
	\]



\end{example}

\newpage

% ��3��
\section{$\lambda\rho$-calculus �̎㐳�K���藝}

\begin{theorem} \label{th4} (weak reduction for $\lambda\rho$-term)
	�C�ӂ� type �t���\�� $\lambda\rho$-term �� $\rho\beta$-reduction ���s�����ɂ��
	���K�`�ɂ��鎖���o����B
\end{theorem}

���̒藝���ؖ�����ɂ́A�i�K�I�ɂ������̕⏕�藝���ؖ�����K�v������B
�ؖ��̕��j�͂��Ȃ�ׂ��ȓ_�܂ŌÐX�ɂ���ė^����ꂽ���A���ۂ̌v�Z���͍������s�����B

\begin{lemma} \label{lem4-1}
	�C�ӂ� $\lambda\rho$-term �� $\rho a.M$ �������� $M$ �̌`�� $\rho$-reduction �ł���B
	�A���A$M$ �ɂ� $\rho$ ����،���Ȃ��B
\end{lemma}

�ؖ�����ɓ�����A�ȉ��� $\order$ �֐����`����B
\begin{definition} ( $\order$ )
	$\lambda\rho$-term �S�̂��玩�R���ւ̊֐��A$\order$ �͍ċA�I�Ɉȉ��̗l�ɒ�`�����B
	\begin{itemize}
		\item $\order(f) = 0$
		\item $\order(\lambda x.M) = 2 \cdot \order(M)$
		\item $\order(\rho a.M) = \order(M) + 1$
		\item $\order(MN) = 2 \cdot (\order(M) + \order(N))$
	\end{itemize}
\end{definition}
$\order$ �̒�`�́A�������^�����������������g���Ă�����`����ɁA�ÐX�����R����
�\���Ȃ��ƂɋC�t�������ς������̂ł���B


\begin{theorem}
	�C�ӂ� $\lambda\rho$-term : $M$ �̒��� $\rho$ ������Ȃ��Ȃ�΁A$\order(M) = 0$ �ł���B
\end{theorem}
{\bf ���� :}\ \ \ \ $M$ �̍\���Ɋւ���A�[�@����e�Ղɏؖ��ł���B

\begin{lemma} \label{lem4-2}
	$\lambda\rho$-term $X$ �̕����� $M$ �̈�� $M'$ �Œu�������āA
	$X$���瓾���� $\lambda\rho$-term �� $X'$ �Ƃ���B
	���̂Ƃ��A
	\[
		\order(M) > \order(M') \Ra \order(X) > \order(X')
	\]
\end{lemma}

{\bf �ؖ� :}\ \ \ \ $X$ �̍\���Ɋւ���A�[�@�ŏؖ�����B
\begin{itemize}
	\item $X=M$ �̏ꍇ�͎����ł���B
	\item $X = \lambda x.N$ �̏ꍇ�A$\order(X) = 2 \cdot \order(N)$�A
		$\order(X') = 2 \cdot \order(N')$�B�A�[�@�̉����� $\order(N) > \order(N')$�B
		�̂ɑ召�֌W�͈ێ�����Ă���B
	\item $X = \rho a.N$ �̏ꍇ�A$\order(X) = \order(N) +1$�A$\order(X') = \order(N') +1$�B
		�A�[�@�̉�����A���̏ꍇ���召�֌W�͈ێ�����Ă���B
	\item $X = N_1 N_2$ �̏ꍇ�A$\order(X) = 2 \cdot (\order(N_1) + \order(N_2))$�A
		$\order(X') = 2 \cdot (\order(N_1') + \order(N_2'))$�B
		���������ۂɂ� $N_1$�A$N_2$ �̂ǂ��炩��������u���������Ă��Ȃ��B
		�A�[�@�̉�����A���̏ꍇ�ł��召�֌W�͈ێ�����Ă���B
		$\square$
\end{itemize} 

���� $\order$ ��p����ƁA�⏕�藝\ref{lem4-1} �͎��̗l�ɏ��������鎖���o����B

\begin{lemma} \label{lem4-3}
	�C�ӂ� $\lambda\rho$-term : $X$ �́A���� $\order$ �� 0 �� 1 �ɂȂ�܂� $\rho$-reduction 
���鎖���o����B
\end{lemma}

{\bf �ؖ� :}\ \ \ \ $X$ �̍\���Ɋւ���A�[�@�ŏؖ�����B$X$ �� contruction �������̂� $X'$ �Ƃ���B
\begin{itemize}
	\item $(\rho a.M)N \rhd_{1\rho\beta} \rho a.(\lambda x.[\lambda y.a(yx)/a](Mx))N$
		\[
		\begin{array}{lcl}
			\order(X) & = & \order((\rho a.M)N) \\
			& = & 2 \cdot (\order(\rho a.M) + \order(N)) \\
			& = & 2 \cdot (\order(M) + 1 + \order(N)) \\
			\\
			\order(X') & = & \order(\rho a.(\lambda x.[\lambda y.a(yx)/a](Mx))N) \\
			& = & \order(\rho a.(\lambda x.(Mx))N) \ \ \ \ \textmc{(�⏕�藝$\ref{lem4-2}$���)} \\
			& = & \order((\lambda x.(Mx))N) +1 \\
			& = & 2 \cdot (\order(\lambda x.(Mx)) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot \order(Mx) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot 2 \cdot (\order(M) + \order(x)) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot 2 \cdot \order(M) + \order(N)) +1
		\end{array}
		\]
		�����ŋA�[�@�̉����K�p�� $M$ �̌`�ɒ��ڂ���B
		$\order(M) = 0$ �̏ꍇ�́A���̂܂ܑ�����Ă��΂悢�B
		$\order(M) = 1$ �̏ꍇ�� $M$ �� $\rho b.M'$ �̌`�����Ă���B���̎� $M'$ �� $\rho$ ��
		����Ȃ����ɒ��ӂ���B��� $\rho a.(\rho b. M')$ �� contruct ��(���̍ۂ� $\order$ ������
		�Ȃ����͌�ɏؖ������)�A�o�Ă��� $\rho a.[a/b]M'$ ��V���� $M$ �Ƃ��Ă��Ə�̏ꍇ�Ɠ��l
		�ɂ��Ċm�F�ł���B
		�]���āAreduction ������� $\order$ �͌������Ă���B\\

	\item $N(\rho a.M) \rhd_{1\rho\beta} \rho a.(\lambda x.[\lambda y.a(xy)/a](xM))N$
		\[
		\begin{array}{lcl}
			\order(X) & = & \order(N(\rho a.M) \\
			& = & 2 \cdot (\order(N) + \order(\rho a.M)) \\
			& = & 2 \cdot (\order(N) + \order(M) +1) \\
			\\
			\order(X') & = & \order(\rho a.(\lambda x.[\lambda y.a(xy)/a](xM))N) \\
			& = & \order(\rho a.(\lambda x.(xM))N \ \ \ \ \textmc{(�⏕�藝$\ref{lem4-2}$���)} \\
			& = & \order((\lambda x.(xM))N) +1 \\
			& = & 2 \cdot (\order(\lambda x.(xM)) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot \order(xM) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot 2 \cdot (\order(x) + \order(M)) + \order(N)) +1 \\
			& = & 2 \cdot (2 \cdot 2 \cdot \order(M) + \order(N)) +1
		\end{array}
		\]
		��Ɠ��l�ȋc�_����Areduction ������� $\order$ �͌������Ă���B\\

	\item $\lambda x.(\rho a.M) \rhd_{1\rho\beta} \rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a]M)$
		\[
		\begin{array}{lcl}
			\order(X) & = & \order(\lambda x.(\rho a.M)) \\
			& = & 2 \cdot \order(\rho a.M) \\
			& = & 2 \cdot (\order(M) +1) \\
			\\
			\order(X') & = & \order(\rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a]M)) \\
			& = & \order(\rho a.(\lambda x.M) \ \ \ \ \textmc{(�⏕�藝$\ref{lem4-2}$���)} \\
			& = & \order(\lambda x.M) +1 \\
			& = & 2 \cdot \order(M) +1 \\
		\end{array}
		\]
		reduction ������� $\order$ �͌������Ă���B\\
	
	\item $\rho a.(\rho b.M) \rhd_{1\rho\beta} \rho a.[a/b]M$
		\[
		\begin{array}{lcl}
			\order(X) & = & \order(\rho a.(\rho b.M)) \\
			& = & \order(\rho b.M) +1\\
			& = & \order(M) +2 \\
			\\
			\order(X') & = & \order(\rho a.[a/b]M) \\
			& = & \order(\rho a.M) +1\ \ \ \ \textmc{(�⏕�藝$\ref{lem4-2}$���)} \\
			& = & \order(M) +1
		\end{array}
		\]
		reduction ������� $\order$ �͌������Ă���B
	$\square$\\
\end{itemize}

\begin{lemma} \label{lem4-4}
	�^�t���\�� $\lambda\rho$-term : $M$ ���^����ꂽ���A��� $\rho\beta$-contruction
	���� $N$ ������ type ������ $\lambda\rho$-term �ł���B
\end{lemma}
{\bf �ؖ� :}\ \ \ \ $M$ �̐��_�}�̍\���Ɋւ���A�[�@�ŏؖ�����B
\begin{enumerate}
	\item $(aM)N \rhd_{1\rho\beta} (aM)$
		\[
		\begin{array}{ccc}
			\infer{(aM)N : \alpha}{
				\infer{aM : \beta \ra \alpha}{M : \gamma}
				&
				N : \beta
			}
			& \rhd &
			\infer{aM : \alpha}{M : \gamma}
		\end{array}
		\]\\

	\item $(\lambda x.M)N \rhd_{1\rho\beta} [N/x]M$
		\[
		\begin{array}{ccc}
			\infer{(\lambda x.M)N : \alpha}{
				\infer{(\lambda x.M) : \beta \ra \alpha}{
					\deduce[\vdots]{M : \alpha}{ [x : \beta] }
				}
				&
				N : \beta
			}
			& \rhd &
			[N/x]M : \alpha
		\end{array}
		\]\\

	\item $(\rho a.M)N \rhd_{1\rho\beta} \rho a.(\lambda x.[\lambda y.a(yx)/a](Mx))N$
		\[
		\begin{array}{ccc}
			\infer{(\rho a.M)N : \alpha}{
				\infer{\rho a.M : \beta \ra \alpha}{M : \beta \ra \alpha}
				&
				N : \beta
			}
			& \rhd &
			\infer{\rho a.(\lambda x.[\lambda y.a(yx)/a](Mx))N : \alpha}{
				\infer{(\lambda x.[\lambda y.a(yx)/a](Mx))N : \alpha}{
					\infer{\lambda x.[\lambda y.a(yx)/a](Mx) : \beta \ra \alpha}{
						\infer{ [\lambda y.a(yx)/a](Mx) : \alpha}{
							[\lambda y.a(yx)/a]M : \beta \ra \alpha
							&
							x : \beta
						}
					}
					&
					N : \beta				}
			}
		\end{array}
		\]
		$\vdash_{\rho\lambda} M : \alpha \Ra 
		\vdash_{\rho\lambda} [\lambda y.a(yx)/a]M : \alpha$ �ł��鎖��
		$M$ �̍\���Ɋւ���A�[�@�ŏؖ�����B
		\begin{itemize}
			\item $M \equiv x$ \\
				$[a/b]x \equiv x$ �ł��鎖���玩���B\\
			\item $M \equiv M_1 M_2$ \\
				�A�[�@�̉����� $\vdash [\lambda y.a(yx)/a]M_1 : \beta \ra \alpha \ ,
				\  [\lambda y.a(yx)/a]M_2 : \beta$ �B�]����
				\[
				\infer{ [\lambda y.a(yx)/a]M_1 M_2 : \alpha}{
					[\lambda y.a(yx)/a]M_1 : \beta \ra \alpha & [\lambda y.a(yx)/a]M_2 : \beta
				}
				\]
				�̂� $\vdash [\lambda y.a(yx)/a]M : \alpha$ �B\\
			\item $M \equiv \lambda x.M'$ \\
				$M$ �� type �� $\alpha \equiv (\beta \ra \gamma)$ �Ƃ���B
				�A�[�@�̉����� $\vdash [\lambda y.a(yx)/a]M' : \gamma$ �B�]����
				\[
				\infer{\lambda x.[\lambda y.a(yx)/a]M' : \beta \ra \gamma}{ [\lambda y.a(yx)/a]M' : \gamma}
				\]
				�܂��A$\lambda x.[\lambda y.a(yx)/a]M' = [\lambda y.a(yx)/a](\lambda x.M') = M$ �ƂȂ�̂ŁA\\
				$\vdash [\lambda y.a(yx)/a]M : \beta \ra \gamma \ \ (\equiv \alpha)$ �B\\
			\item $M \equiv cM'$ \\
				$c$ �ɂ��Ă̏ꍇ�����B
				\begin{itemize}
					\item $a = c$ \\
						���X�̎����ȉ��̗l�ɂȂ�B
						\[
						\begin{array}{ccc}
							\infer{(\rho a.aM')N : \alpha}{
								\infer{\rho a.aM' : \beta \ra \alpha}{
									\infer{aM' : \beta \ra \alpha}{M' : \beta \ra \alpha}
								}
								&
								N : \beta
							}
							& \rhd &
							\infer{\rho a.(\lambda x.[\lambda y.a(yx)/a]((aM')x))N : \alpha}{
								\infer{(\lambda x.[\lambda y.a(yx)/a]((aM')x))N : \alpha}{
									\infer{\lambda x.[\lambda y.a(yx)/a]((aM')x) : \beta \ra \alpha}{
										\infer{ [\lambda y.a(yx)/a]((aM')x) : \alpha}{
											[\lambda y.a(yx)/a](aM') : \beta \ra \alpha
											&
											x : \beta
										}
									}
									&
									N : \beta
								}
							}
						\end{array}
						\]
						�A�[�@�̉����� $\vdash [\lambda y.a(yx)/a]M' : \alpha$ �B\\
						$[\lambda y.a(yx)/a](aM')$ ����
						$(\lambda y.a(yx))[\lambda y.a(yx)/a]M'$ �̐��_�}�͈ȉ��̒ʂ�B
						\[
						\infer{(\lambda y.a(yx))[\lambda y.a(yx)/a]M' : \beta \ra \alpha}{
							\infer{\lambda y.a(yx) : \alpha \ra \beta \ra \alpha}{
								\infer{a(yx) : \beta \ra \alpha}{
									\infer{yx : \alpha}{y : \beta \ra \alpha & x : \beta}
								}
							}
							&
							[\lambda y.a(yx)/a]M' : \alpha
						}
						\]
					�]���āA$\vdash [\lambda y.a(yx)/a](aM') : \beta \ra \alpha$ �B\\
				\item $a \neq c$ \\
					�A�[�@�̉����� $\vdash [\lambda y.a(yx)/a]M' : \beta$ �B\\
					$c[\lambda y.a(yx)/a]M' \equiv [\lambda y.a(yx)/a]cM' \equiv [\lambda y.a(yx)/a]M$
					�ƂȂ�̂ŁA\\
					$\vdash [\lambda y.a(yx)/a]M : \alpha$ ���ؖ��ł���B\\
				\end{itemize}
		\end{itemize}

	\item $N(\rho a.M) \rhd_{1\rho\beta} \rho a.(\lambda x.[\lambda y.a(xy)/a](Mx))N$
		\[
		\begin{array}{ccc}
			\infer{N(\rho a.M) : \alpha}{
				N : \beta \ra \alpha
				&
				\infer{\rho a.M : \beta}{M : \beta}
			}
			& \rhd &
			\infer{\rho a.(\lambda x.[\lambda y.a(xy)/a](xM))N : \alpha}{
				\infer{(\lambda x.[\lambda y.a(xy)/a](xM))N : \alpha}{
					\infer{\lambda x.[\lambda y.a(xy)/a](xM) : (\beta \ra \alpha) \ra \alpha}{
						\infer{ [\lambda y.a(xy)/a](xM) : \alpha}{
							x : \beta \ra \alpha
							&
							[\lambda y.a(xy)/a]M : \beta
						}
					}
					&
					N : \beta \ra \alpha
				}
			}

		\end{array}
		\]
		$\vdash_{\rho\lambda} M : \alpha \Ra 
		\vdash_{\rho\lambda} [\lambda y.a(xy)/a]M : \alpha$ �ł��鎖��
		$M$ �̍\���Ɋւ���A�[�@�ŏؖ�����B�w�ǂ���̏ꍇ�Ɠ��l�ɏo����̂�
		�Ⴄ�_�݂̂������B
		\begin{itemize}
			\item $M = cM'$ \\
				$c$ �ɂ��Ă̏ꍇ�����B
				\begin{itemize}
					\item $a = c$ \\
						���X�̎����ȉ��̗l�ɂȂ�B
						\[
						\begin{array}{ccc}
							\infer{N(\rho a.aM') : \alpha}{
								N : \beta \ra \alpha
								&
								\infer{\rho a.aM' \ : \beta}{
									\infer{aM' : \beta}{M' : \beta}
								}
							}
							& \rhd &
							\infer{\rho a.(\lambda x.[\lambda y.a(xy)/a](x(aM')))N : \alpha}{
								\infer{(\lambda x.[\lambda y.a(xy)/a](x(aM')))N : \alpha}{
									\infer{\lambda x.[\lambda y.a(xy)/a](x(aM')) : (\beta \ra \alpha) \ra \alpha}{
										\infer{ [\lambda y.a(xy)/a](x(aM')) : \alpha}{
											x : \beta \ra \alpha
											&
											[\lambda y.a(xy)/a](aM') : \beta
										}
									}
									&
									N : \beta \ra \alpha
								}
							}
						\end{array}
						\]
						�A�[�@�̉����� $\vdash [\lambda y.a(xy)/a]M' : \beta$ �B\\
						$[\lambda y.a(xy)/a](aM')$ ����
						$(\lambda y.a(xy))[\lambda y.a(xy)/a]M'$ �̐��_�}�͈ȉ��̒ʂ�B
						\[
						\infer{(\lambda y.a(xy))[\lambda y.a(xy)/a]M' : \beta}{
							\infer{\lambda y.a(xy) : \beta \ra \beta}{
								\infer{a(xy) : \beta}{
									\infer{xy : \alpha}{
										x : \beta \ra \alpha
										&
										y : \beta
									}
								}
							}
							&
							[\lambda y.a(xy)/a]M' : \beta
						}
						\]

					\item $a \neq c$ \\
					��̏ꍇ�Ɠ��l�B\\
				\end{itemize}
		\end{itemize}

	\item $\lambda x.(\rho a.M) \rhd_{1\rho\beta}
		\rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a]M)$
		\[
		\begin{array}{ccc}
			\infer{	\lambda x.(\rho a.M) : \beta \ra \alpha}{
				\infer{\rho a.M) : \alpha}{M : \alpha}
			}
			& \rhd &
			\infer{\rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a]M) : \beta \ra \alpha}{
				\infer{\lambda x.[\lambda y.a(\lambda z.y)/a]M : \beta \ra \alpha}{
					[\lambda y.a(\lambda z.y)/a]M : \alpha
				}
			}
		\end{array}
		\]
		$\vdash_{\rho\lambda} M : \alpha \Ra 
		\vdash_{\rho\lambda} [\lambda y.a(\lambda z.y)/a]M : \alpha$ �ł��鎖��
		$M$ �̍\���Ɋւ���A�[�@�ŏؖ�����B�w�ǂ���̏ꍇ�Ɠ��l�ɏo����̂�
		�Ⴄ�_�݂̂������B
		\begin{itemize}
			\item $M = cM'$
				\begin{itemize}
					\item $a = c$ \\
						���X�̎����ȉ��̗l�ɂȂ�B
						\[
						\begin{array}{ccc}
							\infer{	\lambda x.(\rho a.aM') : \beta \ra \alpha}{
								\infer{\rho a.aM' : \alpha}{
									\infer{aM' : \alpha}{M' : \alpha}
								}
							}
							& \rhd &
							\infer{\rho a.(\lambda x.[\lambda y.a(\lambda z.y)/a](aM')) : \beta \ra \alpha}{
								\infer{\lambda x.[\lambda y.a(\lambda z.y)/a](aM') : \beta \ra \alpha}{
									[\lambda y.a(\lambda z.y)/a](aM') : \alpha								
								}
							}
						\end{array}
						\]
						�A�[�@�̉����� $\vdash [\lambda y.a(\lambda z.y)/a]M' : \alpha$ �B\\
						$[\lambda y.a(\lambda z.y)/a](aM')$ ����
						$(\lambda y.a(\lambda z.y))[\lambda y.a(\lambda z.y)/a]M'$ �̐��_�}�͈ȉ��̒ʂ�B
						\[
						\infer{(\lambda y.a(\lambda z.y))[\lambda y.a(\lambda z.y)/a]M' : \alpha}{
							\infer{\lambda y.a(\lambda z.y) : \alpha \ra \alpha}{
								\infer{a(\lambda z.y) : \alpha}{
									\infer{\lambda z.y : \beta \ra \alpha}{y : \alpha}
								}
							}
							&
							[\lambda y.a(\lambda z.y)/a]M' : \alpha
						}
						\]
					\item $a \neq c$ \\
					��̏ꍇ�Ɠ��l�B\\
				\end{itemize}
		\end{itemize}

	\item $\rho a.(\rho b.M) \rhd_{1\rho\beta} \rho a.[a/b]M$
		\[
		\begin{array}{ccc}
			\infer{\rho a.(\rho b.M)) : \alpha}{
				\infer{\rho b.M : \alpha}{M : \alpha}
			}
			& \rhd &
			\infer{\rho a.[a/b]M : \alpha}{ [a/b]M : \alpha}
		\end{array}
		\]	
		$\vdash_{\rho\lambda} M : \alpha \Ra \vdash_{\rho\lambda} [a/b]M : \alpha$ �ł��鎖��
		$M$ �̍\���Ɋւ���A�[�@�ŏؖ�����B�w�ǂ���̏ꍇ�Ɠ��l�ɏo����̂�
		�Ⴄ�_�݂̂������B
		\begin{itemize}
			\item $M \equiv cM'$ \\
				�A�[�@�̉����� $\vdash [a/b]M' : \beta$ �B
				$c[a/b]M' \equiv [a/b]cM' \equiv [a/b]M$ �ƂȂ�̂ŁA
				$\vdash [a/b]M : \alpha$ ���ؖ��ł���B$\square$\\
		\end{itemize}
\end{enumerate}


\begin{lemma} \label{lem4-5}
	�^�t���\�� $\lambda\rho$-term �̌`�� $M$ �܂��� $\rho a.M$ �Ȃ��
	$a\beta$-reduction ���s�����Ő��K���ł���B�A�� $M$ �� $\rho$ �͌���Ȃ��B
\end{lemma}

{\bf �ؖ� :}\ \ \ \ $M$ �� $\rho$ �͌���Ȃ��ׁA�N���肤�� reduction ��
\[
\begin{array}{rcl}
	(aM)N & \rhd_{1\rho\beta} & aM \\
	(\lambda x.M)N & \rhd_{1\rho\beta} & [N/x]M
\end{array}
\]
�̓�ʂ�̂݁B�����ŁA�^�t���\�� $M$ �Ɋւ��� $\vdash_{\rho\beta} M : \alpha$
�Ɋւ���ɑ�_������
\begin{itemize}
	\item $(\to-I)$ �̌��_�A���� $(\to-E)$�̑O��ɂȂ��Ă������
	\item $(Absurd)$ �̌��_�A���� $(\to-E)$�̑O��ɂȂ��Ă������
\end{itemize}
�ƒ�`����B
���_�}�Ɋ܂܂��ɑ�_�����̒��ōł��������̂̒����� $l$ �A�܂����_�}�Ɋ܂܂��
���� $l$ �̋ɑ�_������ $n$ �Ƃ��A$l$ �� $n$ �̓�d�A�[�@�ŏؖ�����B\\

���_�}�̒����璷�� $l$ �̋ɑ�_�����ŁA���̒������̘_�����̏�ɂ͒��� $l$ ��
�ɑ�_�����������̂�I�ԁB���̋ɑ�_���� ($\alpha \to \beta$ �Ƃ���) �ł�
$a\beta$-reduction ���s���B���̌��ʓ����鐄�_�}�ł͐V���� $\alpha$ ��
�ɑ�_�����ɂȂ�\�������邪�A���� $l$ �̋ɑ�_�����̌��� $n-1$ �Ɍ���B
�A�[�@�̉���Ɉ˂�A���̐��_�}�ŉ��񂩂� $a\beta$-reduction ���s�����Ő��K��
�o����B\\

�ȏ���A�藝\ref{th4} �͔C�ӂ̌^�t���\�� $\lambda\rho$-term : $X$ �ɑ΂�
\begin{enumerate}
	\item �⏕�藝 \ref{lem4-1} ��p���� $X$ �� $\rho$-reduction ����B
		���̕ό`�œ����� $M$ �������� $\rho a.M$ �� $X$ �Ɠ��� type �Ō^�t���\�ł��鎖��
		�⏕�藝 \ref{lem4-4} ����ؖ�����Ă���B
	\item	��œ�����ό`���ꂽ $M$ �������� $\rho a.M$ ��⏕�藝 \ref{lem4-5} ��p���Đ��K������B
\end{enumerate}
�̎葱���𓥂ގ��ŏؖ��ł���B$\square$(�藝\ref{th4})

\newpage


% ��5��
\section{$\lambda\rho$-calculus �̍�����}

�ÐX--�� (\cite{Komori2003}) �ł́A$\lambda\rho$-reduction �̃`���[�`�E���b�T�[�����ؖ������
���邪�A���� rule
\[
	( \eta )\ : \ \lambda x.Mx  \rhd M \ \ \ (\textmc{�A�� $x$ �� $M$ �̒��Ɏ��R�Ɍ���Ȃ�})
\]
���������̌n�ł͐��藧���Ȃ��B���̎��� ���c ���x (\cite{Fujita2004}) ���w�E�����ȉ��̗Ⴉ��e�Ղ�
����B\\

\begin{example}
	\[ 	\lambda x.(\rho a.ay)x \]
	\[
	\begin{array}{lcl}
		\lambda x.(\rho a.ay)x & \rhd & \rho a.ay \\
		\\
		\lambda x.(\rho a.ay)x & \rhd & \lambda x.(\rho a.(\lambda x'.[\lambda y'.a(y'x')/a]((ay)x'))x) \\
		& \rhd & \lambda x.(\rho a.(\lambda x'.a(yx'))x) \\
		& \rhd & \lambda x.(\rho a.a(yx)) \\
	\end{array}
	\]\\
\end{example}


�܂��{���� $\lambda\rho$-reduction rule �ł��`���[�`�E���b�T�[�����ؖ��ł��Ȃ��B
�ȉ��� ���c (\cite{Fujita2004}) ���w�E���������������B\\

\begin{example}
	\[ (\rho a.ax)(\rho b.by) \]
	��� $(\rho a.ax)N$ ��ό`����ꍇ
	\[
	\begin{array}{cl}
		\rhd & \rho a.(\lambda x'.[\lambda y'.a(y'x')/a]((ax)x'))(\rho b.by) \\
		\rhd & \rho a.(\lambda x'.(\lambda y'.a(y'x'))x)(\rho b.by) \\
		\rhd & \rho a.(\lambda x'.a(xx'))(\rho b.by) \\
		\rhd & \rho a. \rho b.(\lambda x''.[\lambda y''.b(x''y'')/b](x''(by)))(\lambda x'.a(xx')) \\
		\rhd & \rho a. \rho b.(\lambda x''.x''((\lambda y''.b(x''y''))y))(\lambda x'.a(xx')) \\
		\rhd & \rho a. \rho b.(\lambda x''.x''(b(x''y)))(\lambda x'.a(xx')) \\
		\rhd & \rho a.[a/b](\lambda x''.x''(b(x''y)))(\lambda x'.a(xx')) \\
		\rhd & \rho a.(\lambda x''.x''(a(x''y)))(\lambda x'.a(xx')) \\
		\rhd & \rho a.(\lambda x'.a(xx'))(a((\lambda x'.a(xx'))y)) \\
		\rhd & \rho a.(\lambda x'.a(xx'))(a(a(xy))) \\
		\rhd & \rho a.a(x(a(a(xy))))
	\end{array}
	\]
	��� $N(\rho b.by)$ ��ό`����ꍇ
	\[
	\begin{array}{cl}
		\rhd & \rho b.(\lambda x''.[\lambda y''.b(x''y'')/b](x''(by)))(\rho a.ax) \\
		\rhd & \rho b.(\lambda x''.x''((\lambda y''.b(x''y''))y))(\rho a.ax) \\
		\rhd & \rho b.(\lambda x''.x''(b(x''y)))(\rho a.ax) \\
		\rhd & \rho b. \rho a.(\lambda x'.[\lambda y'.a(x'y')/a](x'(ax)))(\lambda x''.x''(b(x''y))) \\
		\rhd & \rho b. \rho a.(\lambda x'.x'((\lambda y'.a(x'y'))x))(\lambda x''.x''(b(x''y))) \\
		\rhd & \rho b. \rho a.(\lambda x'.x'(a(x'x)))(\lambda x''.x''(b(x''y))) \\
		\rhd & \rho a.[a/b](\lambda x'.x'(a(x'x)))(\lambda x''.x''(b(x''y))) \\
		\rhd & \rho a.(\lambda x'.x'(a(x'x)))(\lambda x''.x''(a(x''y))) \\
		\rhd & \rho a.(\lambda x'.x'(a(x'x)))(a(\lambda x''.x''(b(x''y)))x) \\
		\rhd & \rho a.(\lambda x'.x'(a(x'x)))(a(x(a(xy)))) \\
		\rhd & \rho a.a(x(a(xy)))(a(a(x(a(xy)))x)) \\
		\rhd & \rho a.a(x(a(xy)))
	\end{array}
	\]
\end{example}

�����2�̐��K�n�͍��� rule �ł͓������Ȃ��B�]���Č���ł̓`���[�`�E���b�T�[���͐��藧���ċ��Ȃ��B
���̖�����������ׂɁA���Ƃ��Ĉȉ��̗l�� rule ��ǉ����鎖���l����B\\

\begin{example}
	\[
	\begin{array}{rcl}
		\rho a.M & \rhd_{1\rho\beta} & M \ \ \ (\textmc{$a$ �� $M$ �Ɏ��R�Ɍ���Ȃ�)} \\
		a(\rho b.M) & \rhd_{1\rho\beta} & a[a/b]M \\
		a(N(bM)) & \rhd_{1\rho\beta} & a(bM) \\
		a(bM) & \rhd_{1\rho\beta} & \rhd aM
	\end{array}
	\]
\end{example}

����炪�⏕�藝 \ref{lem4-3} �𖞂������͊ȒP�ɏؖ��ł���B
�܂��A�⏕�藝 \ref{lem4-4} �𖞂������͈ȉ��̗l�ɏؖ��ł���B
\begin{itemize}
	\item $(aM)N \rhd_{1\rho\beta} (aM)$
		\[
		\begin{array}{ccc}
			\infer{(aM)N : \alpha}{
				\infer{aM : \beta \ra \alpha}{M : \gamma}
				&
				N : \beta
			}
			& \rhd &
			\infer{aM : \alpha}{M : \gamma}
		\end{array}
		\]

	\item $\rho a.M \rhd_{1\rho\beta} M$ \ \ ($a$ �� $M$ �Ɏ��R�Ɍ���Ȃ�)
		\[
		\begin{array}{ccc}
			\infer{\rho a.M : \alpha}{ M : \alpha} & \rhd & M : \alpha
		\end{array}
		\]	

	\item $a(N(bM)) \rhd a(bM)$
	\[
		\begin{array}{ccc}
		\infer{a(N(bM)) : \alpha}{
			\infer{N(bM) : \beta}{
				N : \gamma \ra \beta
				&
				\infer{bM : \gamma}{M : \delta}
			}
		}
		& \rhd &
		\infer{a(bM) : \alpha}{
			\infer{bM : \gamma}{M : \delta}
		}
		\end{array}
		\]

	\item $a(bM) \rhd aM$
	\[
		\begin{array}{ccc}
		\infer{a(bM) : \alpha}{
			\infer{bM : \gamma}{M : \delta}
		}
		& \rhd &
		\infer{aM : \alpha}{M : \delta}
		\end{array}
	\]
\end{itemize}
������ rule ��������ƁA$(\rho a.ax)(\rho b.by)$ ���瓱�o�ł���2�� $\lambda\rho$-term ��
�������Ȃ�B
\[
\begin{array}{rcl}
		\rho a.a(x(a(a(xy)))) & \rhd & \rho a.a(a(a(xy)) \\
		& \rhd & \rho a.a(xy) \\
		\\
		\rho a.a(x(a(xy))) & \rhd & \rho a.a(xy) \\
\end{array}
\]\\

����A$\eta$-reduction �ɂ��Đ��������鎖���l���Ȃ��Ă͂Ȃ�Ȃ��B2�̐��_���͈ȉ��̗l�ɂȂ�B
\[
\begin{array}{ccc}
	\infer{\lambda x.(\rho a.ay)x : \beta \ra \alpha}{
		\infer{(\rho a.ay)x : \alpha}{
			\infer{\rho a.ay : \beta \ra \alpha}{
				\infer{ay : \beta \ra \alpha}{y : \beta \ra \alpha}
			}
			&
			x : \beta
		}
	}
	& \rhd &
	\infer{\rho a.ay : \beta \ra \alpha}{
		\infer{ay : \beta \ra \alpha}{y : \beta \ra \alpha}
	}
	\\
	\\
	\deduce[\vdots]{\lambda x.(\rho a.ay)x : \beta \ra \alpha}{}
	& \rhd &
	\infer{\rho a.(\lambda x.a(\lambda z.yx)) : \beta \ra \alpha}{
		\infer{\lambda x.a(\lambda z.yx) : \beta \ra \alpha}{
			\infer{a(\lambda z.yx) : \alpha}{
				\infer{\lambda z.yx : \beta \ra \alpha}{
					\infer{yx : \alpha}{y : \beta \ra \alpha & x : \beta}
				}
			}
		}
	}
\end{array}
\]\\

$\rho a.ay$ �� $\rho a.(\lambda x.a(\lambda z.yx))$ �̐��K�n���������Ȃ�l�ȕό`���l����K�v������B

�������ӂ݂āA$aM$ �Ƃ����`�̘_�������d�v�Ȍ��������Ă���ƍl�����邪�A
����� $a$-reduction ��t�������Ă��܂��ƒׂ�Ă��܂������l������B
���̕ӂ�ɂ��āA�悭�l�@���d�˂�K�v�����邾�낤�B

\newpage

% ��7��
\section*{�ӎ�}
�{�_���̍쐬�ɂ�����A�w�������̌ÐX �Y��搶�A�� �V�l������͂���
�ÐX�������̊F�l�A������w�������H�w���̓��c ���x�搶
�ɑ���Ȃ����͂𒸂��܂������Ƃ�S���犴�ӂ������܂��B

\newpage

% �Q�l����
\begin{thebibliography}{9999}
\addcontentsline{toc}{section}{�Q�l����}
\bibitem[HS86]{Hindley0}
	J.\ Roger Hindley and Jonathan P.\ Seldin.
	{\it Introduction to combinators and $\lambda$-calculus}, Vol.1
	of {\it London Mathematical Society Student Texts},
	Cambridge University Press, 1986.
\bibitem[H97]{Hindley1}
	J.\ Roser Hindley.
	{\it Basic Simple Type Theory}, Vol.42
	of {\it Cambridge Tracts in Theoretical Computer Science},
	Cambridge University Press, 1997.
\bibitem[P92]{Parigot}
	Michel Parigot.
	{\it $\lambda\mu$-CALCULUS: AN ALGORITHMIC INTERPRETATION
	OF CLASSICAL NATURAL DEDUCTION},
	Lecture Notes in Computer Science 624, 190-201, 1992.
\bibitem[K02]{Komori2002}
	Yuichi Komori.
	{\it $\lambda\rho$-Calculus: A Natural Deduction for Classical Logic},
	BULLETIN OF THE SECTION OF LOGIC, VOL.31, No.2, 65-70, 2002.
\bibitem[KC03]{Komori2003}
	Yuichi Komori and Arato Cho.
	{\it $\lambda\rho$-calculus},
	preprint.
\bibitem[F04]{Fujita2004}
	���c ���x. {\it �ÐX �Y��ւ̎��M "CR"},
	Tue 06 Jan 2004.
\end{thebibliography}


\end{document}
