コンピュータサイエンス入門〜アルゴリズムとプログラミング言語〜 2020 年度 Q2 解答例と解説 (再配布しないで下さい)

2020 年 8 月 16 日

問 10.1(p. 137–138) p. 137 に以下のように関数の定義がある．

f が A から B への関数であるのは，任意の x ∈ A について (x, y) ∈ f となる y ∈ B があり，任意の x ∈ A, y ∈

B, z ∈ B について (x, y) ∈ f かつ (x, z) ∈ f なら y = z となるときである．

つまり，論理式で書くと， f が A から B への関数であるのは

(∀x ∈ A.∃y ∈ B. (x, y) ∈ f) ∧ (∀x ∈ A, y, z ∈ B. (x, y) ∈ f ∧ (x, z) ∈ f ⇒ y = z)

と同値である． R が関数であることから，

1. 任意の x について (x, z) ∈ R となる z ∈ A があり，

2. 任意の x, z, z′ ∈ A について (x, z) ∈ R かつ (x, z′) ∈ R なら z = z′ となる．

同様に， S が関数であることから，

3. 任意の z について (z, y) ∈ S となる y があり，

4. 任意の z, y, y′ ∈ A について (z, y) ∈ S かつ (z, y′) ∈ S なら z = z′ となる．

1 と 3 より，任意の x について (x, y) ∈ RS となる y がある．また， 2 と 4 より任意の x, y, y′ について (x, y) ∈ RS かつ (x, y′) ∈ RS なら y = y′ となる．したがって RS は関数である．

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

R^{∗} = ⋃{R^{n} | n ≥ 0}  (1)

R の反射的推移的閉包とは (1)R を含み， (2) 反射的かつ (3) 推移的な関係の中で (4) 最小のものである． R^{∗} が R の反射的推移的閉包であることを (1)–(4) を示すことで示す．

1. R^{∗} は R を含むこと，すなわち R^{∗} ⊇ R を示す： R^{∗} = ⋃{R^{n} | n ≥ 0} ⊇ R^{k} ⊇ R^{1} = R

2. R^{∗} が反射的であること，すなわち任意の x ∈ A に対して (x, x) ∈ R^{∗} であることを示す： R^{∗} ⊇ R^{0} = {(x, x) | x ∈ A} より明らか．

3. R^{∗} が推移性を満たすことを示す： (x, y), (y, z) ∈ R^{∗} とする． R^{∗} の定義よりある k_{1}, k_{2} が存在して， (x, y) ∈ R^{k_{1}} かつ (y, z) ∈ R^{k_{2}} である．ここで，関係には結合側が成り立つことから任意の非負整数 k_{1} と k_{2} に対して R^{k_{1}+k_{2}} = R^{k_{1}}R^{k_{2}} である．したがって， (x, z) ∈ R^{k_{1}+k_{2}} ⊆ R^{∗} である．

4. R′ を R を含み反射的かつ推移的な任意の関係とし R^{∗} ⊆ R′ を示す：任意の非負整数 n (≥ 0) に対して R^{n} ⊆ R′ を示せば十分である． n に関する帰納法で示す． n = 0 の場合を考える． R′ は反射的なので R^{0} ⊆ R′ である． n > 0 の場合を考える．帰納法の仮定より R^{n−1} ⊆ R′ である．また R′ が反射的な R を含む反射的かつ推移的な関係であることから R′R = R′ である．よって R^{n} = R^{n−1}R ⊆ R′R = R′ である．したがって R^{n} ⊆ R′ である．

練習問題問 11.1(p. 141) 次のうちから正しいものをすべて選べ．

1. C = A ∪ B のとき， C ⊇ A である．

2. C = A ∪ B のとき， C ∋ A である．

練習問題問 11.1(p. 141) 2 つの集合 A = {1, 2, 3}, B = {4, 5} に対して， AB を求めよ．解答例 AB = {14, 15, 24, 25, 34, 35}

問 11.1(p. 141) (i) ∅ = R^{0} ⊆ ⋃{R^{n} | n ≥ 0} = R.

(ii) {ϵ} ∈ R^{1} ⊆ ⋃{R^{n} | n ≥ 0} = R. (iii) すべての a ∈ Σ について， {a} ∈ {{b} | b ∈ Σ} ⊆ R^{1} ⊆ ⋃{R^{n} | n ≥ 0} = R. (iv) R ∈ R = {R^{n} | n ≥ 0} であることから，ある k が存在して R ∈ R^{k} である．よって， R^{∗} ∈ {S^{∗} | S ∈ R^{k}} ⊆

R^{k+1} ⊆ {R^{n} | n ≥ 0} = R である． (v) R_{1}, R_{2} ∈ R であることから，ある k が存在して R_{1}, R_{2} ∈ R^{k} である．よって，

R_{1}R_{2} ∈ {S_{1}S_{2} | S_{1} ∈ R^{k}, S_{2} ∈ R^{k}} ⊆ R^{k+1} ⊆ R  (2)
R_{1} ∪ R_{2} ∈ {S_{1} ∪ S_{2} | S_{1} ∈ R^{k}, S_{2} ∈ R^{k}} ⊆ R^{k+1} ⊆ R  (3)

である．ある集合 A が (i) から (v) までの性質：

