指折り残付近をかんがえた

どうも細切れの時間と、本業と干渉がここのところ激しく検討が進まない。

指折り残について考えてみた。あれは結局、複数FSMを組み合わせた
サブシステムとしてみたときに、ある性質ψを満たすためには、
不要なプロトコルがあるよということを指折り演算により検出する
というのが趣旨であった。

一方最近細切れに考えていたのは、プロトコル合成の方は仕組みがわかった
個別プロトコルを合成制約をまぶして１つのプロトコルに合成する仕組みだ。

でも合成されたFSMをシステムとしてくみ上げたときには、またA/G関係に
分割してほげほげ？ということにするなら、最初から合成前の個別プロトコル
がA/Gの元であると思えば、実はA/G分解した後のProofグラフは作る前からできている
ことになる。

不要・不要でないというのは不毛いや不要な議論で、むしろ、ψを満たすか
どうかを、モジュラーにできるかどうか？満たさないときにはどこがわるいか
をProofグラフの中で局所化できるか？というのが本筋で、不要の発見と
いうのは、部分プロトコルXが、ψあるいは部分システムMのコンテキスト
では、なんとかを満たすためには過剰であったということだ。

過剰といわれてもこまって、それは相手の動きの仮定が間違っていた？
それとも動きの理由付けが失われた？（待たなければいけないとか）。

結局プロトコルは何をしていることになるんだろう、情報の流れに対して。
同じことをするのに、相手の動作の仮定に依存して異なるプロトコルで
情報の流れを保証するということなんだろうなあ、すると相手の動作如何では
不要なプロトコルというのもあることになるんだろう。

すると相手の動作に対するプロトコルの要・不要と情報流についてなにか考え
ないとぶれてしまう。そこがしっかり決まれば、

例えば、なにかの仮定のもとには、プロトコルを緩和するとかのもうちょっと
メタなAssumeがあるんではなかろうか？

おおそうかAssume/Guranteeにはなんかレベルがありそうだ。
最大maximumな遅延を考えてだたしく情報がながれるように書いたプロトコルと
そうでなくて、なにか条件をいれて、緩和したもの。

うまく整理できないのかなあ。
結局、４２歳の誕生日はもやもやと停滞している。