TaPL読書録 #1

2018年はmediumで記事を投稿しようと思っていたのですが、はてなブログのほうがなんだかんだ流入がいい気がしたので戻ってくることにしました。乗り換えのきっかけは、ブログのエディタの使い勝手があまりよくないことによっていたのですが、 kibela で書いてからコピペで貼ればいいや、という気持ちになって出戻りです。

mediumでは以下の3記事を書いていました。

『ふつうのLinuxプログラミング』 読了 – hkdnet – Medium

『白と黒のとびら』『精霊の箱』『自動人形の城』読了 – hkdnet – Medium

ある日 Entity Attribute Value に出会った – hkdnet – Medium

さて、今回の記事はTaPL読書録です。おそらくシリーズものになります。

型システム入門 −プログラミング言語と型の理論−

PFDS勉強会から派生してTaPL勉強会ができたのでそこでの疑問や得られた知識、派生して調べたことなどをまとめる予定です。¹なお、記載内容に誤りがあった場合、原因の多くは私の理解不足であろうことを先に いいわけ 謝罪しておきます。 第1回は1, 2章が対象でした。ざっくりまとめると、型にまつわる概略とプログラミング言語とのかかわりが1章、集合などの数学的な基礎知識が2章でした。

ラッセルのパラドックスは、事前学習をしたのですが、wikipediaを見てもよくわからない状態でした。 R = { x | x ∉ x } という集合の定義をみたときに、 x は要素でありながら( x ∉ x の右辺)、集合である( x ∉ x )ということを考えると、 x が要素であるような集合の要素の集合の要素の集合の……と無限ループになってしまってとらえどころがなくて……。
という話をしたところ、右辺の x と左辺の x の「型」が違うはずなのに区別しないから矛盾が導けるよね、というのがラッセルのパラドックスであると教えてもらいました。

定義2.1.8
あまりにも関数に馴染みがありすぎること、関係というと関数が思い浮かびやすいことから案外つまづきました。部分関数の定義を読んでも、これは何であって何でないのか、というのがイメージしにくかったです。いまの私の理解では、「常に t1 = t2 である」が満たされないのは参照透明でない関係のことを指しているのだと思っています(例えばランダム性のあるものなど)。

定義2.2.1
s R t かつ t R s ならば s = t であるとき、Rは反対称的である というのは少しわかりにくいなーと思います。仮定部分の仮定では「s R t かつ t R s」で非常に対称的に見えるので。しかしその場合は「s = t である」という強い制約が導かれるので、ああたしかに反対称的と言われればそうなのかもな、という感じ。

定義2.2.3
上限と下限(結びと交わり)については「S = { 1, 2, 3 }, s = 1, t = 2のとき 結び j = 2」など具体例を挙げて確認しました。どうにも「結び」「交わり」という単語に苦手意識があるのですが、英語では "join" と "meet" らしいですね。そっちのがまだニュアンスがわかるような気がする。

演習2.2.6
反射的閉包の定義をみると「R を含む最小の反射的関係 R' のことである」とあります。 関係 R' を R' = R U { (s, s) | s ∈ S } とした場合に、R' が R を含むことは明らか。 U の右オペランドが反射的閉包の必要条件であることも明らか。 R の左右のオペランドである集合はそれぞれ何かの要素を抜いた瞬間に R' が R の反射的閉包であるための必要条件が満たされなくなるので、それらの和集合は最小であるといえます。

最初、反射的閉包のイメージが掴めなかったのですがイメージが掴めると、これ同じことしかいってねーなという感じ。

画像では R = { R1, R2 }, R' = {R1, R2, R3, R4, R5}です。関係とは図中の矢印の集合であるというのがわかればまあなんとかなるかと。

演習2.2.7
R0, R1, ... というのは下図のようなイメージ。点線をひいてあるところがその関係で追加されるところです。

演習2.2.8
推移的に追っていけばなんとかなるでしょ、という感じ

2章まではこんな感じでした。次回から本編に入るので楽しみです。

---

1. と大風呂敷を広げましたがめんどくさくなったら派生して調べたことがなくなり疑問のまま放置されるでしょう。↩