船井情報科学振興財団

留学報告書

Long Thanh PHAM
Carnegie Mellon University
June 29, 20202019 年 9 月より Carnegie Mellon University (CMU) で Computer Science の博士課程に取り組んでいるファムです。今回の報告書では 2020 年前半を振り返ります。

1

研究

現在取り組んでいる研究プロジェクトは、resource analysis に関するものです。これは、与えられた functional programs がどれだけの資源（e.g. 時間やメモリー）を費やすかを静的に解析・算出するという分野です。この分野の中でも、私が今研究しているのは、automatic amortized resource analysis (AARA) という、type theory を使った resource analysis です。これは、私の指導教授（Jan Hoffmann）の指導教授であるMartin Hofmann 教授（注意：綴りが似ています）が発明し、それを Jan Hoffmann 教授が博士課程中に大きく発展させました。
Turing machines の決定不可能性のため、AARA は全ての場合において、資源量の上限を自動的に算出することができるとは限りません。加えて、以前は AARA のユーザーはどのような場合において AARA による解析が可能なのかを事前に知ることができませんでした。現在の研究は、AARA での解析可能であるための比較的シンプ
ルな suﬀicient condition を提示し、それが実際に AARA においての typability を意味するという証明を目指しています。
2019 年 11 月に論文の前置きとなる結果をまとめたレポートを終え、それ以来、論文の中心となるような問題に取り組んでいました。2020 年 1 月に指導教授のアドバイスで、プロジェクトの方向を少し変えました。最初は一番単純なケースである linear
potential に専念し、次に univariate potential に移り、最後は一般化されたケースである multivariate potential に取り組みました。幸い、論文にまとめられるだけの結果が揃い、現在、Computer Science Logic (CSL) という学会に提出予定の論文を執筆中（締め切り数日後）です。

2授業

2020 年春学期は、Computational Type Theory と Computer Networks を履修しました。
Computational Type Theory は、type theory の権威である Robert (Bob) Harper 教授が担当でした。
教科書・論文では説明されていないような、constructive/computational1

type theory の土台を教えてくださり、今までの私の世界の見方を変えるような新鮮な授業でした。内容が新鮮過ぎて、授業のペースは速く感じました。この授業を経て、もう一度 computational type theory 関連の論文を読むを理解できるのですが、この授業で得た知識・理解無しで論文を読むことは到底無理だと感じました。Computational
type theory の分野は私の現在の研究には直結しませんが、プログラミング言語理論の博士課程学生である以上、Bob Harper 教授の授業は受講すべきですし、Computational
Type Theory のコースは type theory の根本的な理解を深めてくれます。試験や宿題が一切出されないので、自主的に復習することが求められるコースでした。
Computer Networks に関しては、学部時代にネットワークの授業を正式に受講したことがなく、今やインターネットは日常生活に浸透しているため、本格的にネットワークを勉強したいと予てより思っていました。加えて、ネットワークと私の専門であるプログラミング言語理論の交差する分野において興味深い研究が最近なされているというのも、このコースを受講した動機でした。
コース担当の Justine Sherry 教授の教える上手さには感激しました。授業はセミナー形式であり、課題として論文を読み、毎回の授業では各学生に課せられた論文をプレゼンし、最後にディスカッションするというものでした。今までネットワークの授業を取ったことがない人のために、ネットワークの基礎は学期の前半に教科書を使って個人で自主的に学び、週一回の補修で teaching assistant (TA) が重要なコンセプトを説明してくれました。グループでの研究プロジェクトもあり、成果をまとめた（模擬）論文は学期末の（模擬）学会で採択されました。

3