(i) ∅ ∈ A (ii) {ϵ} ∈ A (iii) すべての a ∈ Σ について {a} ∈ A (iv) R ∈ A なら R^{∗} ∈ A である．

(v) R_{1}, R_{2} ∈ A なら R_{1}R_{2} ∈ A かつ R_{1} ∪ R_{2} ∈ A である．

を満たすものとする．任意の n について R^{n} ⊆ A であることを，任意の S ∈ R^{n} が S ∈ A であることを n に関する帰納法により示す． n = 0 の場合．前提が空であり成り立つ． n = k + 1 の場合．帰納法の仮定より，任意の S ∈ R^{k} が S ∈ A である．これと上の性質 (i) から (v) より漸化式の右辺

の和を構成するどの集合の要素でも A に属することがいえる．よって，任意の S ∈ R^{k+1} が S ∈ A である．以上より，任意の n について R^{n} ⊆ A であることが示された．（任意の n について R^{n} が離散集合であることから，） (i) から (v) までの性質を満たす任意の集合 A と任意の n について，

R^{n} ⊆ A であり，したがって， R = ⋃{R^{n} | n ≥ 0} ⊆ A である．この A の任意性により R は (i) から (v) を満たす最小の集合である．

練習問題問 11.2 以下は高校の数学 I[1, pp. 55–] の問である．問 62 A = {a, b, c} のとき， A の部分集合をすべて書け．全体集合 U の部分集合 A について， A に属さない U の要素全体の集合を， A の補集合といい，\overline{A} で表す．すなわち，

\overline{A} = \{x | x ∈ U, x ∉ A\}

問 63 U = {x | x は 10 以下の自然数} を全体集合とするとき，

A = {x | x ∈ U, x は 2 の倍数}
B = {x | x ∈ U, x は 3 の倍数}

に対して，次の集合を，要素を書き並べて表せ． (1) \overline{A} (2) A ∩ \overline{B} (3) \overline{A} ∪ B 問 64 \overline{A ∩ B} = \overline{A} ∪ \overline{A} が成り立つことを示せ．問 65 12 以下の自然数の集合を全体集合 U とする． U の部分集合

A = {x | x ∈ U, x は 2 の倍数}
B = {x | x ∈ U, x は 3 の倍数}

について，要素を書き並べて，ド・モルガンの法則が成り立つことを確かめよ．

問 11.2(p. 141) 性質 (i) の証明のヒント：数学的帰納法を用いる．性質 (iv) の証明のヒント：全体集合を Σ^{∗} として補集合を考えて，任意の集合 X (⊂ Σ^{∗}) がその補集合の補集合 Σ^{∗}\(Σ^{∗}\X) と等しいこととド・モルガンの法則を用いると良い．

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

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

性質 (iv) の証明． R_{1}, R_{2} が正規言語であることから，性質 (iii) より Σ^{∗}\R_{1} と Σ^{∗}\R_{2} が正規言語であり， p. 140 の性質 (v) より (Σ^{∗}\R_{1}) ∪ (Σ^{∗}\R_{2}) は正規言語である．よって

R_{1} ∩ R_{2} = Σ^{∗}\(Σ^{∗}\(R_{1} ∩ R_{2}))  ∵ R_{1} ∩ R_{2} ⊆ Σ^{∗}
= Σ^{∗}\((Σ^{∗}\R_{1}) ∪ (Σ^{∗}\R_{2}))  ∵ ド・モルガンの法則

も性質 (iii) より正規言語である．

問 11.3(p. 141) X = ⋃{R^{n}S | n ≥ 0} が解であり， ϵ ∉ R より唯一の解である． p. 140 の性質 (v) を用いた帰納法により X は正規言語であることが示される．

なお， ϵ ∈ R である場合は，任意の集合 X が X = S ∪ RX を満たす．

練習問題例 11.2(p. 142) −1234, 3.14, 1.09E20 が [[number]] の要素であることを示せ．解答例 −1234 ∈ [[number]] であるときのみを示す．他も同様である．

[[number]] = [[int]]

= [[sign digit^{+}]] = [[sign]] [[digit^{+}]] = [[+ | − | ϵ]] [[digit]]^{+} = ([[+]] ∪ [[−]] ∪ [[ϵ]]) (⋃{[[digit]]^{n} | n ≥ 1}) ⊃ [[−]] [[digit]]^{4} = {−} [[digit]] [[digit]]^{3} = ⋯ = {−} [[digit]] [[digit]] [[digit]] [[digit]] [[digit]]^{0} = {−} [[digit]] [[digit]] [[digit]] [[digit]] {ϵ} ⊃ {−} [[1]] [[2]] [[3]] [[4]] {ϵ} = {−1234} ∋ −1234

問 11.4(p. 146) w の長さに関する帰納法を用いる． w の長さが 0 の場合： δ̂ の定義から明らか． w の長さが 1 より大きい場合： w を aw′ とする．

δ̂(aw′v, q) = δ̂(w′v, δ(a, q))  ∵ δ̂の定義
= δ̂(v, δ̂(w′, δ(a, q)))  ∵ 帰納法の仮定
= δ̂(v, δ̂(aw′, q))  ∵ δ̂の定義

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

問 11.5(p. 146) ヒント：各状態において各終端記号による遷移を考えると良い．問 11.6(p. 147) 問 11.5 で作成した有限状態機械に対応する相互再帰関数を作成する．

