「晩に渋谷でパスタの会：双対編」アジェンダ＆資料 - (保存用) 檜山正幸のキマイラ飼育記メモ編

イントロはマジメに（＝ツマラナイ）予習復習だ

記号に慣れてね。

A×B
A + B
1と0
id_A = A （よく使う、特に僕は）
f×K （id_A = A の応用）
f×g
f + K
f + g
<f, g> と Δ
[f, g] と ∇ （ただし、∇は“足し算”の意味でも使う）
π₁, π₂ （ただし、下添字も使うときは π¹_{A, B} など）
ι₁, ι₂

参考：圏論のお勉強なら、Catyスクリプトでやってミソ - 檜山正幸のキマイラ飼育記メモ編

計算（コンピューティング）の話をするとき、多くの場合：

射は計算行為のなんらかの単位
域は計算開始前の資源状況の型（つまり制約だ！）
余域は計算開始終了後の資源状況の型（ホーアトリプルを思い出せ）
射の方向は時間方向（過去から未来）と一致する。

くれぐれも、特定プログラミング言語や常識的な計算機構に捕らわれないこと。

例：f:int→int, g:int→int の結合

f:int→int はこれ（特に 5|→f(5)）：



int x = 5; // 入力の初期化

int y; // 出力変数

{

 // xからyを計算するコード

}

g:int→int はこれ（特に 10|→g(10)）：



int y = 10; // 入力の初期化

int z; // 出力変数

{

 // yからzを計算するコード

}

(f;g):int→int はこれ：



int x = 5; // 入力の初期化

int z;  // 出力変数

{

 int y;

 // xからyを計算するコード

 

 // yからzを計算するコード

}

たいていは対象＝型に（射にも）モノイド積があり、その意味は：

計算資源を一緒にする／寄せ集めること；または
場合分けによる制御フローの分岐

ここらで愚痴と雑談

「頭おかしい」と「頭たりない」
なんでみんな「対象と射は何でもいい」ってことを忘れるかなーー、頭たりないんじゃないの？
すぐに役立たなくても、現象と法則が見えることに意味があると思う。さもしい姿を見ると、差別用語を使いたくなる。

それはそうとして、圏論のココロのごく一部だが：

点、要素、値は射です。インスタンスの代わりにコンストラクタを考えるようなもの。
対象も射で代用できる（圏論番外：横着者のための型なし圏論（ただしフォーマル） - 檜山正幸のキマイラ飼育記 (はてなBlog)）。カロウビ展開圏では、対象は親の圏のベキ等射だしね。
つまり、キホン、射しかありません。
これは、データより計算行為を重視する考え方。行為には時間方向の向きがあるから、矢印で描きやすい。

右自明モノイドのスタンピングモナドのクライスリ圏

復習。これ(↓)みりゃわかるだろ。

var g = 0; // 大域変数

// 副作用付きの関数（ベースの圏では射とみなしにくい）

function foo(x) {
 g = 3*x;
 return x + 1;
}

function bar(y) {
 g = y + 2;
 return y * 2;
}

// クライスリ圏の射

function Foo(x) {
  return [x + 1, 3*x];
}

function Bar(y) {
  return [y * 2, y + 2];
}

// クライスリ結合

function kl_comp(F, G) {
  return function(x) {
    var Y = F(x);
    var Z = G(Y[0]);
    var effect;
    if (Z[1] === undefined) {
      effect = Y[1]; // undefinedでもいい
    } else {
      effect = Z[1];
    }
    return [Z[0], effect];
  };
}

function kl_commit(Z) {
  if (Z[1] !== undefined) {
    g = Z[1];
  }
  return Z[0];
}

/*

>>> var k = kl_comp(Foo, Bar)
>>> k(1)
[4, 4]
>>> k(2)
[6, 5]
>>> k(3)
[8, 6]
>>> k(4)
[10, 7]

*/

不純な計算とは

不純は面白い、不純は楽しい。

副作用（ストレージへのアクセス）
未定義（必然的な部分性）
例外（エラー報告と処理）
非決定性（不確定な計算）
大域脱出（goto, setjmp/longjmp）

僕の不純な問題意識：副作用とトランザクションと例外の関係をちゃんと理解したい。

今までやったこと

カリー化の圏論的取り扱い（デカルト閉圏）
NJの小さなサブセットと型付きラムダ計算の対応（カリー／ハワード対応）
クラアントサーバースタイルの副作用（アクションモノイドによるモノイダルスタンピング・モナド）

どんなストーリーがありうるか

計算から線形代数へ（非決定性、コンパクト閉圏）
計算から幾何へ（多次元フローチャート、計算的ホモトピーやタングルの圏）
計算から論理へ（シーケント計算、証明図の圏）

どこを経由しても、同じ所に行き着くらしい。アブラムスキー、ジラール、バエズなんかがそう言っている。行き先はいわば、

計算の幾何的代数（geometric algebra of computation）

近隣の地図：

＼	自明な構造	非決定性で自明な構造
直積	対角Δ	合併∨（∪）
直和	フォールド∇	公平な分岐∧

