型システム入門　第2章演習

会社で「型システム入門」の読書会を始めました。

型システム入門 −プログラミング言語と型の理論− Benjamin C. Pierce 住井 英二郎 オーム社 2013-03-26 売り上げランキング : 65013

まだ読み始めたばかりなのでとりあえず2章の数学的基礎を固めて、次回から3章に入っていく感じです。
練習がてら演習問題を解いたので、発表時資料兼ねてブログに残しておきます。
解答が省略されてる問題なので、完全に合ってるかは若干怪しいです。

演習問題の前に、一応定義の確認。
上の関係 に対し、
　 を含む最小の反射的関係 を の反射的閉包、
　 を含む最小の推移的関係 を の推移的閉包、
　 を含む最小の反射的推移的閉包 を の反射的推移的閉包
と呼びます。
ちょっと気をつけないといけないのは、反射的推移的閉包の定義が「反射的閉包かつ推移的閉包」ではないこと。
大抵の場合、反射的推移的閉包は反射的閉包でも推移的閉包でもありません。

例として上げると、

という関係 (要は、yはxよりちょうど1だけ大きい)を考えた時、

という関係 (yはxと等しいか、ちょうど1だけ大きい)が の反射的閉包、

$ R^+ = \{(x,y) | x, y \in {\bf N} \wedge x < y\}$ $= \{ (0,1), (0,2), (0,3), \ldots , (1,2), (1,3), \ldots \}$という関係 $ R^+$ (yはxより大きい)が $ R$ の推移的閉包、　$ R^* = \{(x,y) | x, y \in {\bf N} \wedge x \leq y\}$ $= \{ (0,0), (0,1), (0,2), \ldots , (1,1), (1,2), \ldots \}$という関係 $ R^*$ (yはx以上)が $ R$ の反射的推移的閉包になります。(WordPressで使ってる $ \LaTeX$ プラグインの都合上、eqnarrayが使えないっぽいのでイコールがずれてますがご了承ください)反射的閉包の定義は、反射的である「最小の」関係なので、 $ R'$ より大きい関係は $ R$ の反射的閉包ではありません。反射的推移的閉包である $ R^*$ には、 $ R'$ にはない $ (0,2)$ などが含まれているため、反射的閉包ではないわけです。同様に、 $ R^*$ には $ R^+$ にはない $ (0,0)$ などが含まれることから、推移的閉包でもありません。反射的閉包をベースに考えると、そこに推移的であるように要素を付け加えた時に、元の関係より大きくなってしまうので反射的閉包ではなくなってしまう、というイメージですね。なお、元から反射的かつ推移的な関係であれば、反射的推移的閉包と反射的閉包は等しくなります(そもそも全部元の関係と等しくなるので当然ですが)さて、話題が逸れたので演習問題2.2.6 - 2.2.8を解いていきます。まだ解いてない人のために、この下は展開仕様にしておきます。(追記：区切り位置を変えたため展開使用になっていません)演習2.2.6反射的閉包の構成に関する問題です。[解答]定義2.2.5より、 $ R'$ が $ R$ の反射的閉包であることを示すには、以下の3つの性質を満たすことを示せば良い。　(1) $ R \subseteq R'$　(2) $ \forall s \in {\bf S}. s\ R'\ s$　(3) $ \forall R''. R \subseteq R'' \wedge \forall s \in {\bf S}. s\ R''\ s \Rightarrow R' \subseteq R''$それぞれ(1)が「Rを含む」の部分、(2)が「反射的関係」の部分、(3)が「最小の関係」の部分を表している。(3)が少しややこしいが、定義2.2.5のカッコ書きの部分そのままである。なお、(2)と(3)では定義2.1.5の二項関係の略記法を用いている。(1)及び(2)は$ R'$の定義より自明である。よって(3)のみを背理法を用いて示す。　$ R \subseteq R'' \wedge \forall s \in {\bf S}. s\ R''\ s \wedge R' \not \subseteq R''$ (*)を満たす $ R''$ が存在すると仮定する。ここで $ R' \not \subseteq R''$ より、　$ (p,q) \in R' \wedge (p, q) \not \in R''$　(**)を満たす $ (p,q)$ が少なくとも一組存在する。ここで $ R'$ の定義より、　$ (p,q) \in R \vee (p,q) \in \{(s,s) | s \in {\bf S}\}$仮に $ (p,q) \in R$ とすると、$ R \not \subseteq R''$ となり(*)と矛盾する。また $ (p, q) \in \{(s,s) | s \in {\bf S}\}$ とすると、 $ \forall s \in {\bf S}. s\ R''\ s$ はこの $ (p, q)$ について満たされず、やはり(*)と矛盾する。これらのことから、(**)は満たされない。この矛盾は背理法の仮定より生じており、(*)を満たすような $ R''$ は存在しないことが証明された。これより(3)が証明された。(Q.E.D)思ったより文章量長い上、完全に忘れてた $ \LaTeX$ のコマンドを調べながらなので時間がかかる…演習2.2.7同様に推移的閉包の構成法に関する問題。[解答]2.2.6と同様、　(1) $ R \subseteq R^+$　(2) $ \forall s, t, u \in {\bf S}. s\ R^+\ t \wedge t\ R^+\ u \Rightarrow s\ R^+\ u$　(3) $ \forall R'. R \subseteq R' \wedge (\forall s, t, u \in {\bf S}. s\ R' \ t \wedge t\ R' \ u \Rightarrow s\ R' \ u) \Rightarrow R^+ \subseteq R'$を全て示せば良い。(2.2.7では $ R'$ を反射的閉包として用いたが、今回は別の意図で用いていることに注意)(1)は $ R_0 = R$ が $ R^+$ に含まれていることから自明である。(2)について、　$ s\ R^+\ t \wedge t\ R^+\ u$を満たすような任意の $ s, t, u$ を考える。この時、 $ R^+$ の定義から、　$ s\ R_n\ t$を満たす $ n$ が少なくともひとつ存在する。また同様に　$ t\ R_m\ u$を満たす $ m$ が少なくともひとつ存在する。ここで $ R_i$ の構成法より、 $ \forall n' \geq n. R_{n'} \supseteq R_n$ であることから $ n \geq m$ と仮定しても一般性を失わない。$ R_i$ の構成法より、 $ R_n \supseteq R_m$ であることから、　$ t\ R_n\ u$が成り立つ。これより、 $ s\ R_n\ t \wedge t\ R_n\ u$ となるので、　$ s\ R_{n+1}\ u$が成り立つ。これと $ R^+$ の定義より、　$ s\ R^+\ u$が成り立つことが示された。(3)について、背理法で示す。　$ R \subseteq R' \wedge (\forall s, t, u \in {\bf S}. s\ R' \ t \wedge t\ R' \ u \Rightarrow s\ R' \ u) \wedge R^+ \not \subseteq R'$ (*)を満たすような $ R'$ が存在すると仮定する。ここで $ R^+ \not \subseteq R'$ より、　$ (p,q) \in R^+ \wedge (p, q) \not \in R'$を満たす $ (p,q)$ が少なくとも一組存在する。これと$ R^+$ の定義より、　$ (p,q) \in R_n$を満たすような $ n$ が少なくともひとつ存在する。もし $ n = 0$ と仮定すると、$ (p,q) \in R$ となる。この場合、$ R \not \subseteq R'$ となり(*)と矛盾する。一方 $ n > 0$ と仮定した場合、 か となる。
前者の場合、同様の議論を について再帰的に適用することになる。
また後者についても、 を定めた際、 とすると(*)より となり矛盾することから、少なくともいずれか一方は　 に属さない。
この場合も同様の議論を について再帰的に適用することになる。
しかしながら、自然数 は有限であることから、再帰的に適用した場合必ず に到達する。
前述のとおりこの場合矛盾が生じる。この矛盾は背理法の仮定より生まれており、(*)を満たすような は存在しない。
これより、(3)が示された。
(1), (2), (3) が全て示されたことから、命題が示された。(Q.E.D)