f_{1}(x :: L) = f_{2}(L)  (x ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9})
f_{1}(x :: L) = f_{3}(L)  (x ∈ {+, −})
f_{1}(x :: L) = f_{8}(L)  (x ∈ {′.′,′ E′})
f_{1}(nil) = Reject
f_{2}(x :: L) = f_{2}(L)  (x ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9})
f_{2}(x :: L) = f_{8}(L)  (x ∈ {+, −})
f_{2}(′.′ :: L) = f_{4}(L)
f_{2}(′E′ :: L) = f_{5}(L)
f_{2}(nil) = Accept
f_{3}(x :: L) = f_{2}(L)  (x ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9})
f_{3}(x :: L) = f_{8}(L)  (x ∈ {′.′, +, −,′ E′})
f_{3}(nil) = Reject
⋮

練習問題問 11.7(pp. 150–151) BNF 文法

K ::= () | (K) | K K

で生成される構文木を OCaml のデータ型で表現せよ．解答例 BNF 記法は「文脈自由文法を簡潔に定義する記法」（p. 144）である．上記の BNF 文法は文脈自由文法 G_{1} = (T_{1}, N_{1}, K, P_{1}) を定義している．ここで，

N_{1} = {K}
T_{1} = {(,)}
P_{1} = {K → (), K → (K), K → K K)}

である．「各非終端記号 N をデータ型とみなし， N の各生成規則に対してデータ構成子を定義する」（p.150）ということにしたがって，非終端記号 K をデータ型とみなし，生成規則 K → () に対してデータ構成子 OneParen，生成規則 K → (K) に対してデータ構成子 Paren，生成規則 K → K K に対してデータ構成子 Apply をそれぞれ定義する．データ OneParen は， K をルートノードとし， “(”-木と “)”-木を子とする K-木を表す．データ Paren(t) は， K をルートノードとし， “(”- 木， t が表す K-木，および “)”-木を子とする K-木を表す．データ Apply(t1,t2) は， K をルートノードとし， t1 が表す K-木と t2 が表す K-木を子とする K-木を表す．

以上より求めるデータ型 k は以下の通りである．

type k = OneParen | Paren of k | Apply of k * k

（※ OCaml ではデータ型は英小文字で開始する必要がある．）練習問題問 11.7(pp. 150–151) 問 11.7 の BNF 文法における非終端記号をすべて記せ．解答例 PROGRAM と E の 2 つ．なお，タイプライターフォントで書かれたものはコードであることを明示しているものと思われる．練習問題問 11.7(pp. 150–151) 問 11.7 の BNF 文法における id と int をそれぞれ正規表現を用いて定義せよ．また， id と int はそれぞれ終端記号と非終端記号のいずれであるか．解答例 int には， p. 142 例 11.2 の定義を流用する．

sign = + | - | ϵ
digit = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
int = sign digit^{+}

id は先頭が英小文字， 2 文字目から英数字および_である 1 文字以上の文字列とする．

upper = A | ⋯ | Z
lower = a | ⋯ | z
alphanum = lower | upper | digit | _
id = lower alphanum^{∗}

p. 143 の終端記号の定義では，「通常のプログラミング言語では T の各要素は正規表現で定義される集合を表す」とあるので id と int は両方とも終端記号である．

問 11.7(pp. 150–151) 解答は別途示す． 2020 年度に受講者がはまった点：

• Windows で環境構築が難しい→ VirtualBox + Ubuntu を用いると良い

• OCaml のインストール方法が分からない． [2] のサポートページに記載の方法のうちバイナリパッケージをとってき

  てインストールする方法に失敗した．→公式ページの情報 https://ocaml.org/docs/install.html を参考にす

ると良い． VirtualBox + Ubuntu では apt でインストールのが簡単．

• OCaml インタプリタで日本語が文字化けをおこす． [2] のサポートページに記載の方法では文字化けが直らない．→ ホームディレクトリに以下を記述した .ocamlinit を置く．

  let print_non_escaped_string ppf = Format.fprintf ppf "\"%s\"";;
  #install_printer print_non_escaped_string;;

• ファイルマネージャ Nautilus からダブルクリックで *.ml ファイルを開けない→この方法で開く必要は無い（この方法で開きたい人は「ファイルの関連付け」を調べること）

• コマンド ocaml でコンパイルできない→コマンド ocamlc でコンパイルすること

• GNU Make の使い方が分からない→ [3] の 1 章だけでいいので読むこと．他の節は必要に応じて読むので良い．

• 最新の OCamlMakefile は http://mmottl.github.io/ocaml-makefile/ から手に入る（2020/08/12 現在）

• 与えられた BNF 文法にしたがったプログラムを評価する方法が分からない→この問題では評価器を作る必要は無い • ocamllex や ocamlyacc がよく分からない→まずはマニュアルを要チェック https://ocaml.jp/archive/

  ocaml-manual-3.06-ja/manual026.html

• 英単語： constructor: コンストラクタ，構成子; bind: 束縛; unbound: 束縛されていない

• L^{A}TEX の問題．パッケージのインストール方法が分からない→ tlmgr^{*1}を使うのが簡単である．まず以下を理解する

こと． – パッケージ管理ツール

– TeX Live

– ヘルプの使い方 tlmgr –help, man tlmgr 次に，以下のコマンドを理解した上で実行すること

