このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Alloy本いただいた 2

さらにチラチラ:

  1. (本じゃなくてAlloyが)全体に、オブジェクト指向言語、特にJavaと類似の構文にしようとしている印象。abstractとかextendsとか。それが良いか悪いかはともかく、やるんなら、sigじゃなくてinterfaceにすればよかったのでは。
  2. sig(interface)の実装が、アトム集合になる。アトム集合がクラス相当ってのはけっこう辛いアナロジーかな。もっと辛いのは、「インスタンス」って言葉が使えないことだ。他で別な意味で使っている。
  3. アトムが状態点でアトム集合を状態空間とすれば、まーギリギリだが、クラスとのアナロジーが取れるか。「インスタンス」は使えないとなると、thisの指すものは個体(individual)とでもするか。
  4. sig = interfaceの実装領域(アトム集合)の個体(アトム)ごとに、値が変わるのがフィールド。いちおう辻褄はあう。
  5. フィールドの値はスカラーとは限らず、シングルトンとも限らず、集合かもしれない。
  6. なんでも関係とみなすのはまーいいんだけど、メンタルモデルとしては、演算の項(オペランド)にほんとのアトムやほんとのタプルが入ったとき、演算が可能になるような自動型変換がされる、とするほうが余程分かりやすいだろう。
  7. 概念的には、アトム、アトムのタプル、タプルの集合は区別しなくてはならない。それらの型変換を純粋に思考と概念の世界に押し込めるのは、実は負担が大きい。むしろ、異なる型に属するが、同等なモノへの変換は処理系がすべき。
  8. 例えば、限量子で束縛された変数は要素を走るとするのがどう考えても自然。ベキ集合内のシングルトンセットの領域を走る、と考えるのは辛い。さらに、単項関係(長さ1のタブルの集合)の集合内で、特にサイズ(基数)が1のモノの領域上を走る、なんて考えるのはマゾ!
  9. 「タプル」をサイズ1の関係(一元関係)、「集合」をアリティ1の関係(単項関係)とする用語法は、どうやっても徹底できないだろう。破綻することは眼に見えている。
  10. 「タプル」や「集合」は極めてポピュラーな用語だから、ジャーゴンオーバーロードして使うべきじゃないだろう。
  11. '->' が直積、というのも少し違うような。長さnのタプルの集合と長さmのタプルの集合を、二項直積して出来るタプルの長さは2であって、n+mじゃない。'->'でタプルの繋ぎ目が完全に消えるかというとそうでもない。(a1, ..., an; b1, ..., bm) のようなモノが出来るのだろう。あくまで気持ちとしては、だが。
  12. 関係演算 '->' の結合律はon-the-noseで成立するが、関係圏のカリー化/反カリー化が背後にあるのを忘れないほうがいい。データセットのレベルでは on-the-noseだが、射のプロファイルの変化が伴う。
  13. プロファイル概念(単にタプルの切れ目を「;」とかでマークするだけ)があれば、転置も推移的閉包もずっと一般化出来る。
  14. タプルの切れ目を移動するだけでカリー化/反カリー化も出来る。左に移動でカリー化、右に移動で反カリー化(だいたいだけど)。
  15. graded pointed setの圏に直積を入れて、その圏内のモノイドを考えると '->' の代数的なモデルになる。だいたいだけど。
  16. 関係の圏では、∪をベキ等な可換演算と考えて、それで順序が導入される。なので、可換ベキ等モノイドの圏で豊饒化できる。(なんか関係ない話に行ってしまったか。)
  17. ドットは、記法としては良いが、定義がショボイだろう。プロファイルがないので、なんか恣意的にプロファイルを割り当てている。
  18. 関係の域は、sigがあるので割と明確だが、余域がわからない。余域と像(image)を値域(range)という名で混同している気配がある。全域かどうかは判断できるが、全射的(surjective)の判断は曖昧。
  19. 「値域」は「余域」と「像」にオーバーロードしているのか? それだと困るな。
  20. sigを使う限り、関係の域はアトムの集合に限られる。(普通の意味で)タプルの集合を域に指定することができない。結局、アトムの集合を域として、タプルの集合を余域とする範囲?
  21. しかし、アリティにおいて、1→n だけを取り出すと、ドットの定義がまったく整合性がない。n = 1 以外ではうまくいかない。n = 1 だとすると、関係圏のendmorphismモノイドしか使ってないことになる。so-called「集合」は、subidentityになる。
  22. プロファイルがないのが、全体に暗い影。