発端は照井一成先生の「相互作用としての計算」という論文である。しかしこれは「現代思想」(青土社)という学術誌よりはカジュアルな雑誌に掲載されたもので、内容的にもそれほど堅苦しいものではなく、論文というよりは論考とかエッセイと呼んだほうがよいのかもしれない。
それはさておき。
照井先生という人は京都大学の数理解析研究所という非常に権威ある機関で数理論理学と計算機科学を研究しておられるが、もともとは哲学科の出身で*1、数学の哲学や歴史の話題も盛り込まれた数学・計算機科学入門記事あるいは本をよく書いておられ、特に私なんぞにはおもしろいものが多い。というか失礼な言い方だが文章が上手いのである。「相互作用としての計算」という記事は2012年11月の現代思想のチューリング特集増刊号に掲載されたものであるが、この雑誌はいったいどういう人が読んでいるのか謎で、たまに数学の特集をして死ぬほど難しい記事が載っていたりトンデモっぽい記事が掲載されたりするのだが、照井先生の文章は私のように論理学と計算機科学と哲学をある程度勉強した人間にはちょうどよい*2。この「相互作用としての計算」もクイズから始まったり将棋を題材にしたりしていて、読みやすいしわかりやすくて良いのである。
そんなわけでこの"相互作用としての計算"という概念について調べてみることにした。その調査結果を備忘録的に書いていくよ。今回はその照井先生の論考の内容をまとめて、ついでに調べたことを書いておく。
この"相互作用としての計算"という概念は、チューリング機械やλ計算といった計算モデルに対抗するものである。アラン・チューリングは、人間の「計算」という活動を分析し抽象化することでチューリング機械というモデルを開発した。このチューリングの発見手法を照井先生は「チューリングの精神」と呼んでいる。そして、チューリングやチャーチ以来の伝統的な計算モデルであるチューリング機械やλ計算といった計算モデルは「インプットアウトプット」という形式になっているが、現代における計算の在り方をチューリングの精神に則って分析し抽象化すると「エージェント
エージェント」型の計算モデルが必要である、というのが照井先生の主張である。でこの新しいタイプの計算概念が"相互作用としての計算"というものだ。そしてこのパラダイムは1990年代頃に盛んに研究されたらしく、記事のなかでそうした研究をいろいろと紹介している。
だいたいこんな感じなのだが、やはりこの記事はそれほど本格的なものではないので、相互作用としての計算というもののテクニカルな定義とか詳細な性質の議論とかはなされていない。それに照井先生は哲学者ではないので「相互作用としての計算とは何か？」みたいな議論をこれ以降で深めていって執筆したりとかもしていないようである。しかし調べたところ相互作用を重視する論理学・計算機科学研究の流れというのは確かにあって、哲学的にもなんかポストモダン的な妖しい魅力を放つ話題だし、やはり自分なりに調べて考えてみる価値はありそうだ、と思った。
まずは計算における意味での"相互作用"とは何なのか、という話である。照井記事では相互作用という言葉の説明もあまりないのだが、英語の"interaction"の訳語であると思う*3。この interaction というものを自分なりに解釈してみると、計算において何かを「する側」と「される側」に分けるのではなく、相互に影響を与え合って行われる、ということであると思う。どちらが偉いわけでもなく。チューリング機械では制御部とテープでは制御部のほうが偉そうだし、λ計算では例えば の
のほうが
より偉そうな感じがする。もしくはその逆と感じる人もいるかもしれないが、いずれにせよ非対称的である。と、なんだかふんわりした話になってしまうのだが、このへんをきっちりと形式的に定義するのは難しいかもしれない。照井先生は相互作用的な計算モデルの例をいろいろと挙げていて、これを見ると interaction というものがなんとなくわかってくる。
まずはπ計算である。π計算はλ計算の reduction に似た計算をする体系であるが、特に並行システムのモデルになっている*4。λ計算における関数適用が、π計算ではメッセージのやりとりあるいは通信になってくる。つまりλ計算では入力が計算を発生させるが、π計算では二つのエージェントがやりとりしあうことで計算が発生する。なるほど、相互作用的である。π計算を創始したのは計算機科学者の Robin Milner (以下：ミルナー) という人である。ミルナーはチューリング賞も受賞した偉大な学者で、π計算は彼の業績のほんの一部だったりする。π計算以前にはCCSというモデルを提唱しており、π計算はこれを拡張したものらしい。さらに晩年には bigraph という新たな体系の研究に乗り出していた。チューリング賞の受賞理由には定理自動証明の研究やプログラム言語MLという並行計算とは別の分野の業績も含まれるのであるが、ミルナーの研究の動機には interaction への関心が大きなウェイトを占めていたことは確かであろうと思う。ここのところ私はミルナーの"Communicating and Mobile System: the π-calculus"という教科書を読んでいるのだが、interaction という語は頻繁に出てくる。他の本でもそうのようだ。しかもチューリング賞の記念講演のタイトルも"Elements of Interaction"だった。まだ読んでないけど。ミルナーは哲学者ではまったくないけれど、その思想的な面が気になってくる。
型付λ計算と直観主義論理は同型性があるというのがカリー＝ハワード対応で、近年では他にもいろいろとこれを拡張したりいじったりした論理と計算の対応は知られている。というわけで照井先生は、π計算などの interaction を意識した計算体系と同時期に現れた論理体系として線形論理を紹介している。ちなみに照井先生にとって線形論理は主要な研究テーマの一つのようで、多くの論文や解説記事を書いておられる。線形論理を提唱したのは論理学者の Jean-Yves Girard (以下：ジラール先生) である。ジラール先生はかなりユニークなロジシャンで、計算機科学よりのロジックで多大な業績をあげつつも根っこには深淵な哲学思想があるようだ。というか深淵というより難解で「ジラールの言うことはよくわからん！」みたいな意見もよく見る（気がする）。まあそういうところも魅力的だと私は思う。そしてジラール先生は Geometry of Interaction (相互作用の幾何学) という理論を提唱したり、Ludics (遊技*5 ) という理論を解説した"Locus Solum"というクセ強めなタイトルの本では副題を A purely interactive approch to logic としていたりしていて、interaction というものを意識していそうである。だがこの相互作用の幾何学というのは難しくて、何が相互作用なのかとかも今のところよくわからない。遊技のほうは照井記事でも取り上げられている。だが照井記事ではおもに線形論理の双対性を論じている。直観主義論理の証明の簡略化や正規化が計算の実行に対応するのに対して、線形論理はカット除去を計算と対応させると双対性によって相互作用的な計算になるとのことであるが、このあたりは照井記事では示唆するに留めている感じで*6、このへんはカリー＝ハワード対応と合わせていろいろ調べてみるべきところであろう。さらに照井先生はゲーム意味論も取り上げている。線形論理は双対性があるので対称的なゲームになる。遊技もゲーム意味論の一種で、ゲーム意味論が interaction の一つの現れだというのが照井先生やジラール先生の考えであろう。
π計算と線形論理は近い時期に現れたが、根底の”相互作用としての計算”という思想が一致しているというのが照井先生の考察である。しかしπ計算と線形論理にはカリー＝ハワード対応のような綺麗な対応があるのかどうかとかは記事では述べられていない。調べてみるとπ計算と線形論理の相互翻訳というのがちゃんとあるらしい。おもしろそうである。
というわけでミルナーとジラール先生の理論や思想を調べるとおもしろそうである。しかし私はもうひとり、照井記事に名前は出てこないが重要そうな人物を発見した。それが Samson Abramsky (以下：アブラムスキー先生) という学者である。この人も計算機科学の専門家であろうが、圏論的な論理や量子力学、および量子計算の研究で近年注目の人である。アブラムスキー先生はおそらくジラール先生と比べると格段に明快な人なのだろう。線形論理のゲーム意味論の主要な業績をあげた一人でもあり、相互作用の幾何学もアブラムスキー先生らが圏論を使って再定式化したものが計算機科学の世界ではよく調べられているようだ*7。なおかつアブラムスキー先生の著作にも頻繁に interaction という言葉が出てくる。しかも一時期は"interaction group"というセミナーというか研究会をやっていたらしい。並行計算の研究もしていたようで、ミルナーの研究との繋がりもある。
ここまでは並行計算のモデルとか線形論理の話題だったが、論理と計算の対応をミクロなレベルで考えていた。もっと明示的に通信というものを盛り込んで相互作用を実現する論理体系はある。照井記事とはかなり方向性の違う話になるが、線形論理のカット除去と計算の対応なんかとは別の次元で論理と計算の対応をもたらすであろう。それは例えばマルチエージェントの動的認識論理とか、チャンネル理論とかいうやつなんかである。このへんは線形論理とかよりもさらに知らないことが多いのでこれから調べます。