*1 https://texwiki.texjp.org/?tlmgr

sudo tlmgr update --self --all
sudo tlmgr install listings

ただし， tlmgr を初めて使うときは以下のコマンドを実行する必要がある^{*2}．

sudo apt install xzdec
tlmgr init-usertree

• apt コマンドを使っていて「E: ロック /var/lib/dpkg/lock-frontend が取得できませんでした - open (11:

リソースが一時的に利用できません)」というエラーが出る→ https://qiita.com/tetsuo_jp/items/
9d4bbf415f3ec900b894

「Minimal でも十分プログラミング可能であるが， ML に興味のある読者は，巻末にいくつかあげる ML に関する参考文献を参照し， ML でプログラミングしてみることを勧める」とある．参考文献は [4, 5, 6, 7] である．しかし，本演習では Minimal や Standard ML ではなく OCaml でプログラミングしてみることを勧める．さらに参照する参考文献として [2] を勧める．

なお，文献 [4, 5] はオンラインで PDF を閲覧可能である． [4, 5, 6] は ML のテキストであり， [7] は OCaml の前身の Caml を使って書かれたアルゴリズムの教科書である．

問 12.1(p. 155) p. 154 の与えられたラムダ式の文法は以下の通りである：

M ::= c | x | λx.M | M M | (M, M) | M[1] | M[2]
| 1(M) | 2(M) | (case M of 1(x) ⇒ M, 2(x) ⇒ M)
| let x = M in M | fix(M)

まずは曖昧なラムダ式を考えてみよう：

• λx.M M は (λx.M) M と λx.(M M)

• M M[1] は M (M[1]) と (M M)[1]

• M M[2] は M (M[2]) と (M M)[2]

にそれぞれ解釈できる．

直前の約束 (i)–(iii) が無くてもそれぞれの約束に対応する構文構造が一意に定まるようにすればよい．具体的には， λx.M, M M, M[1], M[2] の周りに括弧を付けると良い．したがって，求める文法は以下の通りである：

M ::= c | x | (λx.M) | (M M) | (M, M) | (M[1]) | (M[2])
| 1(M) | 2(M) | (case M of 1(x) ⇒ M, 2(x) ⇒ M)
| let x = M in M | fix(M)

問 12.2(p. 157) 束縛変数を含まない他の 7 つの場合は以下の赤字の部分である：

M ::= c | x | λx.M | M M | (M, M) | M[1] | M[2]
| 1(M) | 2(M) | (case M of 1(x) ⇒ M, 2(x) ⇒ M)
| let x = M in M | fix(M)

*2 https://texwiki.texjp.org/?Linux%2FLinux%20Mint

これらの場合の代入の定義は以下の通りである：

[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](fix(M)) = fix([N/x](M))

問 12.3(p. 157) 場合分け構文と値の束縛構文は以下の赤字の部分である：

M ::= c | x | λx.M | M M | (M, M) | M[1] | M[2]

| 1(M) | 2(M) | (case M of 1(x) ⇒ M, 2(x) ⇒ M) | let x = M in M | fix(M)

場合分け構文に対する，最も一般的な場合の規則のみを示す:

[N/x](case M of 1(y_{1}) ⇒ M_{1}, 2(y_{2}) ⇒ M_{2}) =

case [N/x]M of 1(z_{1}) ⇒ [N/x]([z_{1}/y_{1}]M_{1}), 2(z_{2}) ⇒ [N/x]([z_{2}/y_{2}]M_{2}) (x ≠ y_{i}, z_{i} ≠ x, y_{i} ∈ FV (N ), z_{i} ∉ FV (M_{1}) ∪ FV (M_{2}) ∪ FV (N))

値の束縛構文に対する規則は以下の通りである：

[N/x](let y = M_{1} in M_{2}) = \begin{cases}let y = [N/x]M_{1} in M_{2} & (x = y) \\ let y = [N/x]M_{1} in [N/x]M_{2} & (x ≠ y, y ∉ FV (N)) \\ let z = [N/x]M_{1} in [N/x]([z/y]M_{2}) & (x ≠ y, z ≠ x, y ∈ FV (N) かつ \\ & z ∉ FV (M_{2}), z ∉ FV (N)) \end{cases}

問 12.4(p. 158) 場合分け構文に対する α 同値公理は次の通りである：

case M of 1(x_{1}) ⇒ M_{1}, 2(x_{2}) ⇒ M_{2} = case M of 1(y_{1}) ⇒ [y_{1}/x_{1}]M_{1}, 2(x_{2}) ⇒ M_{2}  (y_{1} ∉ FV (M_{1}))
case M of 1(x_{1}) ⇒ M_{1}, 2(x_{2}) ⇒ M_{2} = case M of 1(x_{1}) ⇒ M_{1}, 2(y_{2}) ⇒ [y_{2}/x_{2}]M_{2}  (y_{2} ∉ FV (M_{2}))

値の束縛構文に対する α 同値公理は次の通りである：

let x = M_{1} in M_{2} = let y = M_{1} in [y/x]M_{2}  (y ∉ FV (M_{1}) ∪ FV (M_{2}))

問 12.5(p. 158) 先に定義したラムダ式の代入では [λx.x y/z]λw.w z z のような代入を行うと λw.w (λx.x y) (λx.x y) となる．この結果のラムダ式は同じ束縛変数 x が 2 カ所で現れるので仮定 12.1 を満たさない．

