signalsandthreads.com/future-of-pr...

そうすると先の「aの無限列の途中でb」みたいなやつはµX.(aX + bµY.aY)のトレース集合として自然に計算できるようになる。最初µX.(aX + b)と思ったけどこれだとaの有限列もトレース集合に入ってくる（bのあとに暗黙の「正常終了」プロセスがあり、そっちが選ばれると終了する）(というかimage finitenessの問題がある?)

この追い越しを認める逐次合成はweak sequencingと呼ばれ、シーケンス図(Message Sequence Chart)の意味論のために今でも研究しているグループがある。一方、sequencingに追い越しの機能を持たせるのではなく、プロセス計算のprefixingの流儀でweak prefixingというやつを考えてみる。そしてMazurkiewiczトレースのような事後的な並べ変えでなく、演算子の意味(生成するトレース集合)そのものに「追い越し」をハードコードする。

Mazurkiewiczトレースにおいては無関係なアクションの並べ替えでトレースを増やすけれども、これは無限のトレースとは相性がわるい。たとえばaが無限に続くa^ωと、それと無関係なアクションbをsequential compositionでつなぐと無限のトレースは「終わらない」ので通常は(a^ω・b)=a^ωが成り立つけれど、もしaとbが無関係で追い越せる場合は有限回のaの後にbがはさまる(a^ω・b)=a*ba^ωみたいなことになる。後ろにあるプロセスがb単体ならまだわかるけどa^ω・b^ωとかもっと複雑なやつがどうなるのかは無限トレースのための意味論をよく調べないとわからない

欲しい機能はできたのでドキュメントとテストをだな

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

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

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

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

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

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

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