lptk.github.io/programming/... Demystifying MLsub — the Simple Essence of Algebraic Subtyping

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…

CSPの表示的意味論のほか、著者の先行研究 doi.org/10.3233/FI-1992-163-402 もそんな感じ。一方、CCSやπ計算を触っているとトレース何それおいしいのになりがち

もうちょっとだけ簡単になりませんかね…