山田倫大

オックスフォード大学
２０１７年

船井情報科学振興財団

６月

第９回留学生レポート

The only tangible reality about sense is the way it is written, the formalism;
but the formalism remains an unaccommodating object of study, without
true structure, a piece of soft camembert. (by J.-Y. Girard)
英国オックスフォード大学計算機科学科に所属しています、山田倫大です。いよいよ最終学年も終盤を迎え、博士論文を仕上げる段階となりました。

統一的な視点自分の場合、既に４つの独立した論文があるため、博士論文を書く作業は（大まかに言って）これらを纏めて１つの読み物として仕上げるということになります（４つの論文それぞれが博士論文の１つの章に対応）。故に、これから新しい問題を解くということはほとんどなく、最初の導入の章を書き足す、記法を統一する、重複している箇所を取り除く、といった編集作業が中心となります。
この中で最も骨が折れる作業は導入の章を推敲することです。何故ならば、先述した４つの論文はそれぞれ独立して書かれたものですが、博士論文が１つの読み物として成立するためには、導入で統一的な視点を与えることでその後の４つの章が繋がりを持ち１つの物語を紡ぐようにしなければならないからです。それぞれの論文が全く関連を持たない場合は１つを選びこれを少し発展させることで博士論文とするということもできますが、当然その場合は博士論文の「スケール」が小さくなります。故に、半分自己分析にも似た形で、４つの論文の背後にある、自分の大局的な研究興味について考えました。これは数学的・技術的なものではなく、むしろ哲学的・概念的なものであり、特に研究の動機がその核となります。
蓋を開ければ、その答えは既に自分の中にありました。振り返れば、研究課題の設定に２年を費やして自分の納得のいく問題を探したこと、また指導教授と数学的な問題のみならず哲学的な問題についても議論したことで、自分なりの大局的な視点が形成されていった様に思います。４つの論文のトピックはそんな自分の視点!1

が無意識のうちに選んだとも考えられます。これを明確にする作業は博士論文のためのみならず、自分の今後の方向性を考える上でも非常に有意義でした。

論理と計算の数学的かつ構文に依らない定式化
明確になった自分の博士論文のテーマは：「論理と計算の数学的かつ構文に依らない定式化 (mathematical and syntax-independent formulation of logic and computation)」、及び「論理と計算の中の数学 (mathematics in logic and computation)」です。簡潔に背景を説明します。非常に大雑把に言えば、数学は様々な現象や概念（例えば集合、数、空間、変化など）を抽象的に定式化し、その性質を厳密に調べる学問です。こ
こで大切な点は数学的概念の多くは抽象的であり、これによって物事の本質のみを厳密に捉えることが可能であり、また数学を現実世界の問題の多くに適用することが可能となります。この帰結の１つとして、数学的概念は基本的にその記法に依存しないということが言えます。例えば自然数（０、１、２、・・・）は１０進数、２進数、１進数など、どの様な記法で書こうが、そこに本質的な違いはありません1。しかし、論理や計算では多くの概念が形式言語2によって記号的に定義されます（形式体系や関数型プログラミング言語など）。これらの定義やその性質の証明は厳密であるという点では数学的ですが、記号的な概念は瑣末な詳細を含むため十分に抽象的であるとは言えず、背後にある数学的本質を捉えることに対しては不向きです3。また概念的に言えば、伝統的な数学では記号はあくまで何かを表すためのものであり、それ自体は意味を成さないという立場を取ります4。例えば「プログラムの数学的な意味付け」を主な動機としてダナ・スコットとクリストファー・ストレッチーが７０年代にオックスフォードで表示的意味論（プログラムを数学的な概念、特に集合と関数、によって捉える）を考案し、歴史的な業績を残しました。しかし、表示的意味論は主にプログラムの計算結果に焦点を当てたものであり、その途中の計算過程を捉えることはできません。これを受けて、フランスの論理学者ジーン・
ヤビス・ジラードは計算過程を sense とした上で、次の様な言葉を残しています：
The only tangible reality about sense is the way it is written, the formalism; but theformalism remains an unaccommodating object of study, without true structure, a pieceof soft camembert.
1 自然数の集合は帰納的に「ゼロ」とそれぞれの自然数の「次の数」によって定義されます。
2 数学的に厳密に定められた言語（文字列の集合）を形式言語と呼びます。
3 例えば異なる形式体系が圏論的な意味で全く同じ構造を持つということがあり得ます。
4 対照的に証明論や計算機科学では記号的な概念が第一義的であるという立場を取ります。