生活2020 年 1 月にペンシルベニア州の自動車免許を取得しました。ピッツバーグでは公共バスが整っており（と言っても時刻表通りの運航ではないが）、CMU への通学や歯科医を訪れる際はバスを使っています。そのため、普段の生活では自らハンドルを握ることはないのですが、車をレンタルしなければまともに移動できないようなアメリカ国内の場所に学会・観光などで行った場合、アメリカの免許を持っていれば便利だと考えました。と言いつつ、実際は、昔、テキサスで一年間働いていた父が熱心に免許取得を勧めたというのが、私の免許取得の動機です。当時は、車がないとテキサスでの生活は厳しかったようです（街にもよると思いますが）。私は日本国内の免許を既に持っており、それに付随する形で国際免許もあります。しかし、ペンシルバニア州に一年以上住む場合、一年目以降は国際免許ではなく現地の免許を使うことを求められています。
12 月の下旬に筆記試験の準備のために交通ルールをまとめたマニュアルを読み、1 月上旬に筆記試験を受けました。その後、アメリカでの路上運転に慣れるため、一度、実際に車をレンタルし、この機会を利用しバスでは遠すぎるような場所にある美術館（The Andy Warhol Museum）に行きました。日本と違い、アメリカでは自動車は道路の右側を通ります。右折の際、ハンドルを右方向に一気に切るということは日本ではすることはないので（日本での右折は、ハンドルをゆっくり切るため）、少し戸惑いました。最初は、レンタカーで技能試験に臨むつもりでいましたが、調べてみると、レンタカー会社がそれを許可していない場合が多い上、試験官がそれを咎める可能性（たとえレンタカー会社の許可がある場合でも）があったので、最終的には、一2

番不安要素の少ない、民間の教習所での試験を選択しました。試験直前の練習込みで300 ドル近くかかりました。その教習所の先生に聞いたところ、アメリカでは、親が子供に運転を教え、その後、親の車を使って州政府管轄の試験場で技能試験を受けるのが一般的らしいです。民間の教習所は、試験場での技能試験を中々パスできない場合、専門の指導員による追加の練習を提供するのが主な目的です。

4

コロナウィルスの影響
1. コロナウィルスの影響で、大学のキャンパスは 3 月中旬に閉鎖しましたが、授業はスムーズにオンラインに移行しました。
2. 今まで気軽に教授のオフィスに寄ってディスカッションをするということが、ロックダウンの影響でできなくなりました。また、コンピューターサイエンス学科全体において、内部・外部の研究者によるセミナーもほぼ皆無になったので、他の研究分野の知見を広げる機会を失ったのは残念です。
3. ロックダウンが始まった最初の頃は、ノートパソコンでも自宅で仕事できるだ
ろうと高をくくっていましたが、一週間して、背中と首への負担が想像以上に大きいことに気付きました。大学のオフィスにある私個人のモニターを自宅に持ち帰るという手段もあったのですが、既にキャンパスは出入り禁止になっていました。結局、モニター、キーボード、そしてプリンターを購入することになりました。
4. 2020 年 7 月にアメリカ、オレゴンで開催される予定のプログラミング言語理論に関する 2 週間のサマースクール（博士課程学生向け）がキャンセルされました。参加目的として、単に様々な大学からくる研究者による授業を受けるだけでなく、将来、職場の同僚になる可能性のある人達とネットワークを築くというのもあります。
5. 2020 年 6 月に、本来イギリス、ロンドンで開催されるはずの Programming
Language Design and Implementation (PLDI) という学会がオンラインになり、無料参加できました。

5

気付き

イギリスのオックスフォード大学での学部時代の授業と比べ、CMU の授業は面白いものが多く、学部生が羨ましいとつくづく感じます。まず CMU のコンピューターサ
イエンス学科の大きさ、各専門分野の教授の多さは目を見張ります。そのため、理論・応用の両方において幅広い分野のコースが提供され、コースのレベルも様々なので、学部生でも知的好奇心の赴くままに広く探検したり深く掘り下げたりすることが可能です。加えて、研究者としてだけでなく、教育者としても優れた教授が比較的多くいます。勿論、CMU に在籍しているのはまだ一年だけであり、統計的に意味のある結論は出せませんが、それでも CMU の提供するコンピューターサイエンス教育のレベルの高さには圧巻されました。
3

オックスフォード大学は理論（e.g. 圏論、量子コンピューティング）に偏っている印象を受けます。ただし、それはそれで抽象的な思考力を育てるという長所もありますし、どの大学でも所属する研究者の研究分野によって提供できる学部教育が異なるというのは当然なのでしょう。CMU のように偏りのない教育を提供できるというのは、難しいはずです。

4