昨日僕が顔を出していた時間帯には、指数(exponent; ベキ、累乗)の定義が話題でしたが、前回「けっこうめんどくさい」のでなんとなくやり過ごしていた次の問題がヤッパリ気になるので、露骨(explicit)に書き下しておきます。
今日はルーチンな計算ばっかり書きますが、この問題が述べている事実は、普通のコンピュータを「メモリ状態とその遷移」でモデル化することに対応してます。この事実(主張)はまた、コンピュータによる計算が「typelessだけどtypable」であることをうまく定式化していると思います。
用語/記法は、このダイアリー内でよく使っているものを使うことにします。デカルト圏の定義と基本的なことは、「圏論勉強会 復習:主にデカルト圏の等式的計算」にあります。
ベキ等射の圏
V上のベキ等射の圏とは、それをDとすると、次のような圏です。
- 対象: Obj(D) = |D| = {a:V→V | a;a = a}
- ホムセット: D(a, b) = {(a, f, b) | a, b∈|D|, f:V→V で f = a;f;b }
- 結合(合成): (a, f, b);(b, g, c) = (a, f;g, c)
- 単位 : ida = (a, a, a)
Dが圏となることはほとんど明らか*1でしょうが、(a, f, b)と(b, g, c)のこの順の結合(a, f;g, c)が、ホムセットD(a, c)にちゃんと入ることだけ丁寧に(いやっ、無意味に冗長だった、下に追記あり)確認しておきます。 f;g = a;(f;g);c が成立することが必要です。
// (a, f, b)がホムセットに入る条件
f = a;f;b
// 両辺にbをpost compose
f;b = (a;f;b);b
// 結合性
f;b = a;f;(b;b)
// bはベキ等だったから
f;b = a;f;b
// a;f;b は f だったから(最初の等式参照)
f;b = f -- [1]同様にして
g;c = g -- [2]a;(f;g);c
// 結合性
= (a;f;g);c
// [1]と結合性
= (a;f;b);g;c
// a;f;b = f は仮定している
= f;(g;c)
// [2]
= f;g
[追記]なんか、バカなことしていた。a;f = f と g;c = g を前もって示しておけば、a;(f;g);c = (a;f);(g;c) = f;g とより直接的だった。[/追記]
なお、ホムセットによる圏の定義は、「モノイド圏、豊饒圏、閉圏と内部ホム」の2節を参照。
対象の二項直積
「V×VがVのレトラクションになっている」を正確に言えば、i:V×V→Vとr:V→V×Vがあって、(r, i)がレトラクション対、つまり、i;r = V×V(ここの右辺はidV×Vのことね)。(レトラクション対に関する記述は、「レトラクションの起源(かな?)」と「レトラクションとベキ等自己射」にあります。)
a, b∈|D|に対して、対象a*bを次のように定義します。
- a*b = r;(a×b);i
定義より、a*bがV→VというCの射であることは明らかですが、ベキ等であることは:
(a*b);(a*b)
// a*bの定義
= (r;(a×b);i);(r;(a×b);i)
// 結合性
= r;(a×b);(i;r);(a×b);i
// (r, i)がレトラクション対
= r;(a×b);(a×b);i
// 交替律(interchange law)
= r;[(a;a)×(b;b)];i
// aもbもベキ等だったから
= r;(a×b);i
// a*bの定義
= a*b
交替律については、「指を使った足し算と interchange law」を参照のこと。×に関する交替律 (f;g)×(f';g') = (f;f')×(g;g') は、×の定義に戻って等式計算すれば出ます。
射影
次に、Dの対象a*bに対してDの射p1:a*b→a, p2:a*b→b を次のように定義します(正確には、p1, p2はaとbに依存して決まります)。
- p1 = (a*b, r;π1;a, a)
- p2 = (a*b, r;π2;b, b)
ここで、π1, π2は外の圏CにおけるV×V→Vという射影、rはもちろんレトラクションの射V→V×V。p1, p2がwell-defindであることは:
(a*b);(r;π1;a);a
// a*bの定義
= (r;(a×b);i);(r;π1;a);a
// 結合性と、(r, i)がレトラクション対
= r;(a×b);(π1;a);a
// 結合性と、(a×b);π1 = π1;a
= r;(π1;a;a);a
// 結合性と、aはベキ等だったから
= r;π1;a同様にして
(a*b);(r;π2;b);b
= r;π2;b
等式 (a×b);π1 = π1;a は、×の定義からただちに出ます。
ペアリング
Dの射(a, f, b)と(a, g, c)に対して、それらのペアリング[(a, f, b), (a, g, c)]:a→b*c は次のように定義します。
- (a, <f, g>;i, b*c)
ここで、<-, ->は外の圏Cのペアリングです。これもwell-definedであることを示します。
a;(<f, g>;i);(b*c)
// 結合性と、ペアリングに関する“分配律”
= <a;f, a;g>;i;(b*c)
// b*cの定義
= <a;f, a;g>;i;(r;(b×c);i)
// 結合性と、(r, i)がレトラクション対であること
= <a;f, a;g>;(b×c);i
// 「主にデカルト圏の等式的計算」の[6]
= <a;f;b, a;g;c>;i
// a;f;b = f と a;g;c = g
= <f, g>;i
デカルト圏の公理
さてあと一息。a*b, p1, p2, [-, -]を定義したので、これらが次のデカルト圏の公理を満たすことを示します。だいぶ面倒になってきたので、記号を濫用<らんよう>して(a, f, b)を単にfと書くような横着記法を採用し、f:a→b, g:a→c, h:a→b*c :
- [f, g];p1 = f
- [f, g];p2 = g
- [h;p1, h:p1] = h
横着記法で混乱しないように十分注意してください。
[f, g];p1
// [f, g]の定義、p1の定義
= (<f, g>;i);(r;π1;b)
// 結合性
= <f, g>;(i;r);π1;b
// (r, i)はレトラクション対
= <f, g>;π1;b
// 外の圏がデカルト圏だから、<-, ->とπ1の性質から
= f;b
// このエントリーの[1]
= f同様にして
[f, g];p2 = g[h;p1, h:p1]
// [-, -], p1, p2 の定義
= <h;(r;π1;b), h;(r;π2;c)>;i
// ペアリングの“分配律”
= h;r;<π1;b, π2;c>;i
// <π1;b, π2;c>は、外の圏でb×c:V×V→V×V
= h;r;(b×c);i
// r;(b×c);i = b*c (定義)
= h;(b*c)
// b*c は h のcodomainだったから、このエントリーの[1]により
= h
まとめと言い残したこと
外の圏Cがデカルト圏で、V×VがVに埋め込める(かつ、VをV×Vに引き込める)状況では、Vのなかにミニチュアなデカルト圏が作れるわけです。ミニチュア・デカルト構造の定義は(横着記法で):
- a*b = r;(a×b);i
- p1a,b = r;π1;a
- p2a,b = r;π2;b
- [f, g] = <f, g>;i
ミニチュア・デカルト構造の定義は、実例から(多少の試行錯誤を経て)引き写したものです。実例で考えるとずっと面白いんですが、それはまたいつか。
*1:「明らか(自明)」とか「容易に示せる」とかのフレーズには要注意! 「ここで止まって考えろ」という警告だと解釈すべき。