\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}
\newtheorem{definition}{定義}[section]
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{情報数理学特論\Romannumeral{7}  試験 5}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2010 年 12 月 21 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item 述語論理の体系 NJ の正規化定理を証明せよ。
% 2
\item  任意のラムダ項 $M$ にたいして, $\mathsb{Y}(\lambda xyz.M)$ が $x$ についての次の方程式の
	解であることを示せ:
	\[ xyz =_\beta M \ \ .\]
%\vspace{5mm}
% 3
\item $\overline{\zeta}$, $\overline{\sigma}$, $\overline{\pi}$
	を次の関係を満たしている閉ラムダ項とする:
	\[ \overline{\zeta}\,\overline{0}=_\beta \lambda xy.x, \ \ \ 
	\overline{\zeta}\,\overline{n}=_\beta \lambda xy.y \ (n\geq1), \]
	\[ \overline{\sigma}\,\overline{n}=_\beta \overline{n+1}, \ \ \ 
	\overline{\pi}\,\overline{n}=_\beta\overline{n-1}\ (n\geq1). \]
	不動点結合子 $\mathsb{Y}$ および 上記の閉ラムダ項 $\overline{\zeta}$, $\overline{\sigma}$,
	$\overline{\pi}$ と(2 変数関数)和を表す閉ラムダ項 $\overline{add}$
 	を使って(2 変数関数)積を表す閉ラムダ項 $\overline{mul}$ を表せ.
%\vspace{2mm}
% 4
\item 次の 2 つのラムダ項の主要型を求めよ:
\[ \lambda xyz.(\lambda xy.x)xzy \ (\mbox{よりかっこを省略せずに書くと\ } \lambda xyz.((\lambda xy.x)xzy) ),\]
\[ \lambda xy.x(xy). \]
ただし, 主要型であることは示さなくてよい。その型がそのラムダ項の型であることを示すだけでよい。
%\vspace{5mm}
% 5
%\vspace{5mm}
\end{enumerate}
\vspace{10mm}
%\newpage
%{\bf 注意:} これは試験終了後に回収しますので, 書き込みなどはしないで下さい。\\[2mm]
%
{\bf 注意:} 以下では, 細かな条件(変数条件など)は省略されている。
% また, LJ の体系は教科書とは
% 少し異なっている(右辺は空ということはなく, ちょうど一つの論理式)。

{\bf 直観主義述語論理 NJ} の推論規則は次の 5 つです。
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha} \hspace{5mm}
 \infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}} \]
\[ \infer{\mathsb{A}M:\alpha}{M:\bot} \hspace{5mm}
 \infer{\mathsb{J}M: \forall x \alpha}{M: \alpha} \hspace{5mm}
 \infer{\mathsb{F}M: [t/x]\alpha}{M: \forall x \alpha} \]

不動点結合子 $\mathsb{Y}$ は次の式を満たす:
\[ \mathsb{Y}x =_\beta x(\mathsb{Y}x) \ \ .\]

\end{document}