関数適用に対する規則を以下のように変更する：

[N/x](M_{1} M_{2}) = [N/x]M_{1} [[y_{n}/x_{n}] ⋯ [y_{1}/x_{1}]N/x]M_{2}

(∀i. y_{i} ∉ FV ([N/x]M_{1}) ∪ BV ([N/x]M_{1}) ∪ FV (N) ∪ BV (N) ∪ FV (M_{2}) ∪ BV (M_{2}))

ここで y_{i} はフレッシュであることを意図している．ラムダ式の構造に関する帰納法によって仮定 12.1 を満たすことを示せる．問 12.6(p. 159) 命題 p 「a^{b} が有理数であるような無理数^{*3}a, b が存在する」の否定 ¬p は「任意の無理数 a, b に対して， a^{b} は有理数ではない」である．論理式で書くと p = ∃a, b ∈ ℝ/ℚ.a^{b} ∈ ℚ の否定 ¬p は ∀a, b ∈ ℝ/ℚ.a^{b} ∉ ℚ である．

背理法で p を示す． ¬p であることを仮定する．すなわち，無理数 a, b が与えられたとき a^{b} は無理数と仮定する．\sqrt{2} は無理数であるので，仮定より\sqrt{2}^{\sqrt{2}} は無理数である．しかし， a = \sqrt{2}^{\sqrt{2}}, b = \sqrt{2} と仮定すると a^{b} は， 2 であり無理数ではない．よって矛盾．背理法により題意は示された．

問 12.7(p. 162) N ⊢ Δ ▷ A なら Δ ⊧ A であることを，命題論理式 A の構造に関する帰納法で示す．

A = a の場合． N ⊢ Δ ▷ A である．つまり， Δ ▷ a が N によって証明可能である． N の規則（図 12.2）のうち， Δ ▷ a に合致する結論を持ち得るのは規則 (Ax) のみである．したがって， a ∈ Ax である． a ∈ Δ より，任意の η について [[a]]η = true である．すなわち， Δ ⊧ a である．

A = α の場合．規則 (taut) によって α ∈ Δ である．したがって， Δ ⊧ α である．

A = X ⊃ Y の場合．規則 (⊃:I) より Δ ∪ X ▷ Y である．これと帰納法の仮定より Δ ∪ X ⊧ Y ，すなわち

(∀Z ∈ Δ ∪ X. [[Z]]η = true) ならば [[Y]]η = true

である．したがって， (∀Z ∈ Δ. [[Z]]η = true) ならば ([[X]]η = false または [[Y]]η = true)

であり，すなわち

(∀Z ∈ Δ. [[Z]]η = true) ならば [[X ⊃ Y]]η = true

である．よって， Δ ⊧ X ⊃ Y である． A = X ∧ Y の場合と A = X ∨ Y の場合は， A = X ⊃ Y の場合と同様にして帰納法の仮定を用いて証明できる．

問 12.8(p. 162) 排中律が例の１つである： A ∨ (A ⊃ ⊥)

問 12.9(p. 166) 定理 12.2 は以下の通りである：

1. もし N ⊢ Δ ▷ A ならある M があって Λ ⊢ Γ_{Δ} ▷ M : τ_{A} である．

2. 逆に Λ ⊢ Γ_{Δ} ▷ M : τ_{A} なら N ⊢ Δ ▷ A_{τ} である．

1 を N ⊢ Δ ▷ A の導出に関する帰納法によって証明する． N ⊢ Δ ▷ A の導出の最後に使用された（図 12.2 の）推論規則により，場合分けを行う．

(taut) の場合． Δ ∪ A ▷ A であり，ある x と τ_{A} があって Γ_{Δ∪A} = Γ_{Δ}{x : τ_{A}} であり， (var) より Γ_{Δ∪A} ▷ x : τ_{A} である． (Ax) の場合． Δ ▷ a であり，命題定数 a に対応する定数を c_{a} : τ_{a} ∈ Const と仮定すると， (const) より Γ_{Δ} ▷ c_{a} : τ_{a} で

ある．

(⊃:I) の場合． Δ ▷ A ⊃ B かつ Δ ∪ A ▷ B である．帰納法の仮定より Δ ∪ A ▷ B ならある M があって Γ_{Δ∪A} ▷ M : τ_{B} である．したがって，ある x と τ_{A} があって Γ_{Δ∪A} = Γ_{Δ}{x : τ_{A}} であり， (abs) より Γ_{Δ} ▷ λx.M : τ_{A} → τ_{B} である．さらに，任意の A と B に対して， τ_{A⊃B} = τ_{A} → τ_{B} である．

(⊃:E) の場合． Δ ▷ B, Δ ▷ A ⊃ B, かつ Δ ▷ A である．帰納法の仮定より， Δ ▷ A ⊃ B ならある M_{1} があって Γ_{Δ} ▷ M_{1} : τ_{A⊃B} （すなわち， Γ_{Δ} ▷ M_{1} : τ_{A} → τ_{B}）であり， Δ ▷ A ならある M_{2} があって Γ_{Δ} ▷ M_{2} : τ_{A} である．このような M_{1} と M_{2} を仮定する． (app) より Γ_{Δ} ▷ M_{1} M_{2} : τ_{B} である．

