計算可能世界ってなんだ？ トポス（もどき）かも

計算可能なデータ領域と関数の圏をComputableとでもする。と、名前を決めたところで、The Computableが定義できそうにない。なんか適当な定義をでっちあげても、その圏が The Computableだと主張する根拠がない。だが、いろいろなA Computableを定義できるので、計算可能な世界は、単一の圏ではなくて圏のレルムだと解釈すべきだろう。このレルムを調べることが計算可能性を調べることだろう。

計算可能性の圏論的定式化では、EPペア（レトラクト）、ベキ等射などを使う。この部分は比較的整備されている。例えば、圏C内で対象Xのレトラクトの全体をRetr(X, C)とすると、これはEPペアの圏C_EPを使って、Retr(X, C) = C_EP/X と書ける。レトラクトからベキ等射を作るのは自明だ。モノ射m:A→X がレトラクタブルなことと、mがEP圏の射であることは同値。レトラクタブルなモノはベキ等射で表現可能。

レトラクタブルなモノ射*1（の同値類）の全体は、把握可能な部分対象だと思ってよい。つまり、Subobj(X) のようなもの。Subobjが出てくると、なんかトポスの匂いがする。計算可能な圏、A Computableはトポスになるんじゃないだろうか？ トポスそのものじゃなくても、かなりトポスに近い。

トポスの部分対象分類子を特性射と呼ぶことにする。特性射の定義には、真偽集合（真偽値集合）に相当する真偽対象が必要だが、対象Ωと終対象1から射t:1→Ωの組が真偽対象となる。対象XからΩへの任意の射p:X→ΩはX上の述語と呼ばれる。

  A → 1

  ｜   ｜

  ↓ p ↓t

  X → Ω

上の四角形がプルバックになるとき、A→Xは述語pの核と呼ぶことにする。pの核は、ほぼpの外延だと思ってよい。気持ちとしては A = {x∈X | p(x) } 。ただし、述語pに核が存在する保証は一般にはない。A→X が先に与えられたときは、pはA→Xの特性射と呼ぶ。気分としては部分対象Aがpで把握される*2。

計算可能関数は集合論的には部分写像なので、計算可能な圏の終対象は空集合である。真偽対象は単元集合で、自明な埋め込みをt（true）として取れる。部分対象が把握可能とは、それが計算可能関数の定義域となる集合のことである。

述語とレトラクトの相互変換は簡単なので、述語で把握可能な集合とレトラクタブルなモノ射（の同値類）は1:1で対応する。この状況は、当該の圏がトポスか、それに近い構造を持つことを示唆するだろう。

*1:「モノ」が「物」と紛らわしいからモニックとか単的とかがいいか。

*2:comprehensionの訳語は「包括」だが、ここでは「把握」を使うことにする。

ハロ多圏と上江州計算

ハロ多圏と上江州計算を組み合わせると、かなり強力な道具になりそう。

上江州計算では、重複器、放電器、交差の存在を暗黙の前提にしている。それぞれ、変数の複数回出現（重複）、変数の未出現（未使用）、変数の順序交換（出現位置の順序が変わる）ことに相当する。

上江州アタッチメントの概要； Vが変数集合、τ:V→|C|がソート（型）付けとして、C[V, τ]が定義できる。C[V, τ]には、x∈Vに対する変数射x:[x]→A（τ(x) = A）と逆変数射x^-1:A→[x]が含まれる。単にアタッチするだけなら、Cは任意の圏でよい（実はCが圏である必要もない）。

圏のブランド（セオリー）ごとに上江州アタッチメントを定義できるが、自由構成ができないとうまくいかない。モノイド圏やデカルト閉圏ではうまくいくだろう。V上のラムダ式（項）は、アタッチメントC[V, τ]に対して定義される。このとき、Vに全順序を入れておくほうが話が簡単だし、実用性もある。

有限部分集合X⊆Vに対して、Xを整列した列{x₁, ..., x_n)を作れる。これから、対象[x₁]× ...×[x_n]が決まり、この対象をXの領域[X]だと定める。上江州ラムダ項Mと、Free(M)⊆X であるXの組を {X}M と書く。Xが省略されたときは、X = Free(M)だとする。この形式が [X]→τ(M) という射を定める。ここで、τ(M)はMに対する型（再帰的に定義できる）。

Y⊆X に対して、上江州抽象 Y↑({X}M) が定義できる。

• Y↑({X}M) = {X＼Y}(ΛY^→.M)

