TAPL演習の2.2.6を解いてみた。
【問題】
集合S上の関係Rを与え、関係R’を以下の様に定義する。
R' = R ∪ { (s,s) | S ∍s }
R'が反射的閉包であることを示せ。
---------------------------------------------
反射的閉包は定義2.2.1及び2.2.5より下記の条件を満たすものが反射的閉包である。
- Rを含む。
- { (s,s) | S ∍s }を含む。
- 上記1. 2.の条件に合致するもの内、最小の物が反射的閉包である。
- 定義2.2.1よりR∪{ (s,s) | S ∍s }は反射的関係である。（注 Rと (s,s) | S ∍s }を含んでいる。
- R'が最小の反射的関係である事を背理法により証明する。
R'が最小の反射的関係では無いと仮定すると、以下の式を満たすR''が存在する。
R'' ⊂ R'
差集合をD''(≠Φ)とする。
R' \ R'' = D''
前提よりR'=R ∪ { (s,s) | S ∍s }
従って、差分D''は Rまたは{ (s,s) | S ∍s }の要素である。
定義2.2.1よりR''はR又は{ (s,s) | S ∍s }を完全に含んでなく反射的関係では無い。
仮定R''は反射的関係であると矛盾する。
従って、R''なる物は無くR'が最小の反射的関係で、言い換えると反射的閉包と言える。
□ 証明終わり。
---------------------------------------------
TAPLに2章で出された演習問題の回答が無く、ネットをあさったが
気に入った回答が無かったので記載してみた。
ポイントは最小性を示すため差集合を使用した事かな。
R' = R ∪ { (s,s) | S ∍s }
良く見れば反射的閉包は明らかであるが、定義2.1.1に差集合の記載があり、証明にはこれを使えとの事と言っているように感じた。
＊＊昨日からTAPLをまじめに読み始めました。
相変わらずCoqの演習(SOFTWARE FOUNDATION)を行っております。
Logic.vまで進みましたが、実装の知識も有った方が良いのではと思うこと頻りにあり
TAPLとなった。以前6章まで目お通したが、演習は無視し頻発する証明も適当にななめ読みしていた。。汗）
数十年前の事だが、「エイホ、ウルマンのコンパイラ」（培風館版だぜ）と「シュライナー、フリードマンのCコンパイラ設計 yacc/lexの応用」読んだ後に、C言語でどんなアプリケーションも書けると感じられる様になった。
Cコードを書いているとasmコードも同時にイメージ出来る。俺の場合asmコードからCPU動作イメージ、さらにCPU周面を含めた動作イメージを感じる事が出来るので、C → Gateまで一気通貫で感じがつかめる。。汗)
gallina, Ocaml, haskellので 「エイホ、ウルマンのコンパイラ」に相当するのは、やはりTAPLでしょうか。気合を入れて読んでみます。
