まだまだ

研究 主テーマ

先日の同期の件は、実装とCCSの間のギャップという話であるが、大して問題になりそうになさそう。
ということで、落着しよう。

それよりも、肝心の順序制約\psi^1_{a\rightarrow b}の意味が揺らいで、投稿論文にだしたもの(2月)はなんか違っている。むしろ予備審査に出した物(12月)があっている。なんで。？？

なぞは深まる。というよりも投稿論文版(2月)が導出できない。

いろいろやってわかったこと

  • 予備審査版は、a_i\rightarrow b_{i+1}のときのa1の動作が制限されていなさすぎた、
    • 最初は制限がないからやり放題という投稿論文の主張はうそということ
  • 横チェーンは制限した物とはちょっとちがうが、縦チェーンはなぜか一緒
  • LTS3をやめてcnt付きのLTS4をつかって横チェーンを確かめてもOK、本来こちらを使うべき。
  • LTS4で、brbw型でなくてbr2型の制約に切り替えてみると、なんと予備審査版のLTSと同じになった。制限がゆるんだからだろう

どうも予備審査版は\nabla演算の意味定義を素直に適用したもので、投稿論文版はLTS(出来損ないの）で表現したものに並行結合演算を施した物らしい。どうも、1月9〜10日のノートに書かれている内容が、はずれている？らしい。このとき何を気にしていたのか？また戻り？？

d_i\rightarrow a_{i+1}のたとえで、d1はa2に先行しますが、a1よりも先行はできませんということ（投稿論文ではd1は無制約状態であった)。。