イギリスのシェフィールドに滞在しています。
2週間の予定で、いま1週目が終わったところ。1週目はMidlands Graduate School
in the Foundations of Computing Science 2025というのに参加していた。
いろいろなトピックの講義を受けたが、いちばんのお目当てはもちろん線形論理であった。Abhishek DeさんとCharles Grelloisさんが線形論理の講義を担当した。演習のセッションも充実。講義ノートは以下で見られる。
私は線形論理研究者の卵だが、ずっと我流で勉強してきたので、専門家から系統だった講義を受けられてよかった。
講義の構成は、第1回が線形論理のモチベーションと構文論・証明論の導入、第2回が焦点化(focussing)、第3回が圏による表示的意味論、第4回が証明ネット、となっている。どれも線形論理の重要トピックである。もちろん線形論理には、他にも興味深いトピックがたくさんある。
で、私ならどんな構成にするかなとか考え、そこからさらに教科書を書くならどうしようかな、と構想してみた。いまさら線形論理の教科書なんて売れないだろうから、ほとんど妄想なのだけど。
線形論理の教科書といえばTroelstraのものが良い本だが、90年代に出たものなのでだいぶ古くなっている。
元祖であるジラール先生の"The Blind Spot"ももちろん良いけれど、線形論理の教科書というよりジラール哲学の教科書であり、クセが強い。
竹内外史による日本語の『線型論理入門』も竹内流すぎて教科書ではない感じ。
というわけでオリジナルの新教科書を構想(妄想)する価値は十分にある。
まずはAbhishekさんと同じように、カット除去手続きの非決定性から線形論理のモチベーションを説明しようかな。歴史的には線形論理は整合空間(coherence space)による直観主義論理の意味論の研究から始まっているのだから、そこから始めるのも良さそうだが、それだと整合空間の説明に紙幅を費やすことになってよくないかもしれない（"The Blind Spot"ではλ計算やカリー=ハワード同型の話から整合空間、そして線形論理、とちゃんと順を追って進んでいるけど、線形論理の教科書でそれをやるのはマズそう）。
というわけでまず証明論から始めて、カット除去定理など標準的な結果を示す。
その次は証明論の顕著な応用としてDanos氏らのデコレーションを扱うのが良さそう。古典論理や直観主義論理や様相論理への翻訳の研究である。それもカット除去手続きを保存した翻訳。
続いて相意味論(phase semantics)をやるのが良いだろう。ジラール先生の原論文"Linear Logic"ではむしろ相意味論から話を始めているくらいである。相意味論は90年代に改良され、岡田光弘先生によるカット除去定理への応用研究も登場した。この辺はTroelstra本ではまだ触れられていない（昔の本なので）。焦点化定理や決定可能性/不可能性の証明にも相意味論は使える。
次は焦点化。焦点化はAndreoliという人が発見したもので、ジラール先生の原論文の次に重要な成果だとどこかに書いてあった気がする。論理プログラミングへの応用も広いし、哲学的にも興味深いと思う。応用として統合結合子とルディクスに触れる。
で、決定可能性と不可能性、そして計算複雑性あたりだろうか。これはまだ未解決問題も残されている重要テーマであるが、線形論理っぽくない話になるので、流し気味のほうがいいかも。
その次に整合空間と圏による表示的意味論とゲーム意味論あたり。これは私は詳しくないので、まだあまり構想ができない。
そして線形論理の最大の功績とも言える証明ネットをこのへんで。証明ネットは定数なし乗法的断片に対して与えるのは易しいが、定数や加法や指数を考え出すと大変で、どれくらい扱うか塩梅が難しい。私もまだよくわかってないし。
証明ネットのコレクトネスの話から、相互作用の幾何学(GoI)や超越論的シンタクスの展開に触れて締めよう。GoIは関数解析とかの難しい数学を使うこともあるが、置換の代数のようなものとして導入すれば易しいだろう。超越論的シンタクスに触れるには哲学の話が必要になるので大変そうだが。
というわけで出版社の方！ 連絡お待ちしております！