今日のキーワード

檜山の造語が多い。ただし、すべて線形分配圏の議論に出てくる概念の言い換え。

分離する直積（separating direct product）、分離する直和
混合結合律、混合交換律
分合律（dissociative, 線形分配律）
東西南北双対性（近隣の地図）
三項、四項のホム
シーケント計算

双対性

2009-10-13 より。

これは、直積のコモノイド／モノイド双対性：

参照	更新
DBを参照する	DBを更新する
クエリ	更新リクエスト
クエリの実行	更新のコミット
クエリ結果の使い回し	更新リクエストのキューイング
イミュータブルなスコープ	トランザクション

これは類似性：

ストレージ更新	線形代数
更新モナド	スカラー体
ストレージ	ベクトル空間
更新リクエスト	スカラー
リクエストの連接	スカラーどおしの乗法
コミット	ベクトルとスカラーの乗法
何もしない操作	スカラーの 1
矛盾を引き起こすリクエスト	スカラーの 0
矛盾した（回復不可能な）状態	ゼロベクトル

これは、状態（大域変数とか）参照と例外の双対性：分かりにくかったので文言を修正した。

状態	例外
状態に依存する関数	例外を起こす関数
状態の大域的なセット~~(例：注入)~~	例外の最終的な捕捉
状態の生成と初期化	例外の握りつぶし
状態を出力にダンプ	入力を例外としてスロー
状態を参照も変更もしない	例外を捕捉しない
状態のコピー	例外の集約（同一視）

一般化クライスリ結合と分合律

ライブでお絵描き。

最近考えたラムダ抽象（カリー化）の説明

僕のヒモ計算を納得しない人も多いので、クロージャと遅延評価を使った説明を考えた。

値（要素）は三角で描く。射だけど。
クロージャは値なので、三角で描く。
が、三角のなかに四角（関数、計算）が入っている。
クロージャ三角から足が二本。
ヒモを束ねる留め金（clasp）も使う。
三角のなかの三角は環境（束縛）
面倒になると、三角が丸になっちゃうかも。
遅延評価を使えば、値と式はあまり区別しなくてよい。クロージャは値を運ぶ式と思う。ときに、クロージャと値を同一視。

カリー化すると、Λ(f) = f^{^} ができる。
Λ(f) に値を入れると、fのクロージャが出力される。
クロージャと残余引数をevalに入れると、evalのなかでf（のミニチュア）が環境を伴って起動する。
でもさ、これってヒモ計算と同じじゃん。
ヒモ計算では、クロージャに封入された計算（ミニチュアコピー）と元の計算をなんとなく同一視する。値という概念を一切使わない（だから、分かりにくかったのだろう）。
大きなラムダを使った計算は、この状況をちゃんと表してるぞ。ザマーミロ。

シーケント計算

古典論理のシーケント計算は、直積と直和を持つ圏の計算現象に対応する。含意があれば、指数（ベキ対象、随伴）を持ち、カリー化が可能。カリー化の双対が例外ハンドリングコードの構成。

シーケント計算の規則	計算現象
三段論法（カット）	一般化クライスリ結合
減（縮約、コントラクション）左	対角による引き戻しΔ^#
減右	余対角による前送り∇_#
増（水増し、ティ(ン)ニング）左	射影による引き戻しπ^#
増右	入射による前送りι_#
∧右	デカルトペア
∨左	余デカルトペア
→右	カリー化
→左	例外ハンドリング

含意の導入と消去（演繹定理）がラムダ抽象（カリー化）と評価（eval, apply）に対応することはよく知られているが、含意の左規則が例外処理に対応していることが指摘されるのは少ない（気がする）。

あとそれから

非決定性を導入すれば、双積とテンソル積を持ったコンパクト閉圏の議論になる。これは、驚くほどに線形性と双対性を持つ。なぜか、ヒルベルト空間の圏とソックリ。物理との類似性が濃厚。非決定性がpossibilityという質的（二値的）評価しかしないが、量的評価としてのprobabilityを入れると物理になるのか？

フローチャートの変形の幾何は、結び目やタングルの話とつながる。変形の書き換え規則は、特異点の変化の前後を記述しているが、連続に補完すると、それは高次元のなめらかな変形の影であるらしい。フロベニウス法則や双代数法則は、確かに図形変形（の影）の記述になっている。結合律や単位律はいうまでもない。

ジラールは、相互作用の幾何（GoI）とか証明の力学とか言っている。彼は、論理現象をほとんど物理的な現象だと捉えているらしい。ジラールが、「cutなし証明＝データ」「一般の証明＝アルゴリズム」「cut消去＝計算」（意味としては実行）という用語を使っているのはそれなりの意味があってだろう。

シーケント計算（論理）と計算（コンピュテーション）の話では、そもそもシーケント推論規則が基本射のCPS変換（またはその双対）をベースにしている。否定に関しては、大域脱出（継続）との関係が指摘されている。CPS変換＝米田埋め込みを使って、gotoとsetjmp/longjmp の話ができたらいいなー、とか思ってます（現在まだ調査考案中）。