(3)の証明が微妙に怪しいですね…
まだ降下列とか整礎が定義されてないので、このへんを使えないのが痛い。
もうちょいスマートな方法ないかな。

演習2.2.8

[解答]
は によって保存される述語であることから、
　 (*)
まず の反射性について考えると、
　
が成り立つことは自明である。
次に、推移性について考える。
　
と定義すると、 を満たす任意の は、 の推移性により
　
と表すことができる。
ここで の定義より を定めると、(*)より
　
　
　
　
となり、 を示すことができる。

以上より、反射性・推移性について が保存されることが示された。よって、
　
が示された。(Q.E.D)

これも怪しげですね…
反射的推移的閉包の明確な構成法が示されていないので、場合分けがやや中途半端な感じに。
前の演習2つと合わせて であることを証明して、その上で場合分けした方がまだ綺麗だったかもしれないですね。
読書会でもっとスタイリッシュな解法が見られることを期待しておきます…

ところで推移的閉包 は「関係Rを1回以上反復して適用する関係」、反射的推移的閉包 は「関係Rを0回以上反復して適用する関係」ということで表記に納得ができるのですが、反射的閉包は「関係Rを0回か1回適用する関係」なので と書いてもよさそうですが、この表記をすることってないんでしょうか…？
だと一般的すぎて反射的閉包っぽくないような。

気が向いたら読書会の進度に応じて3章以降の演習も逐次解いて上げようかと思います。