不動点意味論のわかりにくいところ

なんとなくわかってきたのでメモ

  • 結局は、半順序、上限がイメージしにくい
    • a{\sqsubseteq}b
    • 半順序は直感的にa より b のほうが情報が多いというだけのもの
    • 半順序かどうかではなく、そうなるように定義されているものとして扱う
      • 上限も同様に性質として存在するもの（たとえばcpo）を扱っている
    • (特に上限は)数値の大小や集合の包含関係のイメージに優先されない
      • たとえば、自然数Nでの順序は、1=succ(0)と規定されているから、1は0から拡張した存在として順序化される。数値の大小として付いているのではない
      • たとえば、Boolは一般的にはtrueとfalseの2値だが、ふつうこの2つの間に順序はつけないので、それだけでは最小限がないことになる。そこで意味論上ではtrueとfalseの他に最小限として機能する⊥を追加したBool+⊥として扱う(Boolに限らずenumのようなものはこうする)。
    • 全順序にならない半順序としては、タプル(組)をイメージすると良いかも
  • 関数は単調・連続というのは（ここでは）「前提」
    • 関数がf:[D{\to}D] であり、a{\sqsubseteq}f(a) であるというなら、Ｄには、f(f(a))はf(a)より「絶対に」情報が多くなる半順序関係が使われるものとしてみる

帰納法とかそうだけど、証明で納得できるのか、というのがある。証明ってそれが正しいとしか言ってない。たとえば、その定理にあてはまるような例がイメージしにくいところにある。この本は、こういうのがずっと続くんだよなあ。