% \documentstyle[proof2, b5j, makeidx]{jbook}
\documentclass[b5paper,11pt]{jsarticle}
\usepackage{latexsym}
\usepackage{proof}
%\documentclass[b5paper]{jsarticle}
\setlength{\textwidth}{120truemm}
%\setlength{\hoffset}{-25.4mm}
%\setlength{\oddsidemargin}{20mm}
%\raggedbottom
%\setlength{\voffset}{-25.4mm}
%\setlength{\topmargin}{27.5mm}
%\setlength{\headheight}{0mm}
%\setlength{\headsep}{0mm}
\setlength{\textheight}{200truemm}
\def\ra{\rightarrow}

\newtheorem{definition}{��`}[section]
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{problem}[definition]{���}

\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{�ÓT�_���̏ؖ��}�ό`�̒�~���ƍ�����}       
\author{�ÐX�Y��(��t��w ���w��)}
\date{}
\begin{document}
\pagestyle{empty}
\maketitle
����$\lambda\rho$-�v�Z�͌ÓT�_���̊܈Ӓf�Ђ̎��R��㈑̌n�ł���B

\begin{definition} ( �^�Ȃ� $\lambda\rho$-�� )
	�Z������ $\lambda$-�ϐ�, $\rho$-�ϐ� ���^�����Ă�����̂Ƃ���B
	$\lambda$-�ϐ�, $\rho$-�ϐ� ���܂Ƃ߂����̂� ���ϐ� �Ƃ�ԁB
	\begin{enumerate}
		\item ���ϐ� �� $\lambda\rho$-�� �ł���B
		\item $M$, $N$ �� $\lambda\rho$-�� �Ȃ�� $(MN)$ �� $\lambda\rho$-�� �ł���B
		\item $M$ �� $\lambda$-��, $f$ �� ���ϐ� �Ȃ��
			$(\lambda f.M)$ �� $\lambda\rho$-�� �ł���B
	\end{enumerate}
\end{definition}

�ϐ� $a$ �� $\rho$-�ϐ��̂Ƃ�, $\lambda a.M$ �� $\rho a.M$ �ƕ\�L����B
���K�^�ɂ��邽�߂̕ό`�K���͎��̂悤�Ȃ��̂ł���B

\begin{definition} ( $\rho\beta$-contraction )
	$\rho\beta$-redex �͈ȉ��ŗ^�����鍶�ӂ̌`������ $\lambda\rho$-�� ��,
	���� contractum �͑Ή�����E�ӂ̌`������ $\lambda\rho$-�� �ł���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 \\
	\end{array}
	\]
\end{definition}

���� $\rho\beta$-reduction �̑̌n�͍�����(Church-Rosser��)�����藧��, ���̏ؖ���
�e�Ղł���B�ȉ��� TA$_\lambda\rho$ (���ꂪ�ÓT�_���̊܈Ӓf�Ђ̑̌n)��
$\lambda\rho$-�� �̌^�t�̑̌n�ł���B

\begin{definition} ( The system $\textmc{TA}_{\lambda\rho}$ )
	$\textmc{TA}_{\lambda\rho}$ �̐��_�K���͈ȉ��� 4 �ł���B
	\[
	\begin{array}{cccc}
		\infer{ MN : \beta }{M : \alpha \ra \beta & N : \alpha}
		&
		\infer{ \lambda x.M : \alpha \ra \beta}
			{\deduce{M : \beta}{\deduce{\Pi}{ x : \alpha  }
		}}
		&
		\infer{ aM : \beta}{ M : \alpha}
		&
		\infer{ \rho a. M : \alpha}{
			\deduce{ M : \alpha }{\deduce{\Pi}{
				\infer{ aQ : \beta }{ Q : \alpha }
			}}
		}
		\end{array}
	\]	
\end{definition}

�̌n TA$_\lambda\rho$ �Ō^�t�\�� $\lambda\rho$-�� �ɂ��Ă͋����K���藝�����藧�B
���R, �㐳�K���藝�����藧�̂ł��邪���̒��ڏؖ���(���̂Ƃ���)�ł��Ȃ��B
���̕ό`�K����t��������Ǝ㐳�K���藝���e�Ղɏؖ��ł���B

\begin{definition} ( $*\rho\beta$-contraction )
	$*\rho\beta$-contraction �� $\rho\beta$-contraction �Ɏ��� 3 �� contraction ��t��������
	���̂ł���B
	\[
	\begin{array}{rcl}
		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}

���������̑̌n�ł͍��������������Ȃ�(���c���x(������)���w�E)�B
�܂�, �ÓT�_���̕ό`�K���� $\eta$-reduction �Ƃ����������� $\rho\beta$-reduction +
$\eta$-reduction �̑̌n�͍��������������Ă��Ȃ��悤�ł���B
�����������藧���Ă��Ȃ��̌n���Ԃ�Ȃ�(reduction �ňڂ����̂𓙂����Ƃ݂Ȃ����Ƃ���
$x=y$ ���o�Ȃ�)���ǂ����͋����[�����ł���B

\begin{problem} ( $*\rho\beta$-contraction )
	\begin{enumerate}
	\item �̌n $*\rho\beta$ �͂Ԃ�Ȃ���?
	\item �̌n $\rho\beta+\eta$ �͂Ԃ�Ȃ���?
	\end{enumerate}
	�ǂ�����^�Ȃ��łԂ��ꍇ�͌^�t�ł͂ǂ���?
\end{problem}

�V�����i�W����������ȉ��ɍڂ���\��ł���B\\
http://www.math.s.chiba-u.ac.jp/\~{}komori/gakkai04-09/
\end{document}
