このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

インターリーブ定理とTuraevゲーム

プログラム意味論 からみ系 課題

X, Yが状態空間（圏論的には単に対象）として、A, Bを遷移（つまり、endomorphism）の集合とする。A∪{idX} = A+, B∪{idY} = B+とする。A, A+, B, B+ などを構文的存在（ラベル、名前）と同一視して、議論を構文領域に持ってくる。

それで、次の3者は全然違う（星印はクリーネスター）。

  1. A+*×B+*
  2. (A+×B+)*
  3. (A++B+)*

しかし、適当な同値関係≡1, ≡2, ≡3を入れると、

  • (A+*×B+*)/≡1 = (A+×B+)*/≡2 = (A++B+)*/≡3

となる。このテの主張がインターリーブ定理。

インターリーブ（interleave, interleaving）定理は、コンピューティング・サイエンス的解釈も圏論的解釈も素朴・自然に行える。そのときの鍵は次のシフト可換律（スライディング可換律）。

  • (f×Y);(X×g) = (X×g);(f×Y)

f- := (f×Y), -g := (X×g) と略記すれば、

  • (f-)(-g) = (-g)(f-)

と、確かに可換律の形をしている。

コンピューティング・サイエンス的には、次の3者の同値性を主張している。

  1. マルチ（とりあえず2つ）プログラムの分離2CPU完全並列実行による効果
  2. マルチプログラムのクロック同期2CPU完全並列実行による効果
  3. マルチプログラムの1CPU時分割直列（順次）実行による効果

圏論的には、シフト可換律を、

  • f×g = (f×Y);(X×g) = (X×g);(f×Y)

と書き換えると、これは交替律と同値な等式となる。つまり、シフト可換律≒交替律≒双関手性（なお、単位に関する双関手性は、2CPUにおけるnop, idle, time-fillerの定義となる）。

インターリーブ定理の圏論的解釈は、（対称とは限らない）モノイド圏の計算法則を与える。f1, ..., fn∈End(X) とg1, ..., gm∈End(Y)に対して、次の3つの表現が同じ射を与える。（便宜上、n < m として書く。）

  1. (f1; ...;fn)×(g1; ...;gm)
  2. (f1×g1); ...;(fn×gn);(X×gn+1); ...;(X×gm)
  3. (fi-)と(-gj)を適当にインターリーブして結合した列

n≠m のときでもid（nop）を挟んで調整できる点に注目（この点は圏論的計算ではありまり意識されてない）。fi, gj がendomorphismであることは実は本質ではなく、ずっと一般的な状況でもOK。


さて、問題はここからで、同値関係≡1, ≡2, ≡3をどう定式化するか？ もちろん、代数的／組み合わせ的な定義はできるが、それじゃつまらないし、わかりやすくない。組み合わせ圏論を使いたい。

トゥラエフの輪切り（スライス）とトゥラエフ移動（ライデマイスター＋ジグザグ（スイッチバック）＋Ψ（プサイ））、ラフォン（Lafont）の図式的レイヤー／図式的等式、ランカスター／ラーソン／タウバー（Lancaster, Larson, Towber）のイベント／トランジション／スチル／フリッカー／ムービーなどを、ゲーム風に仕立てる。

『お絵描き圏論』でも、コンパクト閉圏の計算はゲーム風だと言ったが、それをチャント定式化するってわけ。そのゲームをTuraevゲームと呼ぼう。

Turaevゲームは矩形のゲーム盤にコマ（ブロック）を置いて／動かして一人で行う。盤は横の行（段）に区切られていて、1つの行には（通常は）1個のコマしか置けない。空白部分はidと解釈する。盤の矩形部分をリージョンと呼ぶことにする（ストリング図ではチャンバーと呼んでいた）。ゲームは次の操作で進行する。

  • 盤上のリージョンに注目（フォーカス）して、ルール（トランジション・ルール）に従って別なリージョンに置き換える。

ゲーム盤自体が変形（縮小拡大）することもある。盤自体と盤面状況（コマの配置）の変化列がゲームの履歴となる。2つの盤面状況（シーン？ スチル？）が、とあるTuraevaゲームで繋げるとき同値として同値関係が入る（ゲームは可逆）。

やること：

  1. TODO: Turaevゲームをもっとチャント定義。
  2. TODO: Turaevゲームの実例（トランジション・ルール）を作る。
  3. TODO: Turaevゲームと、ラフォンの定式化、ランカスター／ラーソン／タウバーの定式化との対応関係／用語法の違いをまとめる。
  4. TODO: Turaevゲームを使ってインターリーブ型の定理（異なる表現の同値類の同一性）を示す。
  5. TODO: インターリーブ定理の比喩的な分かりやすい／面白い説明を考える。
  6. TODO: Turaevゲームの幾何学的な合理化を考える。

幾何学的な合理化とは、Turaevゲームにより幾何学的変形や幾何学的単純化（正規化）が実際に行えることを示す -- ホントにやると難しいから、まー、直感的な納得感があればいい。