論文に関する思い出

トップ

主要な論文に関する思い出です。

Algebraic effects and handlers for arrows

Journal of Functional Programming

博士論文の投稿版である。

修士論文を書いた後は、いろいろつらい思いをした。 修士論文の投稿版はなかなか会議に通らないし、学振は落ちるし、自分ではどうしようもできない不幸なことが起きたりで長い間気分が落ち込んでいた。 落ち込んだ気分を騙すために、ひたすら御所や吉田山を散歩しては、写経して心を落ちつけるような心持ちでCategorical Logic and Type Theoryを読む毎日だった。 京都の静かな部分と、数学的な事実は、心の支えとなる。

2022年の6月にMFPSに修論の投稿版が通って、気分が少し晴れた。 代数的エフェクトに関する論文をあさっていると、LindleyのAlgebraic effects and effect handlers for idioms and arrowsという論文を見つけた。 この論文はアロー(とイディオム)に対応するエフェクトシステムの構文だけ作ったという、何の数学的裏付けもない論文である。 ただ後にわかるが、結果的には基本的な直感は良い線をいっている。

Lindleyの論文とは別に、アローの意味論的な発展もあった。 例えば浅田先生がアローは圏と関係手(profunctor)のなす双圏Profにおける強モナド(強プロモナド)だと明らかにした。 しかし、この事実に基づいた構文はまだなかった。

このように、アローについては10年ほど前に活発に研究されていたが、その後あまり研究はなかった。 吉田山で瞑想して、その原因のひとつは、意味論的な発展と構文論的な発展が分断されてしまったことだろうと思い至り、これらの統一を行うことにした。 つまり、強プロモナドから代数をつくり、その代数でうまく意味を与えられるようなプログラミング言語(構文)を作るということである。

まず問題になったのは、Profにおけるモナド(プロモナド)の代数とは何だろうかということである。 Catにおけるモナドの代数は、Eilenberg-Moore圏の対象である。 同様のことを考えて、プロモナドの代数はEilenberg-Moore圏の対象であるとしようとするとうまくいかない。 なぜならば、圏C上のプロモナドからEilenberg-Moore圏を作ると、対象はCの対象と同一になってしまい、なにも面白いことが起こらないからである。 その原因はEilenberg-Moore圏の「中身」という圏論的に正しくないことを考えたからである。 圏論的に正しい行いは、Eilenberg-Moore圏と他の圏との関係を調べることである。 結果的には、2圏論的なEilenberg-Moore圏の普遍性を考慮することで正しい代数の概念を得ることができた(Section 3.1)。

このようにして定義された代数の概念と準同型射を考えることでハンドラの意味が得られた(Corollary 3.4)。 Lindleyのハンドラの型付け規則には謎の"X fresh"が出てくるが、これは米田の補題を考えれば適切に消去できるだろうとわかった(ただ、Lindleyの構文との正確な対応をとることはほぼ不可能なので、論文には明示的に書いてはいない)。

その後、構文を定める段階に入った。 意味論的なことがしっかり固まっているので、安心して構文を考えることができた。 Lindleyたちのarrow calculusを拡張して、オペレーションとハンドラを追加するのが筋がよいだろうとわかった。 構文が定まった後は、操作的意味論を定義し、進行補題と保存補題を証明した。

操作的意味論が定まったので、次は表示的意味論を定めることになる。ここで問題が二つあることが明らかになった。

  1. シグネチャから定まる自由なモデルを作るときに、ナイーブにやると真クラスができてしまい、破綻する。
  2. ハンドラの意味論を定めるときに、強度に由来する現象により、普通のやり方では意味が定義できない。

一つ目に対しては、標準形を導入した(Proposition 5.4)。標準形だけを集めると集合のサイズに収まるので問題が解決する。 後で査読者に教えてもらってわかったが、この標準形はすでにYallopが博士論文で導入していた。

二つ目については、普通の意味論が潰れすぎていることがよくないとわかり、より膨らませた意味論を考えることで解決した。 具体的に言うと、パラメータを一つ余分に付け足すのである(interpretation with a parameter, Section 5.3.2)。 例えるならば、二次方程式の解が存在しない場合があるという悩みに対して、虚数を導入して解の存在する空間を膨らませて解決するようなものである。 これは通常の強モナドでは気にしなくてよかったことが強プロモナドでは問題になったのだった(Remark 5.9.)。

