このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

コンパクト閉圏と絵算で理解する線形代数とシーケント計算(入り口だけ)

モニャダラセミナーのネタにしようかとも思ったんですが、一般論過ぎるのでエントリーにします。


アブラムスキー(ココとかココに写真)は、コンパクト閉圏においてネームコネームという概念を定義しました。コンパクト閉圏の射fに対して、fのネームとfのコネームが定義できて、三者は互いに変換可能です。三位一体(Trinity)を成していると言ってもいいでしょう。

上の図を見ればわかるように、fのネームはゲーデル符号化の記号を流用しています。実際、ネームは符号化になっています。働き(機能性)であるfを、データとみなしたものがfのネームです。関数fのコンパイルされたコード(データとなる)がfのネームだと解釈しても構いません。

fのコネームは、ゲーデル符号化と図形的に対称となる記法を採用しています。コネームもネームと同様にfの符号化を与えますが、コンパクト閉圏の双対性を利用して、ネームの双対となるように定義されています。

ゲーデル符号化の記号は表記しにくいので、fのネームを f 、コネームを f で表すことにします。この記法は、形が絵算と対応しているので、僕は気に入っています。ラムダ計算や圏の指数で使う記法 f^ とも整合しています。f, f, f のうち1つが与えられば、残り2つは作り出せます。つまり、f, f, f は事実上同一物のように思えるのです。これが、三位一体という言葉を使った理由です。

絵算、線形代数、シーケント計算

コンパクト閉圏では、絵算が効果的に機能します。先の三位一体を絵算で描くと次のようになります。絵の描き方は、射の向きが上から下です。

f:V→W という射(絵ではオダンゴ)に対して、fのネーム f の絵が左下です。fの域(domain)側のワイヤーを逆U字型(∩の形)にひん曲げたものが f です。右下はfのコネームです。こっちは余域(codomain)側のワイヤーを∪の形に曲げています。

通常の圏論では、ワイヤー(対象)を曲げるとか、逆走する(図で下から上に向かう)射とかを表現する手段がありません。また、図では、逆さまになったV(Λの形)と逆さまになったW(Mの形)も出現していますが、これもキチンとした解釈が必要です。

キチンとした解釈のひとつとして、線形代数を使う解釈があります。V、Wなどの対象はベクトル空間、射は線形写像だとします。逆さまになったV、Wは双対空間で解釈します。つまり、Λ = V*、M = W*。逆走とU字型カーブの部分は、双線形形式またはその双対で解釈します。次の絵のようになります。

コンパクト論理は、連言(AND, ∧)と選言(OR, ∨)が一緒になってしまった単一の論理演算×と、真と偽が一緒になってしまった単一の論理定数Iを使う論理です*1。トンデモナイ論理のようですが、否定(¬)は存在し、意外と古典論理と似た推論が可能です。コンパクト論理におけるシーケントは、論理式が右側だけで左側には何もない形にできます。「演繹系とお絵描き圏論」で触れたゲンツェン/テイト/シュッテ(Gentzen-Tait-Shutte)スタイルの片側シーケント(one-sided sequent)です。右片側シーケントと双対的に左片側シーケントも定義できます。次のような感じです。

線形代数における三位一体とシーケント計算

コンパクト閉圏、絵算、線形代数、シーケント計算のなかで、多くの人にお馴染みなのは線形代数でしょう。その線形代数における三位一体の説明には、コンパクト論理のシーケント計算がけっこう使えます。シーケント計算は、線形代数の計算には粗っぽ過ぎますが、粗っぽいのでオオヨソの事情を把握するにはかえって好都合なんです。(とかいって、今日は説明しませんけど、、、ダハハハハ)

線形代数における「f, f, f の三位一体」とは、詰まるところ「行列の解釈が3つあるよ」って話です。行列は、2つの添字(例えば、iとj)を持つスカラーの集まりです。即物的に言えば、単に2次元配列データです。この2次元配列データを線形代数の文脈で解釈すると、どうなるでしょう:

  1. 行列は線形写像である。これは、一番普通の解釈でしょう。
  2. 行列は行列である。これは、行列もベクトル(データ)だと見る立場です。m行-n列の行列は(n×m)個のスカラー成分を持つので、(n×m)次元のベクトル空間をなします。このn×m次元ベクトル空間の要素が行列だ、ということです。
  3. 行列は双線形形式である。m行-n列の行列は、適当な基底(枠)を取れば、m次元ベクトル空間とn次元ベクトル空間の双線形形式を表現します。

この3つの解釈のあいだの対応関係を調べることは、基底を使った直接的な計算に頼れば難しくはありません。でも、絵算やシーケント計算を使ったほうがたぶん楽しいです。

線形代数とコンパクト論理

有限次元ベクトル空間においては、二重の双対 (V*)* は、Vと標準的(canonical)に同型です。双対を表す左肩星に代えて「¬」を使って、同型を「≡」で示せば:

  • ¬¬V ≡ V

線形写像 f:V→W があれば、双対空間のあいだの逆向きの写像 f*:W*→V*が作れます。これは次のように書いてもいいでしょう。

  • (V→W) ⇔ (¬W→¬V)

¬¬V ≡ V と (V→W) ⇔ (¬W→¬V) はそれぞれ、二重否定の原理と対偶の原理に対応します。線形代数に、なにやら論理的な対応物があるわけです -- コンパクト論理です。

一方、絵図的に言えば、Vをひっくり返すとΛ、さらにひっくり返すと元に戻ってVですよね。ひっくり返す(180度回転)操作を¬とすると、¬(¬V) と V は同じ形、上から下に向かう矢印 V→W を上下さかさまに(これも180度回転)すると M←Λ という下から上に向かう矢印になります。時間を逆行する電子を陽電子と捉えるのと似たように、逆行する射 M←Λ(下から上)は双対な射 W*→V* (これは上から下)として解釈します。次の絵を眺めてください。

参考とか予定とか

タイトルに「(入り口だけ)」と書いたのは、まとまった事を書く気力が今日はないということです。代わり(?)に、過去に書いた記事へのリンクを挙げておきます。

線形代数における双対・随伴・共役とかは、僕にとっては気にかかるネタで、断片的にですが何度も書いています。

伝統的テンソル計算と線形代数の関係は:

コンパクト論理(線形論理のサブシステム)と線形代数の関係、その概略は次に書きました。

f, f, f という記法は絵にあわせているのですが、絵の描き方における上下左右の問題は次で議論して(愚痴って)います。

シーケント計算とソフトウェアの関係は:

「f, f, f の三位一体」を基礎に据えて、コンパクト論理のシーケント計算を道具にして線形代数(の初歩)を展開するのは面白いなー、と思っています。そのことをチャント書いたことはないので、まー、いつか書くかも。

*1:[追記]本家・ジラールGirard)による定義は、テンソルと余テンソルが一致した線形論理がコンパクト線形論理のようです。[/追記]