なぜにアミダはそれほどに重要か
僕がプログラム意味論とTQFTが関係すると思い出したのは、マーク・ホプキンスの観測と示唆がキッカケだ。マークの観測は完全に正しかった。ステファネスクがやっていたことはそれを裏付けるし、最近のシャイ・ハランのF1の研究（Non-Additive geometry） はさらに状況証拠を与える。
図式プログラミング言語を考えると、ソースコード＝図 となるので、プログラム（のソースコード）の圏は「図の圏」と考えてよい。プログラム意味論とは、ソースコードの意味を定義するものだから、意味写像は 図の圏→適当な圏 という関手となる。
意味領域である「適当な圏」は振る舞いの圏と言ってもよい。「振る舞い」という言葉だと誤解をまねくかもしれないから「振る舞いの記述」といったほうがいいかもしれん。
- 振る舞いの圏の対象はプログラムの入出力を表すナニカ
- 振る舞いの圏の射はプログラムの振る舞いの記述
意味関手＝振る舞い関手 となる。これはまた、計算構造で計算関手と呼んだものと同じ。
- 意味関手＝振る舞い関手＝計算関手＝TQFT関手
プログラム意味論では、実行によらずにプログラムの同値性やプログラムの模倣関係を知りたい。よく使われる手段はプログラムの書き換え／変形である。プログラムは図だったから、これは図の変形操作となる。
プログラムの同値性、プログラムの書き換えの簡単で分かりやすい例は、ブレイド図の圏のアルチン変形とマルコフ移動だ。ブレイド図とブレイド群を完全に区別して、ブレイド図をプログラム、ブレイド群を振る舞いと考える。すると、アルチン変形で移りあえる同値関係が振る舞い同値になる。さらに、ブレイイド閉包を考えると、アルチン関係とマルコフ移動で移れる同値関係（マルコフ同値）が振る舞い同値になる。
状態遷移系の模倣、長谷川やセリンガーの一様性、ステファネスクの酵素規則などもマルコフ同値に近いと思える。行列にアダマール順序（成分比較するだけのバカ順序）を入れた2-圏とかが振る舞い記述の圏になるように思う。ここで不等式が出てくる。
「図」を多様体や複体と解釈すると、コボルディズム圏が出てくる。TQFTとは、多様体を図とするプログラムの振る舞いの理論だと言ってもよいだろう。このとき、振る舞い記述の圏はヒルベルト空間の圏となり、振る舞いはユニタリ線形写像やユニタリ対応となる。
といった諸々のこと、これらの源泉はアミダの圏にある。
それはそうと、円筒にアミダを描いたら、周期的な振る舞いをするプログラムになるよな。これの同値性ってどう判断するんだろう。全部同値になってしまう気がするが。