「＼」は差集合、Y^→はYを整列させた列、Λはデカルト閉圏の意味でで解釈される。

以上の構成を、ハロ多圏を使って再定式化できないか？ できるはずだ。

上江州ラムダ項Mと変数集合Xが与えられると、ケリー／マックレーン・グラフもどきが描ける。Xを全順序で整列した列を上に並べ、Mの自由変数の出現から作られた列（集合やバッグではない！） FreeOcc(M) を下に並べ、対応する変数をつなぐ。このとき、つないだワイヤー群は重複、放電、公差の有限回の組み合わせとなる。これが、変数のジャンクション・パート。

変数のジャンクション・パート以外は、もとの圏Cで解釈できる。代入文を表す射（上江州さんの用語ではv←射）では、逆変数のジャンクション・パートが出現する。変数を扱う部分は、ハロ多圏内で吸収できるのかもしれない。もし、変数の使用をハロ多圏だけで済ませることができれば、上江州アタッチメントも不要になるかもしれない。いや、むしろ、変数を入れたハロ多圏を作り、それをパッキングすることで上江州アタッチメントを構成できるってことだな。

処方箋：

1. モノイド圏から単純ハロ多圏を作る。
2. ハロ多圏にジャンクションや多射を付け加える。
3. 目的の多圏を作る。
4. パッキングする。
5. 目的のモノイド圏を作る。
6. 新しいモノイド圏と多圏がハロ構造になっていることを確認する。

回路図と大きなラムダ計算がキモかな

僕には、既存のコースや教科書を踏襲する必然性も制約もない。だから、ようするに分かりやすくて短時間で説明が完了すればソレデイイノダ。手段は選ばん！

となると、回路メタファーを使うのが早いだろうし、現実世界を記述する道具として位置づけた大きなラムダ式を活用すべきだろう。

ジャンクション（接合器）と回路素子（circuit element）のセットを回路キットと呼んで、特定の回路キットから作れる回路を考えることになる。入り口は算術回路かな。

本来(?)の用語	比喩的な用語
指標	回路キット
プロファイル付き記号	回路素子
パラメータ付きプロファイル付き記号	ジャンクション
ソート	ワイヤーのラベル
変数／値	ワイヤーを流れるデータ／記号的トレーサ
同値	回路の同値

回路キットの雰囲気は、ラキュー（LaQ）の写真でも使うか。電子ブロックが本家か。

命題論理の回路とラムダ計算の回路の場合：

命題論理	ラムダ計算
命題変数	基本型、ソート
論理式	型表現
証明	式（自由変数あり）
前提なしの証明	閉じた式
演繹定理	ラムダ抽象
モダスポネンス	適用
モダスポネンス消去	βη変換

これを使えば、ジラール対応まで説明できるだろう。

ドミニク・ヒューズの証明絵算論文

• Title: Simple free star-autonomous categories and full coherence (July 7, 2005)
• Author: DOMINIC J. D. HUGHES
• URL: http://boole.stanford.edu/~dominic/papers/freestar/freestar.pdf
• Pages: 36

This paper gives a simple presentation of the free star-autonomous category over a category, based on Eilenberg-Kelly-MacLane graphs and Trimble rewiring, for full coherence.

再度一部を印刷

フーフマン論文が見つからない。しょうがないので、カロウビ展開圏のところを再度印刷した。

割り算できそう

メリーズの定式化をヒントに割り算問題を考えてみた。思い付きだから、確認しないとヤバイけどね。

圏Cの部分圏Σが次の条件を満たすとき、Cのメッシュと呼ぶ。

1. 広大部分圏である。
2. 痩せた（細い）亜群である。
3. AとBが同型ならΣ(A, B)は空でない。

Σによる割り算として、商C/Σと強い商C//Σを定義する。C/Σの定義はメリーズと同じ。C//Σは次のように定義する。f:A→B と f':A'→B' が同値であることを次のように定義する。

