\documentclass{jsarticle}
\usepackage{amssymb}		%\rhd
\usepackage{amsmath}		%\cfrac
\usepackage{bussproofs}		%for proof trees
\newcommand{\sem}[1]{[\![ #1 ]\!]}

\title{コンピュータサイエンス入門\\
〜アルゴリズムとプログラミング言語〜\\
問の解答例}
\begin{document}
\maketitle

\noindent
{\bf 問3.3}(p.~35)~関数
\[
 f(n)=\cfrac{2n+(-1)^nn}{3}
\]
が例である．理由は以下の通りである．

オーダー記法の定義より，$\Theta(n) = O(n) \cap \Omega(n)$である．ここで
\begin{align}
O(n)      &=\{g(n)\mid \exists N > 0, \exists C > 0, \forall n \geq N, g(n) \leq Cn \}\\
\Omega(n) &=\{g(n)\mid \exists N > 0, \exists C > 0, \forall n \geq N, g(n) \geq Cn \}
\end{align}
である．
\begin{align}
\forall n \geq 1, f(n) \leq n\\
\forall n \geq 1, f(n) \geq \cfrac{1}{3}n
\end{align}
である．したがって，$f (n) \in O(n)$ かつ $f (n) \in \Omega(n)$，すなわち$f(n) \in \Theta(n)$である．

また，$\cfrac{f(n)}{n}$は充分に大きい$n$について$\cfrac{1}{3}$と$\cfrac{2}{3}$を振動するために，$\lim_{n\rightarrow\infty} \cfrac{f(n)}{n}$は収束しない．\\

\noindent
{\bf 問4.7}(p.~49)~深さ$d$のAVL木のうち，もっとも節が少ない木の節の数を$N_d$とし，その木の葉の数を$L_d$とする．すると
\begin{align}
N_d &= 2L_d - 1 \label{avl:1}\\
L_0 &= 1 \label{avl:2}\\
L_1 &= 2 \label{avl:3}\\
L_d &= L_{d-1} + L_{d-2}\qquad (d \geq 2) \label{leaf_rec}
\end{align}
という式が成り立つ．ここで，式\ref{leaf_rec}は，深さ$d$ ($d\geq 2$)のもっとも葉が少ないAVL木の部分木が深さ$d-1$と深さ$d-2$のもっとも葉が少ないAVL木であれば良いことから成り立つ．

\{$L_d$\}は，初項を取り除いたフィボナッチ数列$\{F_k\}$:
\begin{align}
 F_0 &= 0\\
 F_1 &= 1\\
 F_k &= F_{k-1} + F_{k-2} \qquad (k\geq 2)
\end{align}
と等しく，$N_d = \Omega(e^d)$である．よって$d=O(\log N_d)=O(\log n)$である．
\\

\noindent
{\bf 問5.1}(p.~67)~$X$が有限とすると$X$の上限$\sqcup X$は$X$に含まれる．よって$\sqcup X \not\in X$ならば$X$は無限の要素をもつ．
\\

\noindent
{\bf 問5.2}(p.~63)~
\begin{align}
 \sum_{i=2}^n\lfloor\log i\rfloor &\leq \int_2^n \log x\, dx = \left[x \log x\right]_2^n = n \log n - 2 \log 2 = O(n\log n)\\
 \sum_{i=2}^n\lfloor\log i\rfloor &\geq \int_2^n \log x-1\, dx = \left[x \log x-1\right]_2^n = n \log n + n - 2 \log 2 - 2 = \Omega(n\log n)
\end{align}
より，
\begin{equation}
 \sum_{i=2}^n\lfloor\log i\rfloor = \Theta(n\log n)
\end{equation}
が得られる．
\\


re\noindent
{\bf 問5.5}(p.~71)~入力されるリストの長さが$n=2^m$のときのマージソートの最悪の場合の計算量を$T(n)=m2^m-2^m+1$とおく．
% 入力されるリストの長さ$n$が$2^m \leq n < 2^{m+1}$のときのマージソートの最悪の場合の計算量は$T(2n)$である．
% $\frac{T(2n)}{T(n)} < 2$
$T(2n)/T(n) < 2$
であるので，$T(n)<T(n+1)<\cdots<T(2n)<2T(n) = O(n\log n)$である．したがって，$n=2^m$を満たす任意の$m$について，$i=0,1,\ldots,2^m-1$について$T(n+i) < 2 T(n)=O(n\log n)$である．よって，リストの長さ$n$が一般の場合も，マージソートの最悪の場合の計算量は$O(n\log n)$である．
\\

\noindent
{\bf 問8.1}(p.~102)~任意の$Y(Y\neq X_j \mbox{~for~} j=1,\ldots,m)$と$m\geq 3$について，
\[
 \bigvee_{j=1}^{m}X_j=(X_1 \vee X_2 \vee Y) \wedge \bigvee_{j=3}^{m}X_j
\]
である．この変形を繰り返し行うことで，任意の論理式標準形は3-論理積標準形に変形される．この変形を行う必要がある回数はリテラルの数で押さえられる．よって，SATは3-SATに多項式還元できるので，3-SATも$\mathit{NP}$完全である．
\\

\noindent
{\bf 問8.2}(p.~103)~三色を$\{1,2,3\}$として，$x_j$の色を$1$，$\neg x_j$の色を$0$としても一般性を失わない．$v_1$の色は$y_{i,5}$の色に一致する．$L_{i,1}$, $L_{i,2}$, $L_{i,3}$がすべて色$0$であるとき，$y_{i,5}$は色$0$になる．それ以外のとき，すなわち少なくとも$L_{i,1}$, $L_{i,2}$, $L_{i,3}$のひとつが色$1$であるときは$y_{i,5}$は$0$にも$1$にも彩色できる．

($\Leftarrow$) 3-SAT
\begin{equation}
\bigwedge_{i=1}^{n}\left(\bigvee_{j=1}^{m(i)}L_{i,j}\right)
\label{eq:3cnf}
\end{equation}
が充足可能であるとする．グラフ$G$の$v_1$を$x_j$と同じ色$1$に彩色し，$L_{i,j}$を色$0$か色$1$にそれぞれ彩色する．任意の$i$について，少なくとも$L_{i,1}$, $L_{i,2}$, $L_{i,3}$のひとつが色$1$であることから，$y_{i,5}$は$1$に彩色できる．このようにすべての頂点に彩色できる．

($\Rightarrow$)グラフGが3彩色できていたとする．上記の仮定をおいても一般性を失っていないことに注意して欲しい．この場合，少なくとも$L_{i,1}$, $L_{i,2}$, $L_{i,3}$のひとつが色$1$である．各リテラル$L_{i,j}$が，色0のとき真，色1のとき偽になるようにすると，すべての和が真となるので，式\ref{eq:3cnf}は充足される．
\\

\noindent
{\bf 問10.1}(p.~137)
p.~137に以下のように関数の定義がある．
\begin{quote}
$f$が$A$から$B$への関数であるのは，任意の$x\in A$について$(x,y)\in f$となる$y\in B$があり，任意の$x\in A, y\in B, z \in B$について$(x,y)\in f$かつ$(x,z)\in f$なら$y=z$となるときである．
\end{quote}
$R$が関数であることから，任意の$x$について$(x,z)\in R$となる$z\in A$があり，任意の$x, z\in A, z'\in A $について$(x,z)\in R$かつ$(x,z')\in R$なら$z=z'$となる．同様に，$S$が関数であることから，任意の$z$について$(z,y)\in S$となる$y$があり，任意の$z\in A, y, y'$について$(z,y)\in S$かつ$(z,y')\in S$なら$z=z'$となる．これらから，任意の$x$について$(x,y)\in RS$となる$y$があり，任意の$x, y, y'$について$(x,y)\in RS$かつ$(x,y')\in RS$なら$y=y'$となる．したがって$RS$は関数である．

以下のように式に名前を付ける．

\begin{equation}
R^* = \bigcup\{R^n\mid n\geq 0\}
\end{equation}

$(\supseteq)$の証明．任意の自然数$k$について，$R^* \supseteq R^k$であることを，$k$についての帰納法で示す．
\begin{description}
 \item[$k=0$の場合] 
	    $R^0$は反射的でない関係を含まないので反射的関係$R^*$に含まれる．すなわち，$R^* \supseteq R^0$である．
 \item[$k=l+1$の場合] 
	    帰納法の仮定より$R^* \supseteq R^l$である．$R^*$が推移的であるから$R^* \supseteq R^lR$である．よって$R^* \supseteq R^{l+1}$である．
\end{description}

$(\subseteq)$の証明．$R^*$は$R$の反射的推移的閉包であるので，$(x_0,y)\in R^*$ならばある$k~(\geq 0)$が存在して$(x_0,x_1)\in R, \ldots, (x_{k-1},x_k)\in R$, かつ$x_k=y$, すなわち$(x_0,y)\in R^k$である．
\\

\noindent
{\bf 問11.1}(p.~141) (i) $\emptyset \in \mathcal{R}^0 \subset \bigcup\{\mathcal{R}^n \mid n\geq 0\} = \mathcal{R}$.

(ii) $\{\epsilon\} \in \mathcal{R}^1 \subset \bigcup\{\mathcal{R}^n \mid n\geq 0\} = \mathcal{R}$.

(iii) すべての$a\in\Sigma$について，$\{a\} \in \{\{b\}\mid b \in \Sigma\}\subset \mathcal{R}^1 \subset \bigcup\{\mathcal{R}^n \mid n\geq 0\} = \mathcal{R}$.

(iv) $R\in \mathcal{R}$であることから，ある$k$が存在して$R\in \mathcal{R}^k$である．
よって，$R^* \in \{S^*\mid S\in \mathcal{R}^{k}\}\subset \mathcal{R}^{k+1} \subset \mathcal{R}$である．

(v) $R_1, R_2 \in \mathcal{R}$であることから，ある$k$が存在して$R_1, R_2 \in \mathcal{R}^k$である．
よって，
\begin{align}
R_1R_2 &\in \{S_1S_2 \mid S_1\in \mathcal{R}^{k}, S_2\in \mathcal{R}^{k}\}\subset \mathcal{R}^{k+1} \subset \mathcal{R}\\
R_1\cup R_2 &\in \{S_1\cup S_2 \mid S_1\in \mathcal{R}^{k}, S_2\in \mathcal{R}^{k}\}\subset \mathcal{R}^{k+1} \subset \mathcal{R}
\end{align}
である．

ある集合$A$が(i)から(v)までの性質を満たすというのは，以下の性質が成り立つことである．
\begin{enumerate}
 \renewcommand{\labelenumi}{(\roman{enumi})}
 \item $\emptyset \in A$
 \item $\{\epsilon\} \in A$
 \item すべての$a\in\Sigma$について$\{a\}\in A$
 \item $R\in A$なら$R^*\in A$である．
 \item $R_1,R_2\in A$なら$R_1R_2\in A$かつ$R_1\cup R_2\in A$である．
\end{enumerate}

任意の$n$について$\mathcal{R}^n\subseteq A$であることを，任意の$S\in\mathcal{R}^n$が$S\in A$であることを$n$に関する帰納法により示す．

$n=0$の場合．前提が空であり成り立つ．

$n=k+1$の場合．帰納法の仮定より，任意の$S\in\mathcal{R}^k$が$S\in A$である．これと上の性質(i)から(v)より漸化式の右辺の和を構成するどの集合の要素でも$A$に属することがいえる．よって，任意の$S\in\mathcal{R}^{k+1}$が$S\in A$である．

以上より，任意の$n$について$\mathcal{R}^n\subseteq A$であることが示された．

（任意の$n$について$\mathcal{R}^n$が離散集合であることから，）
(i)から(v)までの性質を満たす任意の集合$A$と任意の$n$について，$\mathcal{R}^n \subseteq A$であり，したがって，$\mathcal{R} = \bigcup\{\mathcal{R}^n\mid n \geq 0 \} \subseteq A$である．この$A$の任意性により$\mathcal{R}$は(i)から(v)を満たす最小の集合である．
\\

\noindent
{\bf 問11.2}(p.~141) 性質(i)の証明．$R$が正規言語であることから，p.~140の性質(ii)と(v)および$\cdot^n$の定義を用いた$n$に関する帰納法により，任意の$n$について$R^n$は正規言語である．

性質(ii)の証明．$R$が正規言語であることから，p.~140の性質(iv)より$R^*$は正規言語である．よって，p.~140の性質(v)より，$RR^*$すなわち$R^+$は正規言語である．

性質(iv)の証明．$R_1,R_2$が正規言語であることから，$\Sigma^*\backslash R_1$と$\Sigma^*\backslash R_2$が正規言語であり，よって$R_1\cup R_2 = \Sigma^*\backslash((\Sigma^*\backslash R_1) \cup (\Sigma^*\backslash R_2))$も正規言語である．
\\

\noindent
{\bf 問11.3}(p.~141) $X=\bigcup\{R^nS\mid n \geq 0\}$が唯一存在する．p.~140の性質(v)を用いた帰納法により$X$は正規言語であることが示される．
\\

\noindent
{\bf 問11.4}(p.~146) $w$の長さに関する帰納法を用いる．

$w$の長さが$0$の場合：$\hat{\delta}$の定義から明らか．

$w$の長さが$1$より大きい場合：$w$を$aw'$とする．
\begin{align*}
 \hat{\delta}(aw'v,q)
 &=\hat{\delta}(w'v,\delta(a,q)) & \because \hat{\delta}の定義\\
 &=\hat{\delta}(v,\hat{\delta}(w',\delta(a,q))) & \because 帰納法の仮定\\
 &=\hat{\delta}(v,\hat{\delta}(aw',q)) & \because \hat{\delta}の定義
\end{align*}

以上より題意は示された．
\\

\noindent
{\bf 問12.1}(p.~155) 直前の約束が無くてもそれぞれの約束に対応する構文構造が一意に定まるようにすればよい．具体的には，$\lambda x.M$, $M~M$, $M[1]$, $M[2]$の周りに括弧を付けると良い．
\\

\noindent
{\bf 問12.2}(p.~157)
\begin{align*}
 [N/x]c &= c\\
 [N/x](M_1,M_2) &= ([N/x]M_1,[N/x]M_2)\\
 [N/x](M[1]) &= ([N/x]M)[1]\\
 [N/x](M[2]) &= ([N/x]M)[2]\\
 [N/x](1(M)) &= 1([N/x]M)\\
 [N/x](2(M)) &= 2([N/x]M)\\
 [N/x](\mathbf{fix}(M)) &= \mathbf{fix}([N/x](M))
\end{align*}
\\

\noindent
{\bf 問12.3}(p.~157)
\begin{align*}
[N/x](\mathbf{let}~y=M_1~\mathbf{in}~M_2) =
 \begin{cases}
  \mathbf{let}~y=[N/x]M_1~\mathbf{in}~M_2 &(x = y)\\
  \mathbf{let}~y=[N/x]M_1~\mathbf{in}~[N/x]M_2 &(x\neq y, y \not\in \mathit{FV}(N))\\
  \mathbf{let}~z=[N/x]M_1~\mathbf{in}~[N/x]([z/y]M_2) &(x\neq y, z \neq x, y \in \mathit{FV}(N) かつ\\
                                               &~z \not\in \mathit{FV}(M_2),z \not\in \mathit{FV}(N))
 \end{cases}
\end{align*}
以下は最も一般的な場合のみを示す:
\begin{multline*}
 [N/x](\mathbf{case}~M~\mathbf{of}~1(y_1)\Rightarrow M_1, 2(y_2)\Rightarrow M_2) =\\
\mathbf{case}~[N/x]M~\mathbf{of}~1(z_1)\Rightarrow [N/x]([z_1/y_1]M_1), 2(z_2)\Rightarrow [N/x]([z_2/y_2]M_2)\\
(x\neq y_i,z_i\neq x,y_i\in\mathit{FV(N)},z_i\not\in\mathit{FV}(M_1)\cup\mathit{FV}(M_2) \cup \mathit{FV}(N))
\end{multline*}
\\

\noindent
{\bf 問12.6}(p.~159) 無理数$a,b$が与えられたとき$a^b$は無理数と仮定する．$\sqrt{2}$は無理数であるので，仮定より$\sqrt{2}^{\sqrt{2}}$は無理数である．しかし，$a=\sqrt{2}^{\sqrt{2}}$, $b=\sqrt{2}$と仮定すると$a^b$は，$2$であり無理数ではない．よって矛盾．背理法により題意は示された．
\\

\noindent
{\bf 問12.7}(p.~162)~ $\mathcal{N}\vdash\Delta\rhd A$なら$\Delta\models A$であることを，命題論理式$A$の構造に関する帰納法で示す．

$A=a$の場合．$\mathcal{N}\vdash\Delta\rhd A$である．つまり，$\Delta\rhd a$ が$\mathcal{N}$によって証明可能である． $\mathcal{N}$の規則のうち，$\Delta\rhd a$に合致する結論を持ち得るのは規則(Ax)のみである．したがって，$a\in \mathit{Ax}$である．
$a\in \Delta$より，任意の$\eta$について$\sem{a}\eta = \mathit{true}$である．すなわち，$\Delta \models a$ である．

$A=\alpha$の場合．規則(taut)によって$\alpha \in \Delta$である．したがって，$\Delta \models \alpha$ である．

$A=X\supset Y$の場合．規則($\supset$:I)より$\Delta\cup X \rhd Y$である．これと帰納法の仮定より$\Delta\cup X \models Y$，すなわち
\[
(\forall Z \in \Delta \cup X.~\sem{Z}\eta = \mathit{true}) ~\mbox{ならば}~ \sem{Y}\eta = \mathit{true}
\]
である．したがって，
\[
(\forall Z \in \Delta.~\sem{Z}\eta = \mathit{true}) ~\mbox{ならば}~ (\sem{X}\eta = \mathit{false} ~\mbox{または}~ \sem{Y}\eta = \mathit{true})
\]
であり，すなわち
\[
(\forall Z \in \Delta.~\sem{Z}\eta = \mathit{true}) ~\mbox{ならば}~ \sem{X\supset Y}\eta = \mathit{true}
\]
である．よって，$\Delta \models X\supset Y$ である．

$A=X \wedge Y$の場合と$A=X \vee Y$の場合は，$A=X\supset Y$の場合と同様にして帰納法の仮定を用いて証明できる．
\\

\noindent
{\bf 問12.8}(p.~162)~排中律が例の１つである：$A\vee (A \supset \bot)$
\\

\noindent
{\bf 問14.1}(p.~201)~ヒルベルトシステムの公理$A$は，任意の$\eta$に対して$\sem{A}\eta=\mathit{true}$となる．よって，$Ax$のメンバーである非論理的公理以外のヒルベルトシステムの公理は，すべて恒真式である．

$\mathcal{H}\vdash\Delta\rhd A$の場合，$A$はヒルベルトシステムの公理のインスタンスである．ヒルベルトシステムの公理は恒真式である．したがって，$\Delta\models A$である．
\\

\noindent
{\bf 問14.2}(p.~203)~
(i) 自然演算証明システム$\mathcal{N}$(p.~162)で以下のように証明される．
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \rhd A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd A\supset A$}
\end{prooftree}
ヒルベルトシステム$\mathcal{H}$(p.~200)ではp.~201の$B\equiv A$の場合の証明木が構成できる．

(ii) 自然演算証明システム$\mathcal{N}$(p.~162)で以下のように証明される．
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \cup B \rhd A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$A \rhd B \supset A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd A \supset B \supset A$}
\end{prooftree}
ヒルベルトシステム$\mathcal{H}$(p.~200)では公理(K)そのものである．

(iii) 自然演算証明システム$\mathcal{N}$(p.~162)で以下のように証明される．
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \wedge B \rhd A \wedge B$}
\RightLabel{($\wedge$:E1)}
\UnaryInfC{$A \wedge B \rhd A$}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \wedge B \rhd A \wedge B$}
\RightLabel{($\wedge$:E2)}
\UnaryInfC{$A \wedge B \rhd B$}
\RightLabel{($\wedge$:I)}
\BinaryInfC{$A \wedge B \rhd B \wedge A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd A \wedge B \supset B \wedge A$}
\end{prooftree}
ヒルベルトシステム$\mathcal{H}$(p.~200)では以下のように証明される．(MP=Modus Ponens)
\begin{prooftree}
\AxiomC{}
\RightLabel{(F)}
\UnaryInfC{$A \wedge B \rhd A \wedge B \supset A$}
\AxiomC{}
\RightLabel{(i)}
\UnaryInfC{$A \wedge B \rhd A \wedge B$}
\RightLabel{($\wedge$:E1)}
\BinaryInfC{$A \wedge B \rhd A$}
\AxiomC{}
\RightLabel{(P)}
\UnaryInfC{$A \wedge B \rhd B \supset A \supset B \wedge A$}
\RightLabel{(MP)}
\UnaryInfC{$A \wedge B \rhd A \supset B \wedge A$}
\RightLabel{(MP)}
\BinaryInfC{$A \wedge B \rhd B \wedge A$}
\RightLabel{(定理14.1(演繹定理))}
\UnaryInfC{$\rhd A \wedge B \supset B \wedge A$}
\end{prooftree}

(iv) 自然演算証明システム$\mathcal{N}$(p.~162)で以下のように証明される．
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \vee B \rhd A \vee B$}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \vee B \cup A \rhd A$}
\RightLabel{($\vee$:I2)}
\UnaryInfC{$A \vee B \cup A \rhd B \vee A$}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \vee B \cup B \rhd B$}
\RightLabel{($\vee$:I1)}
\UnaryInfC{$A \vee B \cup B \rhd B \vee A$}
\RightLabel{($\vee$:I)}
\TrinaryInfC{$A \vee B \rhd B \vee A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd A \vee B \supset B \vee A$}
\end{prooftree}
ヒルベルトシステム$\mathcal{H}$(p.~200)では以下のように証明される．(MP=Modus Ponens)
\begin{prooftree}
\AxiomC{}
\RightLabel{(A)}
\UnaryInfC{$A \vee B \rhd A \vee B \supset (A \supset B\vee A) \supset (B\supset B\vee A) \supset B \vee A$}
\AxiomC{}
\RightLabel{(i)}
\UnaryInfC{$A \vee B \rhd A \vee B$}
\LeftLabel{$\Pi\equiv$}
\RightLabel{(MP)}
\BinaryInfC{$A \vee B \rhd (A \supset B\vee A) \supset (B\supset B\vee A) \supset B \vee A$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Pi$}
\AxiomC{}
\RightLabel{(i)}
\UnaryInfC{$A \vee B \rhd A \vee B$}
\RightLabel{(R)}
\UnaryInfC{$A \vee B \rhd A \supset B \vee A$}
\RightLabel{(MP)}
\BinaryInfC{$A \vee B \rhd (B\supset B\vee A) \supset B \vee A$}
\AxiomC{}
\RightLabel{(L)}
\UnaryInfC{$A \vee B \rhd B \supset B \vee A$}
\RightLabel{(MP)}
\BinaryInfC{$A \vee B \rhd  B \vee A$}
\RightLabel{(定理14.1(演繹定理))}
\UnaryInfC{$\rhd A \vee B \supset B \vee A$}
\end{prooftree}
~\\

\noindent
{\bf 問14.3}(p.~204)~
(K) 自然演繹システム$\mathcal{N}$で以下のように証明される．
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \cup B \rhd A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$A \rhd B \supset A$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd A \supset B \supset A$}
\end{prooftree}
p.~164のラムダ計算の方導出システムを参考にしてラムダ式を求める．(taut)は(var), ($\supset$:I)は(abs)に対応することから，ラムダ式$\lambda x_A.\lambda x_B.x_A$が求まる．