【省略】以下同様にして，

• (∧:I) のとき (prod)

• (∧:E1) のとき (proj1)

• (∧:E2) のとき (proj2)

• (∨:I1) のとき (inj1)

*3 無理数とは，有理数ではない実数のこと．

• (∨:I2) のとき (inj2)

• (∨:E) のとき (case)

を使用して示せばよい．

2 も同様に示せる． p. 164 l.-9– にあるように，「規則 (fix) は，各 τ に対して型 (τ → τ) → τ をもつ定数 fix^{(τ→τ)→τ} の存在を仮定」していることと，規則 (let) は規則 (abs) と規則 (app) を組み合わせることで同じ型をもつ式を構成できることに注意．

問 12.10(p. 168) 以下のラムダ式の定義の λx.M 以外の場合を示せば良い．

M ::= c | x | λx.M | M M | (M, M) | M[1] | M[2]
| 1(M) | 2(M) | (case M of 1(x) ⇒ M, 2(x) ⇒ M)
| let x = M in M | fix(M)

c の場合．仮定より Γ ▷ c : τ かつ y ∉ dom(Γ) である．補題 12.5 より ∅ ▷ c : τ であり，さらに補題 12.4 より [y/x]Γ ▷ c : τ である．したがって， [y/x]Γ ▷ [y/x]c : τ である．

z の場合．仮定より Γ ▷ z : τ かつ y ∉ dom(Γ) である．補題 12.3 より， Γ ▷ z : τ であるので， z ∈ dom(Γ) である．したがって， z ≠ y である．よって，

Γ ▷ z : τ = Γ|x̄ ▷ z : τ  ∵ 補題 12.5
= Γ|x̄{y : Γ(x)} ▷ z : τ  ∵ 補題 12.4
= [y/x]Γ ▷ z : τ  ∵ p. 164 [y/x]Γ の定義
= [y/x]Γ ▷ [y/x]z : τ  ∵ z = [y/x]z

M M, (M, M), M[1], M[2], 1(M), 2(M), fix(M) の場合は帰納法の仮定を用いて簡単に示せる． (case M of 1(x) ⇒ M, 2(x) ⇒ M) と let x = M in M の場合は，束縛変数を λx.M の場合と同様に扱うことで示せる．【省略】

問 12.11(p. 169) x と λx. M 以外の残りの場合を示せば良い． c の場合．

Γ{x : τ_{1}} ▷ c : τ_{2} = Γ ▷ c : τ_{2}  ∵ 補題 12.5
= Γ ▷ [M_{2}/x]c : τ_{2}

M M, (M, M), M[1], M[2], 1(M), 2(M), fix(M) の場合は帰納法の仮定を用いて簡単に示せる． (case M of 1(x) ⇒ M, 2(x) ⇒ M) と let x = M in M の場合は，束縛変数を λx.M の場合と同様に扱うことで示せる．【省略】

問 12.12(p. 169) ラムダ式の構造に関する帰納法を用いる．命題 12.18 の証明． c の場合．

Γ ▷ λx. c : τ = Γ ▷ λy. [y/x]c : τ

x の場合．

Γ ▷ λx. x : τ = Γ ▷ λy. y : τ
= Γ ▷ λy. [y/x]x : τ

z (≠ x) の場合．

Γ ▷ λx. z : τ = Γ ▷ λy. [y/x]z : τ

λz.M の場合．帰納法の仮定より Γ ▷ λz.M : τ_{1} → τ_{2} かつ y ∉ FV (M) なら Γ ▷ λy.[y/z]M : τ_{1} → τ_{2} である．補題 12.7 を使う．【省略】命題 12.19 の証明． c の場合．自明． x の場合．自明． λz.M の場合．仮定より Γ▷λz.M : τ_{2} → τ_{1} かつ λz.M ≡ λz.N である． Γ▷λz.M : τ_{2} → τ_{1} が成り立つので，これが根に

ある導出木が存在する．図 12.3 より根の導出に用いられる規則は (abs) のみである．したがってその前提 Γ{z : τ_{2}}▷M : τ_{1} が成り立つ．帰納法の仮定（Γ′ ▷ M : τ_{1} かつ M ≡ N なら Γ′ ▷ N : τ_{1}）より， Γ{z : τ_{2}} ▷ N : τ_{1} である． (abs) より Γ ▷ λz.N : τ_{2} → τ_{1} である．

M_{1} M_{2} の場合．仮定より Γ ▷ M_{1} M_{2} : τ_{1} かつ M_{1} M_{2} ≡ N_{1} N_{2} である．式の構成法よりある τ_{2} が存在して Γ ▷ M_{1} : τ_{2} → τ_{1}, Γ ▷ M_{2} : τ_{2}, M_{1} ≡ N_{1}, および M_{2} ≡ N_{2} である．帰納法の仮定（Γ ▷ M_{1} : τ_{2} → τ_{1} かつ M_{1} ≡ N_{1} なら Γ ▷ N_{1} : τ_{2} → τ_{1} であり， Γ ▷ M_{2} : τ_{2} かつ M_{2} ≡ N_{2} なら Γ ▷ N_{2} : τ_{2} である．）より， Γ ▷ N_{1} : τ_{2} → τ_{1} かつ Γ ▷ N_{2} : τ_{2} である． (app) より， Γ ▷ N_{1} N_{2} : τ_{1} である．

