%\documentclass{jarticle}
\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newtheorem{definition}{��`}[section]
\newtheorem{theorem}[definition]{�藝}
%\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{���_���w\Romannumeral{2}  ���� 4}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2003 �N 2 �� 5 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ $\forall y(\forall x(\neg pxx\to pxy)\to\forall x(pxy\to\neg pxx)\to pyy)$
 \ �̏q��_���̑̌n NJ �̏ؖ��}��������.
% 2
\item ������ $ \forall x\ rxx \ra \forall x \forall y \forall z ( rxy \to rxz \to
	\neg ryz \to rzy)$
	���̌n LK �ŏؖ��ł��Ȃ����Ƃ�����.
%\vspace{5mm}
% 3
\item CL �� \ \ $\lambda^* xyz.x(yz)$ \ \ �����߂�($S$, $K$ �ŕ\��)�B
%\vspace{5mm}
% 4
\item CL �� \ \ $(\lambda^* xyz.x(yz))xyz$ \ \ �� weak reduction ����B
%\vspace{5mm}
% 5
\item �����_�� \ \ $\lambda xy.(\lambda uvy.v(xy))(xy)(\lambda z.zy)$ \ \ �����ł���ʓI�Ȍ^
	$\delta$ ������,\\
	\ \ $\lambda xy.(\lambda uvy.v(xy))(xy)(\lambda z.zy)\in\delta$ \ \ �Ɏ��� TA$_\lambda$ �̏ؖ��}
	�������B
%\vspace{5mm}
% 6
%\vspace{2mm}
\item �����_�� \ \ $\lambda xy.(\lambda uvy.v(xy))(xy)(\lambda z.zy)$ \ \ �� $\beta$ ���K�`($\beta$-nf)
	$M$ ������,  $M$ �����ł���ʓI�Ȍ^ $\delta$ ������, \ \ $M\in\delta$ \ \ �Ɏ�
	�� TA$_\lambda$ �̏ؖ��}�������B
\end{enumerate}
%\newpage
\vspace{2cm}
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
\begin{definition}[�\��(structure)]\label{def-structure}\em
���� $\cal L$ �̍\�� $\cal A$ �͎��� 3 �̂��̂���\������Ă��܂�:
\begin{enumerate}
\item $\cal A$ �̐��E�ƌĂ΂���łȂ��W�� $|\cal A|$.
	$|\cal A|$ �̌��� $\cal A$ �̌̂Ƃ����܂�.
\item ���� $\cal L$ �̊e�X�� $n$ �ϐ��֐��L�� $f$ �ɑ΂���, $|\cal A|$ ����
 $|\cal A|$ �ւ� $n$ �ϐ��֐� $f_{\cal A}$.
 (�Ƃ���, 0 �ϐ��֐��L�� $e$ �ɑ΂���, $e_{\cal A}$ �� $\cal A$ �̌̂ł�.)
\item ���� $\cal L$ �̊e�X�� $n$ �ϐ��q��L�� $p$ �ɑ΂���, $|\cal A|$ �� $n$
 �̒��� $|{\cal A}|^n$ �̕����W�� $p_{\cal A}$.
\end{enumerate}
\end{definition}

���� $\cal L$ �� $\cal A$ �̌̂̑S�Ă̖��O��t�������ē����錾��
�� $\cal L(A)$ �Ə����܂�. �� $c$ �̖��O�� $\bar{c}$ �Ə����܂�. 