!2

彼も記法に依存しない数学的な計算過程の定式化の重要性を説いており、それが彼の代表的業績の１つ Geometry of Interaction (GoI) の主な動機となっています。
纏めると、（伝統的な）数学の視点からすると、論理や計算における記号的な概念はあくまで数学的定式化の対象であり5、それ自体は十分に数学的・抽象的ではないということです。しかし論理や計算は比較的新しい分野であり、これらに関する数学は未だ発展途上です（先述した表示的意味論や GoI はこの分野ための新しい数学）。１つ目のテーマの動機はここにあり、論理や計算における諸概念を記法に依らない形で数学的・抽象的に捉えたいということです。特に博士論文では計算過程、高階計算の計算可能性、依存型、及び計算的同値、といった概念を捉えることを目指します。また、そこで導入される概念それ自体が数学的（特に代数的）な構造に富み、その探求が２つ目のテーマに当たります。次回のレポートではこれらの説明をしたいと思います。

ネロとウルヴァリンの定理
話題を変えて、少し日常生活の話をします。今年のオックスフォードの天候はおかしなことになっています。これまでの４年以上の留学生活の中で最も変です。先週
はとても暑く、気温が３０度くらいまで上がりました。３０度と言えばそれほど暑くない様に思われるかもしれませんが、こちらの建物はそこまでの気温を想定して建てられていないため、冷房がなく、また熱が籠ります。そのため部屋の中は温室状態で、日中の室内はおそらく３０度代後半、日が沈んでも室内の気温はあまり下がらずとても寝苦しいです。慌てて街に扇風機を買い出しに行くと、どこの店も売り切れ状態だったので、某オンラインショップで扇風機を２つ注文しました。ところが今週は一気に最高気温が２０度以下まで下がりとても寒いです。不要となった扇風機２台だけが部屋に残り、何となく心も寒いです。
一方、先週まで自宅もオフィスも日中は非常に暑かったため、毎日の様にカフェに通いました。大学と街が一体となったオックスフォードでは至るところにカフェがあります。自分のお気に入りは中心街の本屋「ウォーターストーンズ」の３階にあるカフェです（下の写真参照）。大きな窓の外に見える景色が綺麗で、疲れた時に窓の外に目をやると良い気分転換になります。また客層も落ち着いているため騒々しくなく、仕事も捗ります。何度も通っているうちに店員さんと仲良くなり、コーヒーを無料で頂いたりスタンプ・カード（スタンプがたまるとコーヒー１杯が無料）
5 この点において論理・計算と物理は類似していると言えます。一方、前者はそれ自体が（記号的ではあるものの）数学的に厳密ですが、後者（物理現象）は形式的ではないという違いがあります。
!3

を一度に５個くらい押して頂きました6。また、そこで知り合った歴史学専攻の学生に（これまで訪れたことのない）Magdalen College でのディナーに招待してもらうということもありました。災い転じて福となす、ということでしょうか。
場所を変えることは研究に関してもプラスに働くことがあります。自分の場合、（間違いがあってはならない）厳密な作業をする時には自宅か研究室を選びますが、新しいアイディアや閃きを探している時はカフェを選ぶことが多いです。その様な時には散歩も有効です。余談ですが、今年２月中旬、１週間くらい考えていた問題がその週末にカフェ「ネロ」を訪れている際に一気に解けました。その前日にはX−メンのウルヴァリンに関する映画「Logan」を観ていました。嬉しさのあまり、その定理を「ネロとウルヴァリンの定理」と名付けました7。ネーミングのセンスは置いておいて、時々普段と異なる場所で研究を行うことをお勧めします。

今後の予定博士論文と並行して、ジャーナルへの論文投稿と次のアカデミック・ポジション探しをしているため慌ただしい時期となっています。次のレポートではこれらに関して良い報告ができる様にしたいと思います。なお、前回のレポートで約束していたマルティンレフ型理論の計算的解釈については次回に譲らせて下さい。

街の中心街にあるウォーターストーンズ・カフェ

6 他のお客さんには秘密にしておいて下さい。
7 さらに余談ですが、数年前に τ（タウ）と π（パイ）が文中に出てくる定理を証明した際に、漫画「ドラゴンボール」が好きな友人にこれは「桃白白（タオパイパイ）の定理」だと紹介しました。
!4