【残りの場合は省略】

問 12.13(p. 170) p. 164 の図 12.3 を用いて導出木を作れば良い．型環境を次のように定める：

Γ = {mul : int × int → int}
Γ′ = Γ{x : int}
Γ′′ = Γ′{y : int}
Γ′′′ = Γ′′|x̄{x : int × int}

導出木 Π_{1} を次のように定める：

Γ′′′ ▷ mul : int × int → int

Γ′′′ ▷ x : int × int

(proj1)

Γ′′′ ▷ x[1] : int

Γ′′′ ▷ x : int × int

(proj2)

Γ′′′ ▷ x[2] : int

(prod)

Γ′′′ ▷ (x[1], x[2]) : int × int

(app)

Γ′′′ ▷ mul(x[1], x[2]) : int

(abs)

Γ′′ ▷ λx.mul(x[1], x[2]) : int × int → int

求める導出木は以下の通り：

Γ′′ ▷ x : int

Π_{1}

Γ′′ ▷ x : int  Γ′′ ▷ y : int

(prod)

Γ′′ ▷ (x, y) : int × int

(app)

Γ′′ ▷ (λx.mul(x[1], x[2]))(x, y) : int

(prod)

Γ′′ ▷ (x, (λx.mul(x[1], x[2]))(x, y)) : int × int

(abs)

Γ′ ▷ λy.(x, (λx.mul(x[1], x[2]))(x, y)) : int → int × int

(abs)

Γ ▷ λx.λy.(x, (λx.mul(x[1], x[2]))(x, y)) : int → int → int × int Γ ▷ 2 : int (prod)

Γ ▷ (λx.λy.(x, (λx.mul(x[1], x[2]))(x, y))) 2 : int → int × int Γ ▷ 3 : int

(prod)

Γ ▷ (λx.λy.(x, (λx.mul(x[1], x[2]))(x, y))) 2 3 : int × int

2 つ目の λx の内側に現れる x[1] と x[2] は型環境 Γ′′′ の中の x の型 int × int で型チェックされ，内側の λx の定義に対応した変数として扱われている．

問 12.14(p. 173) 定理 12.11 において N_{1} と N_{2} が正規形である場合を考えればよい．

M ⇓ N_{1} かつ M ⇓ N_{2} と仮定する．したがって， M ⟶^{∗} N_{1} かつ M ⟶^{∗} N_{2} である．定理 12.11 より， N_{1} ⟶^{∗} N_{3}, N_{2} ⟶^{∗} N_{4} かつ N_{3} ≡ N_{4} となる N_{3}, N_{4} が存在する． N_{1} と N_{2} が正規形であることから， N_{1} = N_{3} かつ N_{2} = N_{4} である^{*4}．したがって， N_{1} ≡ N_{2} である．

問 12.15(p. 178) η 簡約が含まれる反例を考えると良い．任意のモデル A について，

*4 ここでは N_{1} と N_{3}, N_{2} と N_{4} がそれぞれ完全に一致しているので “=” を用いた．なお， ≡ は α 同値性を表す記号である．

A[[Γ ▷ λx. inc x : int → int]]η = v ∈ A^{int}に A[[Γ{x : int} ▷ inc x : int]]η{x : v} を対応させる関数 = v ∈ A^{int}に A[[Γ{x : int} ▷ inc : int → int]]η{x : v}(A[[Γ{x : int} ▷ x : int]]η{x : v}) を対応させる関数 = v ∈ A^{int}に\overline{inc}(A[[Γ\{x : int\} ▷ x : int]]η\{x : v\}) を対応させる関数 = v ∈ A^{int}に\overline{inc}(v) を対応させる関数 = \overline{inc} A[[Γ ▷ inc : int → int]]η

である．したがって， ⊧ {inc : int → int} ▷ λx. inc x = inc : int → int

である．しかし， 2 つの異なるラムダ式 inc, λx. inc x は，図 12.4 のどの変形規則でも変形することができない．したがって

⊢ {inc : int → int} ▷ λx. inc x = inc : int → int

ではない．

問 12.16(p. 179) ヒントにあるとおりに， M の構造に関する帰納法を用いる． x の場合．型システムの定義より τ_{1} = τ_{2} である．両辺が A[[Γ ⊢ N : τ_{1}]]η になり成立する． y (y ≠ x) の場合．両辺が η(y) となり成立する． λy.M_{0} の場合． §12.2 で説明した束縛変数に関する約束を仮定する．自明．【省略】

問 12.17(p. 179)

(fst) の場合． Λ ⊢ Γ ▷ (M_{1}, M_{2})[1] : τ_{1} と仮定する．型システムの定義よりある τ_{2} が存在して， Λ ⊢ Γ ▷ (M_{1}, M_{2}) : τ_{1} × τ_{2} であり， Λ ⊢ Γ ▷ M_{1} : τ_{1} かつ Λ ⊢ Γ ▷ M_{2} : τ_{2} である． η を Γ を満たす任意の A 環境とする．以下の等式が成り立つ．

A[[Γ ▷ (M_{1}, M_{2})[1] : τ_{1}]]η

