■

●日付を間違えた。今日の日記が昨日の日記で、昨日の日記が今日の日記。
●ちょっと前にツイッターで清水高志さんが取り上げていて面白そうだったので、照井一成「相互作用としての計算」（「現代思想」のチューリング特集）を読んでみた。チューリングが想定していたような（関数的な）「インプット→アウトプット」という形の計算ではなく、複数のエージェントの相互作用による「エージェント⇔エージェント」という形の計算を考えるという話。どこまで理解出来ているのかは心もとないけど。
≪（…）かつて単一の主体による地道で孤独な作業としてとらえられたきた計算が、複数の主体による共同作業へとイメージ・チェンジを果たす。このイメージ・チェンジにおいて注目すべき点は対称性である。チューリング機械にはヘッドとテープの区別があった。計算はヘッドが能動的に行うものであり、テープは記憶媒体として受動的な役割を果たすに過ぎない。（…）計算はいまやヘッドとテープの相互作用であり、どちらかが一方的に能動的であったり受動的てであったりするわけではない。≫
●まず、「計算する」ことと「証明する」ことは別のことではない、ということ。そして、その計算＝証明の基本を、「肯定式」から「矛盾律」に移行させることで、計算＝証明の対称性が得られること。
≪（…）“計算する”ことと“証明する”ことの間には、普通に考えられるよりもはるかに深い関係がある。たとえば「素数は限りなく存在する」というユークリッドの定理を考えてみよう。「素数が限りなく存在する」ということは、「どんな自然数が与えられても、それより大きな素数が存在する」と言い換えることができる。それゆえ、この定理を証明するためのもっとも自然な方法は、インプットとして何らかの自然数が与えられたときに、それよりも大きな素数を具体的に構成する方法（アルゴリズム）を記述することであろう。そのような証明からは、プログラムを自動抽出することができる（構成的プログラミング）。このようにして計算というファクターが証明に関わってくる。≫
≪証明と計算の関係をミクロのほうに向かって突き詰めていくと、論理推論とアルゴリズム構成法の関係に行き着く。なぜなら証明とは論理推論を積み重ねることにより、公理や仮定から結論を導く過程に他ならないからである。たとえば論理推論の基本をなすのは肯定式（modus　ponens）であるが、(…)肯定式は、A→Bを「AならばB」と読めば推論の法則であるが、「AからBへの関数」と読めば関数適用の規則でもあるのだ。かくして論理と計算はミクロのレベルでも対応する。この対応は論理学と計算科学の間に互恵的な関係をもたらし、やがて「証明とはプログラムであり、命題とはタイプである」というカリー・ハワード同型対応に結実するに至った。≫
≪(だが…)肯定式と関数適用との同一性を証明-計算関係の典型とみなす必然性も全くないことがわかる。ジラールはむしろ矛盾律(あるいはゲンツェンのカット規則)に証明-計算関係の根幹を求める。肯定式と矛盾律の何が一番異なるかというと、後者は前者に比べてはるかに対称的だということである。実際、二重否定律を受け入れてAと¬¬Aは同じものだと思うことにすれば、Aと¬Aとの役割は完全に交換可能である(AとA→Bの役割は交換可能ではない)。計算論的に考えても、矛盾律には“関数”と“値”の区別のような非対称性は全く見当たらない。矛盾律はあたかも“エージェント”Aと“エージェント” ¬Aの出会いを記述しているかのようである。そして二人の対等な“エージェント”が出会うことで“計算”が発生する。≫
●そのような矛盾律を基本とする計算=証明である「ゲーム意味論」において、「計算する＝証明する」ということがどのような過程であるのかについて。ここからが面白い。
≪ゲーム意味論では、これらの相互作用を二人のプレイヤー間で行われるゲームとしてとらえる。ゲームには勝ち負けがあるが、これはあまり重要ではない。それよりも重要なのは、各プレイヤーは相手プレイヤーの指し手に応じて次の一手を指すという対話性である。勝敗を無視して考えれば、ゲーム、たとえば将棋とは、二人のプレイヤーの協調作業により将譜を完成させる行為であると言うこともできる。これは複数エージェントの協調作業によって一つの計算を成し遂げるという現代的な意味での計算にぴったりと対応する。ゆえに論理をゲームとしてとらえることが、論理の背後に相互作用的な計算を見出すことにつながるのである。≫
≪古典論理の二値意味論では、各論理式は真か偽のどちらかを表すのであった。一方ゲーム意味論では、各論理式は何らかの二人ゲームを表す。たとえば将棋やしりとりなどの具体的なゲームを念頭においてくれればよい。(…)ただし各ゲームでは、先手・後手はあらかじめ決まっているものとする。具体例として、論理式Cは先手=羽生名人、後手=あなたとして対局する将棋を表すものとする。
論理式の否定をとる操作は、先手と後手とを入れ替えることに相当する。たとえば論理式Cが上のとおりの場合、論理式¬Cは先手=あなた、後手=羽生名人として対局する将棋を表す。すなわち否定という論理的操作を「ゲーム盤をひっくりかえす」こととして解釈するのである。ゲーム盤は二回ひっくりかえせば元に戻るから、どんなゲームについても¬¬A＝Aが成り立つ。≫
≪論理式の(乗法的)選言をとる操作は、ゲーム盤を二つ並べてゲームを並行的にプレイすることに相当する。≫
≪後手の勝利条件はA、Bどちらか一方のゲームで勝つことである。先手の勝利条件はA、B両方のゲームで勝つことである。引き分けはないものとする。≫
≪以上の解釈のもとでC∨¬Cという論理式を考えると、これは次のようなゲームになる。あなたと羽生名人は将棋盤を二つ並べて二局の対局を同時に平行して行う。あたなは一方の盤では後手であり、もう一方の盤では先手である。あなたは一方の盤からもう一方の盤へと自由に移ることができる。羽生名人はあなたが最後に指したのと同じ盤で手を指さなければならない。≫
≪羽生名人が一つの盤で一手指すたびに、あなたは別の盤に移って同じ手をまねればよい。すると羽生名人が一手返してくるから、あなたは元の盤に戻ってその手をまねればよい。これを続けていけば、「羽生対あなた」だったはずのゲームが「羽生対羽生」にすりかわり、あなたの将力に関係なくゲームは一勝一敗に終わるはずである。≫
≪同じことはどんなゲームAについても成り立つ。すなわちA∨¬Aというゲームにおいて後手は絶対に必勝法を持つのである。ゲーム意味論では、このように後手が必勝法をもつことによって命題は正当化されたとみなす。≫
●そしてこの先にはさらに驚くべきことが書かれている。
≪論理のもっとも基本的な法則である同一律は、ゲーム意味論においては、上で記述したようなものまね戦略の存在をもって正当化されるのである。≫
●つまり、羽生名人が羽生名人であるという「同一律」(羽生名人の再帰的な自己同一性)は、羽生(1)対羽生(2)の対決が必ず一勝一敗に終わることをもって正当化され、そのためには、ゲームの相手として媒介者=模倣者(後手)の存在が必要だということになる。これはほとんど精神分析の論理ではないだろうか。精神分析的に言えば、「わたし」は、ここで羽生名人の位置にも、「あなた」と呼びかけられる「私」の位置にも、どちらでもあり得る。というか、この二人の対話によって「わたし」となる。
●しかもここで、計算の過程が関数という孤独な内的過程(内省)ではなく、鏡像的な他者が相手とはいえ、他者との一手、一手の相互的なやり取りの過程としてある以上（それは、羽生(1)と羽生(2)の間にある時間的なズレとしても表現される）、いかに「必勝法がある」とはいえ同一律が揺らいでしまう不安をゼロにすることは出来ないのではないか。いや、ここで言われていることはそういうことではないかもしれない。同一律が、無時間的、一挙的に与えられるのではなく、時間的、対話的過程のなかで与えられるという違いがあるだけで、「必勝法」があるという事実において同一律に不安はないことになる（証明がなされた、となる）のか…。これはあくまで理論（証明の手続き）の話で、実際に計算を走らせるという話とは違うのかも。
●だがもし、実際に計算を走らせる場面を考えるとすれば、羽生名人が、羽生(1)と羽生(2)の間で成長したり退化したりする揺らぎがあるとすれば、あるいは模倣者が模倣し損なったとしたら、A∨¬Aは成り立たないこともあり得る。そして、計算が、閉じた系ではなく相互作用としてある場合、その計算自体をそのままもう一度やり直すことは原理的に出来ないのではないか（もう一度やり直すと、それは「また別の計算」になってしまうのではないか）。その「一度きり」の計算においては、命題「A∨¬A」が偽であったのか、それとも計算過程が間違っていたのかを、原理的には検証できないということになるのではないのだろうか。
●このような考えが、そもそも「間違った理解」から導かれているという可能性もあるけど。