これらの問題を解決して、無事に表示的意味論が定まり、操作的意味論との整合性(健全性と妥当性)を証明できた。 途中で、実はうまくいっていないのではないかと冷や冷やしたが、操作的意味論と進行補題・保存補題をAgdaで形式化していたので、少なくとも構文的には絶対にうまくいっているという事実が安心材料となった。

あとは構文屋さんを満足させるために具体的な応用例を作らなければならない。 はじめ、アローの歴史に従い、構文解析の例を書いたが、これは実は例になっていなかった(査読者に指摘された)。 構文解析のためには、アローにさらに付加的な構造を持たせる必要があった。 構文的にはこういう構造を付け足すのは造作もないことだが、意味論的にはもうちょっと考えたいので、この構文解析の例はやめた。 代わりに論理回路シミュレーションの例を書いた(Section 1.2)。

アローの特徴は、代数の要素が列であることだ。 通常のモナドの代数の要素が木である(Category-Graded Algebraic Theories and Effect Handlersの思い出を参照せよ)のと比べると、アローでは演算の結果によって条件分岐できないという制約が付く。 このことは次のように理解できる。 モノイドは群の一般化であるために逆元を取る操作が制限されている。 これと同様に、アローはモナドの一般化であるために条件分岐を行う操作が制限されている。 このような制約は不便だと思うかもしれないが、状況によってはうまく利用することができる。 これはプログラムに型という制約をつけることで、「正しいプログラム」のみを許すという考え方と似ている。 例えば、静的な(ビットの値によって回路自体をダイナミックに変更しない)論理回路のシミュレーションには、アローが適している。

2023年6月にJournal of Functional Programmingに投稿した。 10月に査読結果が返ってきて、major revisionとなった。 内容には肯定的で"innovative", "significant contribution"などと評価されたのが嬉しかった。 ただ、余エンドの計算や豊穣圏論の議論が難しすぎると言われたので、Appendixを追加して1圏論がわかっていれば原理的には読めるようにした。 2024年2月にminor revisionとなり、少しの修正を行った。 5月にacceptとなった。

この論文は博士論文でもある。2023年11月に提出し、2024年1月に公開講演を行い、無事に博士号を取得した。 ちなみに、数理解析研究所では(少なくとも私が在籍していたときは)博士申請時にその博士論文が出版されている必要はないようで、そのため、この論文を博士論文にできた。

Explicit Hopcroft’s Trick in Categorical Partition Refinement

CMCS 2024

小島氏、小森田氏、室屋先生、蓮尾先生との共著論文である。

私は博士課程の間、量子フェローシップという制度で生活費と研究費をもらっていた。 量子フェローシップの義務の一つに、期間中にかならず民間企業または研究機関にインターンにいかなければならないというものがあった。 そこで、私は国立情報学研究所の蓮尾先生のところに2022年9月の2週間の間インターンに行くことにした。

蓮尾先生からさまざまな論文を提示され、その中にJacobsとWißmannのFast Coalgebraic Bisimilarity Minimizationがあった。 この論文はcoalgeraicといいつつ、かなりの議論が集合論的に議論されているので、それをもっと圏論的にできないかというものだった。 結果的には、圏論的な定式化ができた。 その過程で既存の分割細分(partition refinement)アルゴリズム全般に適用できる不等式を発見しHopcroft不等式と名付けた。 ここでは、Hopcroft不等式の発見に関する思い出を書く。

分割細分アルゴリズムは、システムの状態を分類するときに、区別できる状態を段階的に分割していくアルゴリズムである。 このアルゴリズムの計算量評価にはHopcroftのトリックと呼ばれる議論が使われる。 Hopcroftのトリックは、部屋を分割していくつかの小さい部屋にすると、一番大きい部屋以外の大きさは、分割前の部屋の大きさの半分以下になるということが本質である。 ほとんどの分割細分アルゴリズムはこのトリックを用いて計算量を削減している。

しかし、Hopcroftのトリックだけが計算量評価の本質ではない。 いろいろな分割細分の論文をみると、Hopcroftのトリックを使った後に、よくわからないアドホックな計算をしている。 蓮尾先生に、この職人芸的な部分をなんとか理解したいと言われ、解読を試みた。

