\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{2012 年 1 月 31 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item 次の 4 つのラムダ項の主要型を求めよ：
  \[\lambda xyz.xy , \ \ \lambda xy.xyy , \ \ (\lambda xy.xyy)(\lambda xyz.x(yz)) , \ \ \lambda xyz.(\lambda xyz.xy)xy(xz) .\]
ただし, 主要型であることは示さなくてよい。その型がそのラムダ項の型であることを示すだけでよい。
% 2
\item  任意のラムダ項 $M$ にたいして, $x$ についての次の方程式が
	解をもつことを示せ:
	\[ xyzu =_\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{mul}$
 	を使って(2 変数関数)べき乗($x^y$)を表す閉ラムダ項 $\overline{pow}$ を表せ
 	($\overline{pow}xy = x^y$).
%\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{12mm}
%\newpage
%{\bf 注意:} これは試験終了後に回収しますので, 書き込みなどはしないで下さい。\\[2mm]
%
%{\bf 注意:} 以下では, 細かな条件(変数条件など)は省略されている。
% また, LJ の体系は教科書とは
% 少し異なっている(右辺は空ということはなく, ちょうど一つの論理式)。

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

\end{document}
