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

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

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

［参照用 記事］

多圏の必要性、煩雑さ、そして単純化

雑記／備忘

ラムダ計算やシーケント計算の意味論を展開する際に、多圏（polycategory）はほぼ必須です。それ無しでやるのは不自然です。にも関わらず、多圏の説明は少なく、敬遠されている傾向があります。それというのも、多圏の扱いがやたらに面倒くさいからでしょう。

「この状況、何とかならないか」と長年思っていたわけですが、最近になってようやく、多圏の定義を単純化する方法に目星が付いた気がします。

内容：

[追記]4年以上のブランクの後で続きを書きました。

[/追記]

多圏、多圏と言ってるだけで中身がない

ラムダ計算やシーケント計算の意味論には単なる圏では不十分で多圏（Polycategory）を使うべきだ、と随分前から僕は言っています。このブログだと、2007年には既に記述があります。その後も折にふれて繰り返し同じ指摘をしています。指摘しているばっかり、指摘しているだけなんですよね。探しても説明している箇所がありません。

2007年 直積と射影がらみの高階関数たちの相関図

圏論的な解釈としては、A×Bはともかく、A, B って何よ？ ってことになりますが、たぶん、複圏（multicategory）や多圏（polycategory）を導入しないと意味付けできないでしょう。それと、ホムセットをもう一度対象と考えているので、C(-, -)は内部ホムになってます。

2009年 演繹系とお絵描き圏論

さらに、構造規則は回路図（ボックス＆ワイヤー図、ストリング図）と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏（polycategory）という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。

2011年1月 デカルト閉圏を計算するスタックマシン、シーケント計算、カリー／ハワード対応

タプルの一変数じゃなくて多変数の関数を扱うなら、普通の圏より複圏（multicategory）のほうが便利です。多値関数も含めるなら多圏（polycategory）を使うといいですね。

シーケント計算を少しでもご存知の方は、実行過程を描いた図がシーケント計算の証明図と似ていると感じたでしょう。はい、そうです。カリー／ハワード対応です。多圏における絵算を使えば、これらの事がより鮮明に直感的に説明できます。絵算を少しでもご存知の方は試してみてください。

2011年11月 大きなラムダ式／小さなラムダ式

カリー化をより正確に定義するには、Cから作った多圏（polycategory）を使うべきですが、まー、そこまでしなくていいとしましょう。

2011年11月 Alloy、コンパクト論理、関係圏

シーケントの意味論は、Cからいったん多圏（polycategory） Poly(C) を作ったほうが精密ですが、めんどくさいので割愛。おおよそは次のようです。

  1. シーケントのカンマ「,」は、Cのモノイド積だと解釈する（「×」と同じ解釈）。
  2. シーケントには、Cの射を割り当てる。
  3. 特に公理シーケントには、Cの恒等射を割り当てる。
  4. 推論規則には、射のあいだの変換（ホムセットのあいだの写像）を割り当てる。
2012年1月 圏論の筆算としてのシーケント計算

ちゃんと解釈しようとすると、多圏と高次圏を導入することになりますが、だいたいの話ならホムセットだけでも説明できます。

2012年1月 シーケント計算と圏論（続きみたいな）

シーケント計算の背景には、単なる圏よりはむしろ複圏／多圏（multicategory/polycateogry）があるので、年末年始に複圏／多圏について調べようとしたんですが、結局あんまりやれなかったですねぇ。

2015年 中学レベル代入計算からカリー／ハワード流証明の圏へ

コンテキストとシーケント列の圏は、単なる圏以上の構造を持っています。デカルト閉構造はありそうです。複圏（オペラッド）、多圏として考えるとどうでしょうか。この圏をベースとするインデックス付き圏やファイバー圏も作れそうです。絵の描き方（絵算法）も整備したいし。

多圏はメンドクセー

というわけで、僕は多圏の説明をサボっています。でも、僕だけじゃないみたい。多圏についてちゃんと説明している例はとても少ないです。あえて多圏には言及せずにコソッと使ってしまうとか、多圏を正式には定義せずに、なんとなくモンヤリ導入するとか。

こんな状況となっているには、次の2つの理由があると思われます。

  1. 多圏の初歩的概念は、正確に定義しなくても直感で理解できる。
  2. 多圏を正確に定義しようとするとエラく手間がかかる。

多圏をキッチリ定義しようとした試みとして、次の2つの論文があります。

　　

二番目のリチャード・ガーナーの論文は、一番目のユルゲン・コスロウスキの理論をもとに、それを整理・発展させていて、よりモダンな定式化を提供しています。

ガーナーは、彼の論文の冒頭で、多圏を扱うのがいかに大変かを述べています。「もう、死ぬほどメンドクセーよ、あったくもう」と（意訳）言ってます。一文だけ引用すると：

For a start, the sheer quantity of data that one must check for even simple proofs quickly becomes overwhelming.

