加算合成のめどがついたのですが、そこで停滞気味です。 もうちょっと最後までやろう。 現行のしくみで加算合成の出るパターンをすべて書き下してみる 実は、２つのＦＳＭの合体も加算合成の変種であることを示す。 そうすると、ずんずん、加算合成をやって…

アルゴリズムの正しさを証明するためのシステムとしてWhyをいうのがある。 こいつはoccaml風のアルゴリズム＋アサーションを入力として、各種定理証明器向けの入力を 出力するという代物です。下はsqrtの例ですが、ここまで書かないと正しさを証明はできない…

http://www.diku.dk/~yokoyama/TetsuoYokoyamaOld.htmlさんの論文Deterministic Higher-order Patterns for Program Transformationというのがあった、どうもパターン（ルール）をつかって言語変換するといいうフレームワークの理論的な論文らしい。 Higher-…

会社賢人その１と加算合成関係の話していたら、どうも、圏論で一連の論理展開は整理できるそうです。 加算合成は、圏論でいうところのPushoutに相当するそうで*1、どうもプロセス代数は有名な例だそうです。圏論が本研究の何の役に立つのかよくわかりません…

PAP上の加算合成は、つまるところは で表せる対象に、という順序依存性を インポーズするということ。対象式を展開すると ・・ M1 ・・LM3 ・・ M1ここで、bとcの順序依存性を考慮して矛盾項を消去すると。 のみが残るという計算をしますということたったそ…

PAでは、PAP(Process Algebra for Parallelism)にデッドロックとencapsulation を追加した ものを ACP(Algebra of Communicating Processes)と呼ぶのだが*1やっとencapsulation の意味がわかった。これは、通信実行（同期実行）を強制するためのオペレーショ…

いろいろ考えると、STG(状態遷移グラフ)、EDG(イベント依存グラフ)、 EPT(イベントプロセス項)、EPG(イベントプロセスグラフ) の間に成り立つ直上的な変換関係は以下のようになるのだが STG_v->STG_e->EDG->(EPTEPG) EDGをSTG_e(STG_v)に逆変換する方法がよ…

いままで、雰囲気で取り扱ってきた、イベント依存グラフを、すこし 形式化しようとしている。結局加算合成をイベント依存グラフ上で 計算しないといけないことになって、悩む。とくに状態とイベント依存 関係がごっちゃになってしまう。ふとノートを見返すと…

PAのなかのPAPのやっかいなところは、ループ構造を直接的には表せないところだ。 regularなものが必要になる。ここでPAの勉強がとまっていたが、 Regular Expressions in Process Algebra http://alexandria.tue.nl/extra1/wskrap/publichtml/200511.pd当面…

やっぱり論文形式のドキュメントはGoogleDocで書くのはつらい。 元の木阿弥 Latexに戻すことにする。MACとwindows機の間で特定のファイルやフォルダを手っ取り早くsyncさせたいのだが FolderShareなるサービスが結構使えそうだ。 https://www.foldershare.co…