$t$ ������ $\cal L(A)$ �̕��Ƃ��܂�. ���� ${\cal A}$ �̌� ${\cal A}(t)$
 ���A�[�I�ɒ�`���܂�.
\begin{enumerate}
\item ${\cal A}(\bar{c}) = c$,
\item ${\cal A}(ft_1...t_n) = f_{\cal A}({\cal A}(t_1),...,{\cal A}(t_n))$.
\end{enumerate}

$\alpha$ ������ $\cal L(A)$ �̕_�����Ƃ��܂�. ���� $\alpha$ �̐^�U�l
 ${\cal A}(\alpha)$ ���A
�[�I�ɒ�`���܂�.
\begin{definition}\em \ 
\begin{enumerate} 
\item ${\cal A}(pt_1...t_n) = \top \Longleftrightarrow p_{\cal A}
({\cal A}(t_1),...,{\cal A}(t_n))$,
\item ${\cal A}(\bot) = \bot$,
\item ${\cal A}(\alpha \to \beta) = {\cal A}(\alpha) \to {\cal A}(\beta)$,
\item ${\cal A}(\forall x \alpha) = \top \Longleftrightarrow 
�C�ӂ� {\cal A} �̌� c �ɑ΂��� {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{definition}

$\Gamma \ra \Theta$ ������ $\cal L$ �̕������Ƃ��܂�. �S�Ă� $\alpha \in
 \Gamma$ �ɂ��� ${\cal A}(\alpha) = \top$ �̂Ƃ��ɂ�, ���� $\beta \in \Theta$
 �����݂��� ${\cal A}(\beta) = \top$ �ƂȂ�Ƃ�, ������ $\Gamma \ra \Theta$
 �� $\cal A$ �Ő������Ƃ����܂�.

$\Gamma \ra \Theta$ ������ $\cal L$ �̐������Ƃ��܂�. $\Gamma \ra \Theta$ ��
���R�Ɍ����̕ϐ��̑S�Ă� $y_1,...,y_n,...$ �Ƃ��܂�. ��
��, $t_1,...,t_n,...$  ��
���� $\cal L(A)$ �̕��Ƃ��܂�.  $\Gamma \ra \Theta$ ��
���R�ϐ� $y_1,...,y_n,...$ �� $t_1,...,t_n,...$ �����ꂼ�������ē�����
���� $\cal L(A)$ �̕�������
 $\Gamma \ra \Theta$ �� $\cal A$-{\bf �����} �Ƃ����܂�.  $\Gamma \ra \Theta$ �̔C�ӂ�
 $\cal A$-����� $\Gamma' \ra \Theta'$ �� $\cal A$ �Ő������Ƃ�,
 ������ $\Gamma \ra \Theta$ �͍\�� $\cal A$ �Ő������Ƃ����܂�.

$\Gamma \ra \Theta$ ������ $\cal L$ �̐������Ƃ��܂�. $\cal L$ �̔C�ӂ̍\
�� $\cal A$ �� $\Gamma \ra \Theta$ ���������Ƃ�, $\Gamma \ra \Theta$ ��
{\bf �P�^}�ł���Ƃ����܂�.
%
\begin{theorem}[LK �̌��S���藝]\label{the-LK-kenzen}\em
������ $\Gamma \ra \Theta$ �� LK �ŏؖ��ł����, $\Gamma \ra \Theta$ ��
�P�^�ł���.
\end{theorem}

������ $\Gamma \ra \Theta$ ���P�^�łȂ���
��, ����\�� $\cal A$ �� $\Gamma \ra \Theta$ �� $\cal A$-�����
 $\Gamma' \ra \Theta'$ �����݂���, �S�Ă� $\alpha \in \Gamma'$ �ɂ���
 ${\cal A}(\alpha) = \top$ �� �S�Ă�
 $\beta \in \Theta'$ �ɂ��� ${\cal A}(\beta) = \bot$ �ƂȂ��Ă���Ƃ��ł�.
 ���̂悤�ȍ\�� $\cal A$ �� $\cal A$-����� $\Gamma' \ra \Theta'$ �̑�
 $<{\cal A},\Gamma' \ra \Theta'>$ �𐄌��� $\Gamma \ra \Theta$ ��{\bf ����
}�Ƃ����܂�. 

\newpage
\begin{definition}[Weak reduction]\em
Any CL-term $KXY$ or $SXYZ$ is called a (weak) redex. Contracting an occurence of a redex in a term
$U$ means replacing one occurence of
\[\begin{array}{lll}
KXY & by & X, \\
SXYZ & by & XZ(YZ).\\
\end{array}\]
If this changes $U$ to $U'$, we say that $U$ (weakly) contracts to $U'$ , or
\[U\rhd_{1w} U'.\]
We say that $U$ (weakly) reduces to $V$, or
\[U\rhd_w V\]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of weak contractions.
\end{definition}

\begin{definition}[Abstraction]\label{def-abstraction}\em
For each CL-term $M$ and each variable $x$, a CL-term $\lambda^* x.M$ is defined by induction on $M$, thus:
\[\begin{array}{lllll}
(a) & \lambda^* x.M & \equiv & KM & \mbox{if\ } x\notin FV(M);\\
(b) & \lambda^* x.x & \equiv & SKK & ;\\
(c) & \lambda^* x.Ux  & \equiv & U   & \mbox{if\ } x\notin FV(U);\\
(d) & \lambda^* x.UV  & \equiv & S(\lambda^* x.U)(\lambda^* x.V) & \mbox{if neither (a) nor (c) applies.}
\end{array}\]
\end{definition}

\begin{definition}[The type-assignment system TA$_\lambda$]\em
It has no axiom-schemes and two rules the $\ra$-elimination rule ($\ra$e) and
the $\ra$-introduction rule ($\ra$i);
$$ 
\infer[(\ra\mbox{e})]{XY\in\beta}{X\in\alpha \ra \beta & Y\in\alpha},
$$
$$ 
\infer[(\ra\mbox{i})]{\lambda x.M \in \alpha\ra\beta}{\deduce{M\in\beta}{[x\in\alpha]}}.
$$
\end{definition}

\end{document}