2022年12月のある夜中に数理解析研究所のコンピュータ・サイエンス室で計算をしていた。 そのときに分割細分の様子を重み付き木で表現することで「よくわからないアドホックな計算」が理解できることに気づいた。 分割細分アルゴリズムの計算量評価は、実は長方形の面積の「縦かける横=横かける縦」という幾何学的な性質に基づいているのだった。 この「縦かける横=横かける縦」とHopcroftのトリックを組み合わせることで、根付き重み付き木に対する綺麗な不等式が得られることがわかった。 この不等式をHopcroft不等式と名付けた。 この不等式を利用して、償却計算量解析を行うことで、多くの分割細分アルゴリズムの計算量評価がシステマチックに行える。

Category-Graded Algebraic Theories and Effect Handlers

MFPS 2022

修士論文の出版版である。 元々の修士論文にはモデルの構成にミスがあったことが査読者の指摘で発覚した。 それを修正したバージョンがこの論文である。

2020年の2月ごろにERATO蓮尾プロジェクトで1ヶ月ほど国立情報学研究所に滞在していた。 当時修士1回生で、プロセス計算の勉強などをしていたものの、どういうことが研究になるのかよくわかっていなかった。 滞在中も成果が出ていなかった。 滞在後半のある日、勝股先生福田さんと食事に行った。 そのときに勝股先生が代数的エフェクトは木のイメージなのだと説明した。 そのわかりやすい説明を聞いて私はすぐに代数的エフェクトの思想が理解できた。

国立情報学研究所の滞在を終えていくつか代数的エフェクトに関する文献を読み始めると、Orchardたちが次数圏付きモナド(category-graded monad)という概念を導入しているのを見つけた。 彼らの論文にはいろいろ微妙なところがあるのだが、例えば必要な条件が抜けていたりする(Appendix C. footnote 3)。

次数付きモナドを使って代数的エフェクトのエフェクトシステムを捉えるという研究は勝股先生がすでにやっていた。 したがって、この研究を真似して、順序付きモノイドを圏に置き換えることで、新しいことができるだろうと考えた。

ハンドラを定義するには次数圏付きモナドの代数とは何かを考え、代数の間の準同型射を考える必要がある。 次数付きモナドに関しては内藏さんの研究があった。 また、かなり一般的な状況、つまりlax関手に関するEilenberg-Moore構成が50年前にStreetにより研究されていた。 この二つを眺めると、次数圏付きモナドに対応する代数の概念が導出できるのだった。

2020年の8,9月ごろに意味論的な計算をいろいろやって、エフェクトシステムの大まかな形ができあがった。 そのあとこの言語が役に立つ例を捻り出す作業をして、プログラムが通信プロトコルに従っているかどうかを検証できるという例を作った。 私にとっては、新しい数学的概念を元に言語を作ったということだけで満足できたのだが、構文屋さんを満足させるには役に立つ例が重要なようだ。

2021年3月に修士論文として、この論文(の古いバージョン)を提出した。学位記授与正代表(理学研究科)となった。

その後、この論文を投稿することになったが、会議に通すのにかなり苦労した。 意味論を理解してもらえた人からは優しいレビューをもらえたが、そうでない人からは正反対なレビューがやってきた。 何度か落とされて、最終的にMFPS 2022に通った。

MFPS 2022はニューヨーク州イサカにあるコーネル大学で行われた。 自分の論文で海外に行くのは初めてであった。 コロナの影響でオンライン参加も選べたが、せっかくなので現地参加にすることにした。 いろんな人に優しく話しかけてもらい、楽しい思いをした。 自分の発表の質疑応答ではいくつか質問がきた。 オンライン参加者の質問がうまく聞き取れなかったが、スピーカーの音質が悪いと言ってごまかした(申し訳ない)。

当時は帰国する前にコロナの検査をして帰国便の搭乗手続き時に陰性の検査結果を提示しなくてはならないということになっていた。 そのため、一度マンハッタンまで行き、検査を受けた。 帰国便は自分の検査結果を見せなければ乗れない。 帰国便の搭乗手続きをする少し前にメールで結果が届いたのだが、名前がよく似た別人の検査結果だった。 すぐに検査場に電話して正しい結果を送ってもらった。 名前の微妙な違いに気づかなければ日本に帰れなくなるところだった。