知らない単語があるんで英辞郎引きました。

  • sheer : 〔生地などが〕シアーの、透けるほど薄い
  • overwhelming : 〔感情的に人を〕圧倒する、打ちのめす / 〔力や数で〕圧倒［征服］する / 〔大きさなどが〕圧倒的な、巨大な

つうことは、

単純な証明のためにチェックすべきちょっとしたデータでも、あっという間にもうトンデモナイ手間になっちゃうんだよね。

という感じでしょう。a morass of trivial details（どうでもよさげな細部の泥沼）がある、とも言ってます。多圏に正面から取り組む作業は、Herculean task だそうです*1。

  • Herculean : 〔仕事などが〕大力を要する、非常に困難な［骨の折れる］

僕も昔ちょっとだけ計算をやってみたのですが、すぐに百数十ケースの場合分けが出現して、こりゃダメだ、と投げ出しました。

多圏を定義するには

多圏には素朴な定義があり、それは十分に分かりやすいものです。しかし、その定義をもとに計算や証明をするのはHerculean taskになってしまい、現実的ではありません。より機能的で洗練された定義が必要なのです。

コスロウスキやガーナーは洗練された定義を与えていますが、それは大掛かりな道具を使ったものです。目的の定義に到達する前に、道具の使い方を習得するのが大変です。

基礎知識の準備を全部すっ飛ばして、ガーナーによる多圏の定義の概要だけ記してみます。出てくる言葉からしてワケワカランということであればスキップしてください。

ガーナーは、多圏をモナドとして定義します。モナドは、圏Cに対して「C上のモナド」として定義されます。圏Cは圏の圏Catの対象なので、抽象化すると2-圏Kの対象Xに対して「X上のモナド」概念が定義できます。

さらに一般化して、Kが双圏（bicategory）であるときにも、双圏Kの対象X上のモナドが定義できます。問題となるのは、多圏をモナドとして定義するときの舞台となる双圏Kの構成です。

ベースとなる双圏は、「圏、プロ関手（profunctor）、プロ関手のあいだの変換」からなる双圏ですが、最初に与えられた双圏Bから、新しい双圏Kを作り出す手順を一般的に準備します。その手順とは、もとの双圏B上の擬モナド（pseudomonad）と擬コモナド（pseudocomonad）、そして擬分配法則（pseudo-distributive law）があるときに、これらから両側クライスリ双圏（two-sided Kleisli bicategory）を作る手順です。

ベース双圏Bと、その上の擬モナド、擬コモナド、擬分配法則から作った両側クライスリ双圏がKのとき、Kの離散対象（discrete object）Xを選べば、X上のモナドが多圏を表現する構造だ、というのがガーナーのシナリオです。

これは、「死ぬほどメンドクセー」を回避するために選んだ戦略ですが、別な意味で死にそうに大変な定義なんですけど……

多圏を何に使いたいのか

僕の場合の多圏に対する動機は、多変数・多値を許すラムダ計算やコンパクト・シーケント計算に必要だからです。多圏の一般論をしたいわけではありません。用途を限定すれば、もう少しこぢんまりとした多圏の定義がありそうな気がします。

ラムダ計算やシーケント計算の意味論に使う圏はモノイド閉圏（典型例がデカルト閉圏）です。テンパリー／リーブ圏なども扱うなら、対称（symmetric）ではないモノイド圏も含めます。意味的領域であるモノイド閉圏Cに対して、計算デバイスとなる多圏Poly(C)が構成できればいいのです。

これは、多圏の一般論に比べればはるかに単純な状況です。具体的なモノイド閉圏Cから出発して細工すればいいので、大道具を駆使しなくても日曜大工で何とかなるだろう、と思っていました。

ですが、何の工夫もなしでやってみると、やっぱりHerculean taskになります。状況が単純なので、人間の手に負えない量じゃない気もしますが、僕の気力・体力では太刀打ちできません。手をこまねいているうちに10年ほどたってしまった、と。ハァー(ため息)。

何とかなりそう

単純化した状況でも多圏の定義がなおも大変なのは、もとの圏Cに対称性を仮定してないことが大きな理由です。Cが対称モノイド閉圏ならば劇的に簡単になり、たいした問題なしにPoly(C)を定義できます。でも、テンパリー／リーブ圏や自己関手の圏とかも扱いたいので、対称性は仮定したくないのです。

最近、対称性がある場合の構成法を眺めていたら、同様な方法が非対称のケースにも適用可能なことに気が付きました。先入観があったんですね。対称性を仮定した議論が非対称の場合に通用できるはずがない、って。

というわけで、特定目的のための特定状況下においては、多圏の構成はそれほど難しくないことが分かりました。とはいえ、ブログ記事一回分で述べられるほどのショートカットではないです。多圏の話を少しずつでも書き進めることが出来たらいいな、とゆるく思っています。

[追記]4年以上のブランクの後で続きを書きました。

[/追記]

*1:洗練された定義を提示してもHerculean taskは残るようで、ガーナーは別な論文でダブルクラブ（double club）という概念・手法を開発して対処しています。