\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}  試験 6}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2006 年 1 月 10 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item 述語論理の体系 LJ の基本定理を述語論理の体系 NJ の正規化定理を使って証明せよ。
	(体系 NJ の正規な証明図の長さに関する帰納法によるが, 長さが 1 のとき, 最後に使われた規則が
	導入規則のときは省略してよい。最後に使われている規則が消去規則のときだけを書けばよい。)
% 2
\item  任意のラムダ項 $Z$ にたいして, $\mathsb{Y}(\lambda xy.Z)$ が $x$ についての次の方程式の
	解であることを示せ:
	\[ xy =_\beta Z \ \ .\]
%\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 numeral $\overline{n}$ を次のように帰納的に定義する(ここで $\bot \equiv \lambda xy.y$ である):
	\[ \overline{0} \equiv \lambda x.x, \ \ \ \ \overline{n+1} \equiv \lambda x.x\bot \overline{n}. \]
	このとき, 問題 3 にある閉ラムダ項$\overline{\zeta}, \overline{\sigma}, \overline{\pi}$ を定義
	し, 問題 3 に書かれている性質を満たすことを示せ.
%\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} \]

{\bf 直観主義述語論理 LJ} の公理型は次の２つです.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]

{\bf 直観主義述語論理 LJ} の推論規則は次の 8 つです。
\begin{description}
\item[構造に関する推論規則]\ 
\[
\infer[(w \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(c \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\alpha, \alpha, \Gamma \rightarrow \gamma}
\]
\[
\infer[(e \rightarrow)]
	{\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
	{\Delta, \alpha, \beta, \Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\alpha, \Delta \rightarrow \gamma}
\]
\item[論理記号に関する推論規則]\ 
\[
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\beta, \Delta \rightarrow \gamma}, \hspace{7mm}
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \beta}
\]
\[
	\infer[(\forall \rightarrow)]
		{\forall x \alpha, \Gamma \rightarrow \gamma}
		{[t/x]\alpha, \Gamma \rightarrow \gamma}, \hspace{7mm}
	\infer[(\rightarrow \forall)]
		{\Gamma \rightarrow \forall x \alpha}
		{\Gamma \rightarrow \alpha}
\]
\end{description}

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

\end{document}
