ものすごく久しぶりの第三弾。このテーマはそのまま修論になる可能性があるので継続していきたい所存。
サムソン・アブラムスキー先生の1994年の"Proofs as Processes"（リンクはPDFです）という短い論文を読んだのでその記録である。
内容は"相互作用としての計算"にとって超重要な洞察を提示しているのだが単純明快である。数学的に難しい話は出てこないので私でも理解でき、今後このテーマについて話すときはこの論文を挙げるとよさそうである。またそれに加えてこの論文が書かれた経緯も述べられており、こちらも重要である。
プロセスとしての証明とは？
タイトルの"Proofs as Processes"を理解する。まず"proofs"すなわち「証明」を復習し、続いて"process"すなわち「プロセス」を説明する。
証明とは？
証明というのは証明体系における形式的証明のことである。この論文はカリー=ハワード同型対応（以下：CHI）のような論理と計算の対応を論じたものである。CHIでは基本的に直観主義論理の自然演繹と型付ラムダ計算の対応を考える。その際、命題は型に、証明はラムダ項（プログラム）に、証明の簡略化は計算の実行に、証明の正規化は計算の停止に対応する。しかしこの論文では自然演繹と簡略化ではなく推件計算とカット除去を考えている。
プロセスとは？
プロセスというのはコンピュータ科学用語である。私はこの用語にあまり馴染みがない。CPUというのは"Central Processing Unit"の略で、プロセッサともいう。このプロセッサに計算を行わせるひとつひとつの単位をプロセスという（という感じでいいのだろうか？）。複数のプロセスを上手いこと管理するのが並行プログラミングである。プロセス代数とかプロセス計算の体系というのはこの並行計算の体系で、複数のプロセス間の通信（communication）あるいは相互作用（interaction）をモデル化している。その意味でのプロセスである。
プロセスとスレッドの違いとか、また「並行」計算（concurrent）と「並列」計算（parallel）の違いとかもあんまりわかっていない私である。
プロセスとしての証明とは？
つまりこの論文は、CHIが証明とプログラムを対応させたように、証明をプロセスと対応させているのである。ここで証明というのは古典線形論理の証明で、プロセスはCCS（Calculus of Communicating Systems）やCSP（Communicating Sequential Processes）やπ計算といったプロセス計算の体系である。
直観主義論理のカット規則は非対称的だが、古典線形論理のカット規則は対称的である。これはどういうことか。後者のカットでは、左辺にカットされる命題があるシーケントのその命題（）に否定を付けて（
）右辺に持ってくることで、カットを否定に対して対称的な操作とみなすことができる。こういうことである。
カット除去をCCSやCSPのparallel composition＋hiding (あるいは restriction)、すなわち並行するプロセスを合成してそれらを繋ぎ（plugging）、チャネルを作ってインタラクションを発生させる計算、とみなすと、これが古典線形論理のカット除去手続きに対応するということらしい。（このあたりは6〜7ページで述べられている。）
カットが対称的であるため、どちらかが計算の主体になることはない。インタラクションであるよ。
この論文に至る経緯
この論文は、同じ雑誌（Theoretical Computer Science 135, 1994）のGianluigi Bellin & Philip Scott の"On the π-calculus and linear logic"という論文の前書き（の役割を果すもの）として付されたものである。
上述のようなCCSやCSPと線形論理との対応は"Computational interpretations of linear logic"という1993年の論文で述べられている。アブラムスキー先生はそれ以前から「プロセスとしての証明」というテーマでレクチャーをしていたが、論文という形にはなっていなかったらしい。線形論理とπ計算の対応もロビン・ミルナーと議論しつつある程度できていたらしい。ミルナーも線形論理をπ計算に翻訳する研究をしてアブラムスキー先生とやりとりをしていたようだが、出版はされていない模様。しかしこの研究がπ計算の改良に役立っているとアブラムスキー先生は読んでいる。
しかしこうした研究はちょっと停滞していた。そこへベリン&スコットが現れて先に進めた（彼らの論文では前段落の改良版のπ計算が使われている）。それに刺激を受けてのこの論文ということらしい。（こうした経緯は7〜8ページで述べられている。）
アブラムスキー先生はこの「プロセスとしての証明」の重要性を訴えているが、現在ではどうなったのだろう？
重要箇所の引用
My programme was to transfer the propositions as types paradigm to concurrency, so that concurrent processes, rather than functional programs, become the computational counterparts of proofs. This was the intention behind the "proofs as processes" slogan. The motivation was twofold:
- To lay the foundation for a useful discipline of typed concurrent programming.
- To provide the basis for a more structural view of concurrency, comparable to what we have for functional languages; and indeed to integrate the two paradigms into a single, unified theory.（6ページ）
私のプログラムは、"型としての命題"パラダイムを並行性へ持ち込み、関数プログラムよりも並行プロセスが証明の計算的対応物になるようにすることである。これが「プロセスとしての証明」というスローガンの背景の意図である。動機は二重になっている。
- 型付並行プログラミングの有用なdiscipline（訳しづらい）のための基盤を確立すること。
- 並行性に対してより構造的な見方をするための基礎を、関数言語におけるそれに匹敵する程度に与えること。そして二つのパラダイムを一つの理論に統一すること。
それを受けての私
直観主義論理のカットが非対称的だというのはわかるが、だとすると線形論理ではなく普通の古典論理でもプロセスとの対応はありそうである。じじつ論文には直観主義線形論理のカットも非対称的と書いてある（6ページ）が、そこからただの古典論理へ話がいかない。何故だろうか。線形論理ではない古典論理を計算と対応させるという発想がないのだろうか。しかしCPS変換を使った対応とかもある。この発見はもっと後だっけか。なので、「何故ただの古典論理ではなく古典線形論理なのか？」という点に注目してアブラムスキー先生の前の論文やベリン&スコット先生の論文を読みたい。やはり乗法的論理結合子が重要なのだろうか。"linear realizability algebras"という何やら難しそうな話も「プロセスとしての証明」で触れられている。
それと、当シリーズの起点となっている照井一成「相互作用としての計算」（現代思想2012年11月臨時増刊号）について。照井先生はCCSとπ計算の提唱者のミルナーと線形論理の提唱者のジラール大先生の名前は出しているが、それらの間の対応を確立したアブラムスキー先生には触れていない。何故だろう？ 多分たまたまというか紙幅の都合だろうが、何か隠された意図がある可能性もなくもなくもない。
