\documentclass[a4paper,12pt]{jsarticle}
%\documentclass[a4paper]{slides}
%\documentclass[a4paper,landscape]{slides}
\usepackage{proof,color}
% \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{definition}{��`}
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{problem}[definition]{���}
\newtheorem{example}[definition]{��}

\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{�ÓT�_���̏ؖ��}�ό`�̒�~���ƍ�����}       
\author{�ÐX�Y��(��t��w ���w��)}
\date{2004 �N 9 �� 24 ��}
\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\rho$-��, $f$ �� ���ϐ� �Ȃ��
			$(\lambda f.M)$ �� $\lambda\rho$-�� �ł���B
	\end{enumerate}
\end{definition}

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

\begin{definition}\label{contraction} ( $\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}

\begin{example}[$((\alpha \to \beta) \to \alpha) \to \alpha$]
\[\infer[\lambda y]{\lambda y. \rho a. y(\lambda x.ax):((\alpha \to \beta) \to \alpha)
\to \alpha}{\infer[\rho a]{\rho a. y(\lambda x.ax):\alpha}{\infer
{y(\lambda x.ax):\alpha}{
y:(\alpha \to \beta) \to \alpha &
\infer[\lambda x]{\lambda x.ax:\alpha \to \beta}{\infer[a]{ax:\beta}
{x:\alpha}}}}}, \]
%
����͏ȗ��`�ł͎��̂悤�ɏ������(�ȗ��`���猳�̏ؖ��}�����S�ɕ����ł��邱�Ƃɒ��ӂ���);
\[\infer[\lambda y]{((\alpha \to \beta) \to \alpha) \to \alpha}
{\infer[\rho a]{\hspace{2mm}\alpha\hspace{2mm}}{\infer{\alpha}
{y:(\alpha \to \beta) \to \alpha &
\infer[\lambda x]{\alpha \to \beta}{\infer[a]{\beta}
{x:\alpha}}}}}. \]
\end{example}

\begin{example}[��`\ref{contraction}�� 3 �Ԗڂ� contraction]
$M\equiv z(\lambda u.au)$ �Ƃ���ƍ��ӂ͎��̏ؖ��}�ɂȂ�:
\[\infer{\beta}
{\infer[\rho a]{\hspace{2mm}\alpha\to\beta\hspace{2mm}}{\infer{\alpha\to\beta}
{z:((\alpha \to \beta)\to\gamma) \to \alpha\to\beta &
\infer[\lambda u]{(\alpha \to \beta)\to \gamma}{\infer[a]{\gamma}
{u:\alpha\to\beta}}}}
& \infer*{N:\alpha}{}
}. \]
�E�ӂ͂��̂܂܂ł͕��G�Ȃ̂Œ�`\ref{contraction}�� 2 �Ԗڂ� reduction($\beta$-reduction)
������� $\rho a.z(\lambda u.a(uN))N$ �ƂȂ�, ����͎��̏ؖ��}�ɂȂ�:
\[\infer[\rho a]{\beta}
{\infer{\hspace{2mm}\beta\hspace{2mm}}{\infer{\alpha\to\beta}
{z:((\alpha \to \beta)\to\gamma) \to \alpha\to\beta &
\infer[\lambda u]{(\alpha \to \beta)\to \gamma}{\infer[a]{\gamma}{\infer{\beta}
{u:\alpha\to\beta & \infer*{N:\alpha}{}}}}}& \infer*{N:\alpha}{}}
}. \]
$a$ �� $\rho a$ �̓K�p���Ȃ�ׂ������Ș_�����ɂ���悤�ȕω��ɂȂ��Ă��邱�Ƃ�������B
\end{example}

�̌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(�Q�n��)���w�E)�B
�܂�, �ÓT�_���̕ό`�K���� $\eta$-reduction �Ƃ����������� $\rho\beta$-reduction +
$\eta$-reduction �̑̌n�͍��������������Ă��Ȃ�($\lambda x.(\rho a.ay)x$ �� $\eta$-reduction
���ɂ��� $\rho a.ay$ �ƂȂ�, $\rho$ �ɂ��Ă� reduction ���ɂ��X�ɉ��� reduction
������� $\lambda xa.a(yx)$ �ƂȂ�B�ǂ����$\rho\beta$-reduction +$\eta$-reduction �ɂ����Đ��K
�`�ł���B���̗�ł� $\rho a.aM\rhd\rho a.M$, \ \ $\rho a.M\rhd M \ \ \mbox{if}\ a\notin FV(M)$\ \ ��������� $y$ �ɍ�������)�B
�����������藧���Ă��Ȃ��̌n���Ԃ�Ȃ�(reduction �ňڂ����̂𓙂����Ƃ݂Ȃ����Ƃ���
$x=y$ ���o�Ȃ�)���ǂ����͋����[�����ł���B

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