でこれきさんのが十分うまくいっている

読むとうまくいってないね

なんらかのmetricを決めたら不動点が決まると思っていたけれど、そういうmetricが存在するような空間では不動点はuniqueになるってことなのか(???

例えば、のところが間違えている気がしてきた

p.50, subtyping lattice上の単調関数について不動点をとると最小不動点と最大不動点は一般に一致しないと思う (例えば x = a.x + b は最小不動点をとるとb, 最大不動点をとると所望の無限木が得られる) んだけど、なんかBanachの不動点をとることで両者が一致してると言っていて、まだよくわからない

選択演算子なんだからトレースの和集合でしょという漠然としたイメージが少し修正された。なんらかのシミュレーション関係っぽい。構成をやりなおしか？

これがためにループの意味をプロセス計算のトレース集合の不動点でとると実はうまくいかないのか

たぶんこの枠組みでよくある証明テクなんだけど選択演算子で片方が選択されたときに射影後のプロセスではまだそれが反映されてないことがあって、グローバルなビューとローカルな実態が厳密な一対一対応を維持せず進行している。サブタイプ関係がついたまま進行する。

オートマトンっぽい本(Rudiments of µ-Calculus)を読んでたからwordの集合で考えてしまっていたけどプログラミング言語のトレースはこのように扱うのだな。正直prefix-closedにする意義が全然わかってなかったよ…(センスがない。

Bill Roscoe本p.36: It is natural to model an untimed CSP process by the set of all traces it can perform. It turns out that recording only finite traces is sufficient in the majority of cases – after all, if u is an infinite trace then all its finite prefixes (initial subsequences) are finite traces…