(S)
\begin{prooftree}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \supset B \supset C \cup A \supset B \cup A \rhd A$}
\AxiomC{}
\RightLabel{(taut)}
\UnaryInfC{$A \supset B \supset C \cup A \supset B \cup A \rhd A \supset B \supset C$}
\LeftLabel{$\Pi\equiv$}
\RightLabel{($\supset$:E)}
\BinaryInfC{$A \supset B \supset C \cup A \supset B \cup A \rhd B \supset C$}
\end{prooftree}
\begin{prooftree}
\AxiomC{}
\AxiomC{}
\RightLabel{($\supset$:E)}
\BinaryInfC{$A \supset B \supset C \cup A \supset B \cup A \rhd B$}
\AxiomC{$\Pi$}
\RightLabel{($\supset$:E)}
\BinaryInfC{$A \supset B \supset C \cup A \supset B \cup A \rhd C$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$A \supset B \supset C \cup A \supset B \rhd A \supset C$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$A \supset B \supset C \rhd (A \supset B) \supset A \supset C$}
\RightLabel{($\supset$:I)}
\UnaryInfC{$\rhd (A \supset B \supset C) \supset (A \supset B) \supset A \supset C$}
\end{prooftree}

以下，省略．
\\

\noindent
{\bf 問14.4}(p.~205)~p.~172のラムダ式の文脈を参考にして，コンビネータ理論における式の文脈を次のように定義する．
\[
 D ::= \left[\:\right] ~|~ C~D ~|~ D~C
\]
ここで$\left[\:\right]$はコンビネータ理論の式が埋め込まれるべき穴を表す．文脈$D$の穴にコンビネータ理論の式$C$を埋め込んで得られる式を$D[C]$と書く．$1$ステップ簡約関係を，この文脈を使い，以下のように定義する．
\begin{prooftree}
\AxiomC{$C \Longrightarrow C'$}
\UnaryInfC{$D[C] \longrightarrow D[C']$}
\end{prooftree}
ここで$C \Longrightarrow C'$は図14.3のコンビネータの簡約関係である．この$1$ステップ簡約関係の反射的推移的閉包が$C \xrightarrow{~*~} C'$である．
\\

\noindent
{\bf 問14.5}(p.~205)~以下のことより示される．
\begin{itemize}
 \item 図14.3の簡約公理の適用前後で型が同じ．
 \item 簡約公理の適用回数の帰納法．
 \item (app)がModus Ponensに対応．
\end{itemize}
~\\

\noindent
{\bf 問14.6}(p.~206)~$C$の構造に関する帰納法を用いる．

$x\not\in \mathit{FV}(C)$の場合を考える．$\mathcal{C}\vdash \Gamma\{x:\tau_1\}\rhd C : \tau_2$の変数の型環境から$x:\tau_1$を取り除いた$\mathcal{C}\vdash \Gamma\rhd C : \tau_2$も成り立つ．したがってある証明$\Pi$が存在して以下の証明が存在する．
\begin{prooftree}
\AxiomC{}
\RightLabel{(図14.2)}
\UnaryInfC{$\Gamma\rhd \mathbf{K} : \tau_2\to\tau_1\to\tau_2$}
\AxiomC{$\Pi$}
\UnaryInfC{$\Gamma\rhd C : \tau_2$}
\RightLabel{(app)}
\BinaryInfC{$\Gamma\rhd \mathbf{K}~C : \tau_1\to\tau_2$}
\end{prooftree}
したがって，$\lambda^*x.C$の定義より$\Gamma\rhd \lambda^*x.C : \tau_1\to\tau_2$である．

$C=x$の場合を考える．
任意の$\tau$について，
図14.2の(var)より$\Gamma\{x:\tau\}\rhd x : \tau$が成り立ち，
また$\Gamma\rhd \mathbf{S}\mathbf{K}\mathbf{K} : \tau \to \tau$が成り立ち，
したがって，$\lambda^*x.C$の定義より$\Gamma\rhd \lambda^*x.x : \tau \to \tau$が成り立つ．

$C=C_1C_2$の場合を考える．
$\mathcal{C}\vdash \Gamma \{x:\tau_1\}\rhd C_1C_2:\tau_3$と仮定する．
$\mathcal{C}\vdash \Gamma \{x:\tau_1\}\rhd C_1:\tau_2\to\tau_3$かつ
$\mathcal{C}\vdash \Gamma \{x:\tau_1\}\rhd C_2:\tau_2$であるような$\tau_2$が存在する．
帰納法の仮定より
$\mathcal{C}\vdash \Gamma \rhd \lambda^*x.C_1:\tau_1\to\tau_2\to\tau_3$かつ
$\mathcal{C}\vdash \Gamma \rhd \lambda^*x.C_2:\tau_1\to\tau_2$である．
したがって，$\mathcal{C}\vdash \Gamma \rhd \mathbf{S}(\lambda^*x.C_1)(\lambda^*x.C_2):\tau_1\to\tau_3$を根とする証明木が存在する．したがって，$\lambda^*x.C$の定義より$\Gamma\rhd \lambda^*x.C_1C_2 : \tau \to \tau$が成り立つ．
\\

\noindent
{\bf 問14.7}(p.~208)~
\begin{align*}
 \overline{(\lambda x.x)\lambda x.x}
&= \mathbf{S}\mathbf{K}\mathbf{K}(\mathbf{S}\mathbf{K}\mathbf{K})\\
&\xrightarrow{~*~} \mathbf{S}\mathbf{K}\mathbf{K}\\
\end{align*}
\begin{align*}
 \overline{(\lambda x.(x,x))~1}
&= \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{P})(\mathbf{S}\mathbf{K}\mathbf{K}))(\mathbf{S}\mathbf{K}\mathbf{K})1\\
&\xrightarrow{~*~} \mathbf{P}~1~1
\end{align*}
~\\

\noindent
{\bf 問14.8}(p.~208)~
p.~164, p.~205, p.~207を参照．

(inj1)の場合．
ある$M_1$, $\tau_1$, $\tau_2$があって，$\tau = \tau_1 + \tau_2$, $M\equiv 1(M_1)$, かつ$\Lambda \vdash \Gamma \rhd M_1 : \tau_1$である．
帰納法の仮定より$\mathcal{C} \vdash \Gamma \rhd \overline{M_1} : \tau_1$である．
規則(app)を使用すると，$\mathcal{C} \vdash \Gamma \rhd \mathbf{L}~\overline{M_1} : \tau_1 + \tau_2$を得る．
一方，$\overline{1(M_1)} \equiv \mathbf{L}~\overline{M_1}$である．
(inj2)の場合も同様に示せる．

(case)の場合．
ある$M'$, $\tau_1$, $\tau_2$があって，$\Lambda \vdash \Gamma \rhd M' : \tau_1+\tau_2$, $\Lambda \vdash \Gamma\{x_1:\tau_1\} \rhd M_1 : \tau$, $\Lambda \vdash \Gamma\{x_2:\tau_2\} \rhd M_2 : \tau$である．
帰納法の仮定より，$\mathcal{C} \vdash \Gamma \rhd \overline{M'} : \tau_1+\tau_2$, $\mathcal{C} \vdash \Gamma\{x_1:\tau_1\} \rhd \overline{M_1} : \tau$, $\mathcal{C} \vdash \Gamma\{x_2:\tau_2\} \rhd \overline{M_2} : \tau$である．
後ろの2つと定理14.3より$\mathcal{C} \vdash \Gamma \rhd \lambda^*x_1.\overline{M_1} : \tau_1\to\tau$, $\mathcal{C} \vdash \Gamma \rhd \lambda^*x_2.\overline{M_2} : \tau_2\to\tau$を得る．
規則(app)を3回使用すると$\mathcal{C} \vdash \Gamma \rhd \mathbf{A}~\overline{M'}~(\lambda^*x_1.\overline{M_1})~(\lambda^*x_2.\overline{M_2}):\tau$を得る．
一方，$\overline{\mathbf{case}~M'~\mathbf{of}~1(x_1)\Rightarrow M_1, 2(x_2)\Rightarrow M_2} \equiv \mathbf{A}~\overline{M'}~(\lambda^*x_1.\overline{M_1})~(\lambda^*x_2.\overline{M_2})$である．

(fix)の場合．．．．

(let)の場合．．．．
\\

\noindent
{\bf 問14.9}(p.~209)~図12.5のラムダ式をコンビネータ式に書き換えたものに(ext)規則を加えて得られる．
~\\

\noindent
{\bf 問14.12}(p.~211)~
$i=1,2$に対して，$x\neq y_i,y_i\in\mathit{FV(M_1)}$と仮定し，
$z_i\neq x,z_i\not\in\mathit{FV}(M_1)\cup\mathit{FV}(M_2^2)\cup\mathit{FV}(M_2^3)$となるような$z_i$を考える．そうでない場合は，$y_1$, $y_2$をフレッシュな変数に置き換えてこの条件を満たすようにする．このような仮定を置いても一般性を失わない．
\begin{align*}
& \mathit{CL}^\mathit{ext}\vdash \overline{[M_1/x] M_2}\\
& \quad =~ \overline{[M_1/x](\mathbf{case}~M_2^1~\mathbf{of}~1(y_1)\Rightarrow M_2^2, 2(y_2)\Rightarrow M_2^3)} & (\because 仮定)\\
& \quad =~ \overline{\mathbf{case}~[M_1/x]M_2^1~\mathbf{of}~1(z_1)\Rightarrow [M_1/x][z_1/y_1]M_2^2, 2(z_2)\Rightarrow [M_1/x][z_2/y_2]M_2^3} & (\because \mbox{p.~157~問12.3})\\
& \quad =~ \mathbf{A}~(\overline{[M_1/x]M_2^1})~(\lambda^*z_1.\overline{[M_1/x][z_1/y_1]M_2^2})~ (\lambda^*z_2.\overline{[M_1/x][z_2/y_2]M_2^3}) & (\because \mbox{p.~207} ~\overline{M})\\
& \quad =~ \mathbf{A}~([\overline{M_1}/x]\overline{M_2^1})~(\lambda^*z_1.[\overline{M_1}/x]\overline{[z_1/y_1]M_2^2})~ (\lambda^*z_2.[\overline{M_1}/x]\overline{[z_2/y_2]M_2^3}) & (\because 帰納法の仮定)\\
% & \quad =~ \mathbf{A}~([\overline{M_1}/x]\overline{M_2^1})~(\lambda^*z_1.[\overline{M_1}/x][z_1/y_1]\overline{M_2^2})~ (\lambda^*z_2.[\overline{M_1}/x][z_2/y_2]\overline{M_2^3}) & (\because \mbox{p.~210, 1番目の場合})\\
& \quad =~ [\overline{M_1}/x](\mathbf{A}~\overline{M_2^1}~(\lambda^*z_1.\overline{[z_1/y_1]M_2^2})~ (\lambda^*z_2.\overline{[z_2/y_2]M_2^3})) & (\because \mbox{p.~157, 代入の定義})\\
& \quad =~ [\overline{M_1}/x](\overline{\mathbf{case}~M_2^1~\mathbf{of}~1(z_1)\Rightarrow [z_1/y_1]M_2^2, ~2(z_2)\Rightarrow[z_2/y_2]M_2^3}) & (\because \mbox{p.~207} ~\overline{M})\\
& \quad =~ [\overline{M_1}/x](\overline{\mathbf{case}~M_2^1~\mathbf{of}~1(y_1)\Rightarrow M_2^2, ~2(y_2)\Rightarrow M_2^3}) & (z_i\not\in \mathit{FV}(M_i))\\
& \quad =~ [\overline{M_1}/x]\overline{M_2} & (\because 仮定)\\
\end{align*}

残りの場合は，適用と同じようにして証明できる．
~\\

\noindent
{\bf 問14.17}(p.~218)
$c$, $x$の場合．値の型の定義から明らかである．

$M[1], M[2], 1(M), 2(M)$の場合．帰納法の仮定を単に使用すれば良い．

$(M_1,M_2)$の場合．
ラムダ計算の型導出システム(p.~164)の規則(prod)より，ある$\tau_1, \tau_2$があって，$\Gamma\rhd M_1:\tau_1$かつ$\Gamma\rhd M_2:\tau_2$である．
計算の定義より，ある$v_1, v_2$があって，$E \vdash M_1 \Downarrow v_1$かつ$E \vdash M_2 \Downarrow v_2$である．
これらと自然意味論の評価関係の規則により$E \vdash (M_1,M_2) \Downarrow (v_1,v_2)$であり，$v=(v_1,v_2)$である．
帰納法の仮定より$\models v_1:\tau_1$かつ$\models v_2:\tau_2$である．
値の型の定義より$\models v:\tau_1 \times \tau_2$である．

$\mathbf{case}~M'~\mathbf{of}~1(x_1)\Rightarrow M_1, 2(x_2)\Rightarrow M_2$の場合．
ラムダ計算の型導出システム(p.~164)の規則(case)より，ある$\tau_1, \tau_2$があって，$\Gamma\rhd M':\tau_1+\tau_2$, $\Gamma\{x_1:\tau_1\}\rhd M_1:\tau$, および$\Gamma\{x_2:\tau_2\}\rhd M_2:\tau$である．
計算の定義より，ある$v'$があって，$E \vdash M' \Downarrow v'$である．
帰納法の仮定より$\models v' : \tau_1 + \tau_2$である．
値の定義より$v'=1(v'')$もしくは$v'=2(v'')$である．
%
$v'=1(v'')$と仮定する．
計算の定義より$E\{x_1:v''\} \vdash M_1 \Downarrow v$である．
値の型の定義より，$\models v'' : \tau_1$であるので，$\models E\{x_1:v''\} : \Gamma\{x_1:\tau_1\}$である．
帰納法の仮定より，$\models v : \tau$である．
また，$v'=1(v'')$と仮定した場合は，$v'=1(v'')$の場合と同様にして示せる．

%$\mathbf{fix}(\lambda f.\lambda x.M')$
$\mu.f.x.M'$の場合．
$v=\mathit{rec}(E,\mu.f.x.M')$であり，$\Gamma \rhd \mu.f.x.M' : \tau$であり，よって値の型の定義によって要求される$\Gamma$をこの$\Gamma$ととれば$\models \mathit{rec}(E,\mu.f.x.M') : \tau$である．

(let?)
\end{document}