1. AとA'、 BとB'はCで同型である。
2. Σの射を[A, A'], [B, B']のように書く。
3. f' = [A',A];α;f;β;[B,B'] と書けるとき、fとf'は同型である。ただし、αとβはCの自己同型。

メッシュΣの標準的な選び方はまったく存在しないので、ΣとΓがメッシュのとき、C//ΣとC//Γが圏同値になることを示さないといけない。

DがCの十分な部分圏のとき、CのメッシュΣをDに制限してもメッシュができる。C//ΣとD//Σは圏同値だと思うがどうか？

線型代数で言えば、線形写像の標準形を求める話。有限次元ベクトル空間の圏のなかで、数空間の圏が十分な部分圏になっている。特に数空間では標準基底が選べるから、数空間の圏には標準的メッシュが存在する。つうか、骨格部分圏か（圏が骨格的 ⇔ 同型の対象は等しい）。強い同値関係だから、ランクだけで分類されてしまう。結局、{0, 1, ..., n}を対象としして、0からkまでを0に移し、残りは単射で埋め込む写像の圏と圏同値になる。ほかの分類や標準形も、圏の割り算で説明できるか？

それと、十分な骨格部分圏の上で、f' = α;f;α^-1で同値関係を入れたらどうなるだろう。

等式的推論の推論規則

推論の構造規則

回路図ではジャンクション。

1. 無（恒等、NOP）
2. 増（重複、コピー）
3. 換（クロス）

放電器は入れない。また定数true（T、I）も入れないことにする。面倒になる割に恩恵が少ないから。

推論の論理規則

略記号	役割	対応する射
Sel1	∧-消去1	π1
Sel2	∧-消去2	π2
And	∧-導入	(-, -)
MP	⊃-消去	・
DT	⊃-導入	Λ, λ

∧の交換律を入れれば、∧-消去が1つになるが、対称性を重視して左右の消去を入れておく。

等式の推論規則

1. 公理・定理のインスタンス化 Inst
2. 等式を前提とした置換 Subst

他に、等号に関する公理を入れる。

有理数の公理

足し算に関する公理、掛け算に関する公理、分配法則も入れる。定数演算記号は、+, *, 0, 1 以外に ~, (-)^-1 を入れておく。実際には、有理数を特定するわけではなくて、単に体の公理。

連立一次方程式のためのマクロ推論規則

Subst' 規則

A[y/y] ≡ A を使う。

   y = C

 -----------[Subst']

  A = A[C/y]

代入法の原理

Subt'とSymm, Tranを使う。

  A = B   y = C

 -----------------[Ass]

  A[C/y] = B[C/y]

左変型規則と右変形規則

  A = B

 --------[Left:A = A']

  A' = B

  A = B

 --------[Right:B = B']

  A = B'

連続等式変型

   A  [S = S']

 = A' [T = T']

 = A''
よって、A = A''

  S = S'

 ------------------[Subst]

  A[S/x] = A[S'/x]

  (A = A')               T = T'

                --------------------[Subst]

                 A'[T/X] = A'[T'/x]

                (A' = A'')

 -------------------------------[Tran]

  A = A''

Δとσはこんなにいろいろな言い方がある

Δ：1つのモノをコピーして2つにする

1. 対角（diagonal）
2. 余加法（coaddition）
3. 分岐（blanching, ramification）
4. 重複（duplication, duplicator）
5. コピー（copy）
6. クローン（clone）
7. フォーク（fork）
8. 水増し（weakening, thinning）

σ：2つのモノの並び順を入れ替える

1. 対称（symmetry）
2. 対称ブレイディング（symmetric braiding）
3. クロス、交差（cross, crossing）
4. 交換（exchange, interchange）
5. フリップ（flip）
6. スワップ（swap）
7. ツイスト（twist）

いろいろな算術システムの例

A1

1. 任意のnに対して掛け算 (*n) : 1→1
2. 足し算 (+) : 2→1

xだけ、x, y、x, y, zに関してどんな出力が出来るか？ なんらかの標準形（正規形）は定義できるか？

((x + x) + x) + x, (x + x) + (x + x ) を描くとどうなる？

A2

1. Δ : 1→2
2. (+) : 2→1

xだけ、x, y に関してどんな出力が出来るか？ A1と比較。

A3

1. Δ : 1→2
2. σ : 2→2
3. (+) : 2→1
4. (*) : 2→1

x, y に関して x*y + x*z は出来るか？ 標準形（正規形）は定義できるか？σをなくすと表現力はどうなるか？

その他

定数や放電器の扱い。

半環のイデアル問題、部分半環の問題。

絵暗算＜えあんざん＞

• 紙を使わず、目をつぶり、頭のなかに絵をイメージして、絵算すること。
• かなりの修行を要する。
• やってみるか。
• … …
• いや、待て、何を計算するのだ？
• 課題も頭の中でイメージ、、、、むっ、難しすぎる。