= Proj _{1}^{τ_{1},τ_{2}}(A[[Γ ▷ (M_{1}, M_{2}) : τ_{1} × τ_{2}]]η)  ∵ p. 177 図 12.6 l.8
= Proj _{1}^{τ_{1},τ_{2}}(Prod^{τ_{1},τ_{2}}(A[[Γ ▷ M_{1} : τ_{1}]]η, A[[Γ ▷ M_{2} : τ_{2}]]η))  ∵ p. 177 図 12.6 l.6–7
= A[[Γ ▷ M_{1} : τ_{1}]]η  ∵ p. 175 (ii)

以上より， ⊧ Γ ▷ (M_{1}, M_{2})[1] = M_{1} : τ_{1} が成り立つ．【省略】

問 12.18(p. 181) (i) 補題 12.16(i) を示す． Γ▷(λx.M) N : τ と仮定する．これを根とする導出木が存在するので， p. 164 図 12.3 の (app) と (abs) よりある τ_{1} が存在して Γ{x : τ_{1}}▷M : τ と Γ▷N : τ_{1} である．補題 12.7(p. 168) より Γ▷[N/x]M : τ である．

【省略】 (ii) 簡約関係の回数に関する帰納法で示すと良い．

問 12.19(p. 182) M_{2} の型付けに失敗する場合がある． Λ ⊢ ∅ ▷ 3 : int かつ (λx.3) (1 2) ⟶^{∗} 3 であっても Λ ⊢ ∅ ▷ (λx.3) (1 2) : int とならない． Λ ⊢ ∅ ▷ 3 : int かつ (3, x)[1] ⟶^{∗} 1 であっても Λ ⊢ ∅ ▷ (3, x)[1] : int とならない．図 12.3(p. 164) の型導出システムでは型

を導出することができないからである．

（構文論的性質）すべての変数と定数に型を注釈として付記する．関数適用などでは型が整合していないと正しいラムダ式では無いものとする．（cf. 単純型付けラムダ式）

問 12.20(p. 183) (fst) に対応する証明の簡略変換は

\begin{matrix}Π_{1} \\ (Δ ▷ A) \end{matrix}  \begin{matrix}Π_{2} \\ (Δ ▷ B) \end{matrix} (∧:I) Δ ▷ A ∧ B (∧:E1) Δ ▷ A

から

\begin{matrix}Π_{1} \\ (Δ ▷ A) \end{matrix}

への変換である． (snd) に対応する証明の簡略変換は

\begin{matrix}Π_{1} \\ (Δ ▷ A) \end{matrix}  \begin{matrix}Π_{2} \\ (Δ ▷ B) \end{matrix} (∧:I) Δ ▷ A ∧ B (∧:E2) Δ ▷ B

から

\begin{matrix}Π_{2} \\ (Δ ▷ B) \end{matrix}

への変換である． (case1) に対応する証明の簡略変換は

\begin{matrix}Π_{1} \\ (Δ ▷ A) \end{matrix} ; (∨:I1) ; Δ ▷ A ∨ B \begin{matrix}Π_{2} \\ (Δ ∪ A ▷ C) \end{matrix}  \begin{matrix}Π_{3} \\ (Δ ∪ B ▷ C) \end{matrix} (∨:E) Δ ▷ C

から

\begin{matrix}Π_{1} \\ (Δ ▷ A) \end{matrix}  \begin{matrix}Π_{2} \\ (Δ ∪ A ▷ C) \end{matrix} ; (⊃:I) ; Δ ▷ A ⊃ C (∨:E) Δ ▷ C

への変換である． (case2) に対応する証明の簡略変換は

\begin{matrix}Π_{1} \\ (Δ ▷ B) \end{matrix} ; (∨:I1) ; Δ ▷ A ∨ B \begin{matrix}Π_{2} \\ (Δ ∪ A ▷ C) \end{matrix}  \begin{matrix}Π_{3} \\ (Δ ∪ B ▷ C) \end{matrix} (∨:E) Δ ▷ C

から

\begin{matrix}Π_{1} \\ (Δ ▷ B) \end{matrix}  \begin{matrix}Π_{3} \\ (Δ ∪ B ▷ C) \end{matrix} ; (⊃:I) ; Δ ▷ B ⊃ C (∨:E) Δ ▷ C

への変換である．

参考文献

[1] 高橋陽一郎ほか：数学 I，啓林館 (2011).

[2] 浅井健一：プログラミングの基礎，サイエンス社 (2007). サポートページ： http://pllab.is.ocha.ac.jp/~asai/

   book/Top.html.

[3] RobertMecklenburg （著），矢吹道郎（監訳），菊池彰（訳）： GNU Make 第 3 版， O’Reilly (2005). Available from

   https://www.oreilly.co.jp/library/4873112699/.

[4] Milner, R., Tofte, M. and Harper, R.: The Definition of Standard ML (revised, MIT Press (1997). Available from

   https://smlfamily.github.io/.

[5] Paulson, L.C.: ML for the Working Programmer (2nd Ed.), Cambridge University Press (1996). Available from

   https://www.cl.cam.ac.uk/~lp15/MLbook/.

[6] Ullman, J.D.: Elements of ML Programming, Prentice-Hall, Inc. (1994). Supplemental materials available from

   http://infolab.stanford.edu/~ullman/emlp.html.

[7] Cousineau, G. and Mauny, M.: The Functional Approach to Programming, Cambridge University Press (1998).