お茶情の研究を覗いてみよう
このシリーズでは、情報科学科の学生が行った最先端の研究から、
国際学会で高い評価を得たものを紹介していきます。
第5弾:プログラミングを進化させる
紹介論文
シリーズ第 5 弾で紹介する研究は、石尾千晶さんが博士課程在学中に行った以下の研究です。
"Chiaki Ishio and Kenichi Asai, “Type System for Four Delimited Control Operators"
2022 年 12 月に開催されたプログラミングに関する国際会議 the 21st International Conference on Generative Programming: Concepts & Experiences (GPCE 2022) にて、採択された論文 15 件の中から最も優れた論文 1 件のみに贈られる Best Paper Award を受賞した論文です。
プログラミングの研究って何をするの?
コンピュータはプログラムを書くことで動かすことができます。今では、コンピュータやスマートフォンはもちろん、車、飛行機、家電など、身の回りのさまざまな機械がプログラムで制御されています。これらが誤動作しないように、適切に制御するためのプログラムを書くことが重要です。しかし、誰にでもミスはつきものですから、間違いのない完璧なプログラムを書くことは難しいです。このような状況の中で、「どうすれば、よりよいプログラムを書けるか?」ということが研究されてきました。
では、具体例とともに考えてみましょう。例として、ホテルの予約ができるウェブサイト(以下、予約サイト)があるとします(図1)。予約サイトには、さまざまなホテルが掲載されていて、その中から好きなホテルを選んで予約できます。以下の図のように、ユーザが予約サイトをブラウザで開いてホテルを選ぼうとしているとします。
ユーザは、ブラウザのタブ①で予約サイトを開き、ホテルを検索してその一覧情報を表示させます。一覧の中ではホテルAが良さそうだったのでホテルAの詳細情報を表示しました。その後、もう少し他のホテルも調べたいと思ったので、新しいタブ②を開いて予約サイトにアクセスし、ホテルの一覧情報を表示させます。別のホテルBも良さそうだと思ったので、詳細情報を表示させます。しかし、やはりホテルAの方が良かったので、前のタブ①に戻り、「このホテルを予約」というボタンを押しました。そのとき、どんな動作が想定されるでしょうか?
当然、ユーザの意図としては、ホテルAのページから「このホテルを予約」ボタンを押したので、ホテルAを予約したいはずです。しかし、予約サイトで最後に見たホテルの詳細情報はホテルBの情報ですから、誤ってホテルBの予約に進んでしまう可能性もあります。このような間違いを防ぐためには、予約サイト側が「ユーザーは、タブ①でホテルAを選択していた」という情報を覚えておいて、途中でタブ②に移動して戻ってきたときも、タブ①での操作を適切に続けられるようにすることが必要です。
予約サイトの例からも分かる通り、プログラムの実行の流れは、途中で中断されたり、途中から再開されたりすることがあります。そのような場合に対応するために、途中まで作業していた内容を覚えておいて、後で利用できるようにしておくことが必要になります。しかし、こういったプログラムの実行の流れを細かく制御するのは大変で、正確にプログラムを書くにはスキルが必要です。このような、「どうしたら、プログラム実行の流れを、間違うことなく制御できるか?」という課題は、プログラミングの研究で取り組まれていることの一つです。この記事で紹介する研究は、プログラム実行の流れの制御に関係する研究になります。
継続とは?
ここまでで、プログラム実行の流れの制御の必要性について、予約サイトの例で考えてみました。プログラム実行の流れを制御する方法にはいろいろありますが、その一つに「継続」というものがあります。継続とは、プログラム中でこれから実行すべき残りの処理を表すものです。先ほどの予約サイトの例では、タブ①で予約ボタンを押す前の段階では、「選択されたホテルに対して、そのホテルの予約をおこなう」というのが継続にあたります。
プログラムの中で継続を扱うための道具として、限定継続演算子というものがあります。限定継続演算子を使うことで、プログラムの中のある場所からはるか離れた場所に飛ぶというような命令を書くことができます。限定継続は、先ほど説明した継続の中でも、限定された範囲の継続のことを指します。つまり、「これから実行すべき残りの処理のうち、限定されたある部分」ということになります。例えばその「ある部分」に相当する何個かの命令を切り取って、あとで実行するようにする、といったことを指定できる仕組みになっています。
まずは、以下の式の例を使って、どのような操作ができるのか説明していきます。(図2)
上の式には、足し算(+)、掛け算(*)、関数の呼び出し( f x、関数 f に引数 xを渡して実行する)の他に、限定継続演算子S が含まれています。限定継続演算子にはいくつか種類がありますが、今回の例で使うのは shift/reset (シフト・リセットと読む)というものです。これらの二つの演算子は一緒に組み合わせて使われるものです。先に reset から説明すると、reset は〈…〉という記号で表され、継続の範囲を区切ります。このように reset によって範囲を限定された継続のことを「限定継続」と呼びます。一方、shiftは(Sk. … )のように表し、reset によって区切られた範囲までの継続を切り取ることができます。
図2の 1 行目では、括弧の一番内側の部分である、 (Sk. k 1 + k 2) の部分から実行されます。この部分は(Sk. …)という形の shiftの式ですから、一番近い reset 演算子までで区切られた継続を切り取ります。今回の例では、shiftの式(Sk. …)とreset の間にある「残りの処理(継続)」は「shift の式全体の計算結果はまだわからないが、その結果がわかったら、そこに3をかける」というものになりますから、穴あきの式([ ]*3)と表すことができます。この継続を 切り取って、k という変数に登録して後で使えるようにした状態が、図2の2行目に表されています。2行目に出てくる k = [ ]*3 という式は、k(x) = x*3 と書くのと同じ意味と思って構いません。この後は、k という関数を呼び出して四則演算の計算を進めていきます。3行目にでてくるreset演算子は、(もうshift演算子がないので)結果には何も影響しないので、無視して構いません。関数 k が2回呼び出されて、(k 1 + k 2) + 4 = (1*3 + 2*3) + 4 = 13 と計算することができます。
ここまでで、限定継続演算子の動きがイメージできたと思います。せっかくなので、四則演算だけではなく、同じ式を先ほどの予約サイトの例に置き換えて考えてみましょう。下の図3は、先の例の + 4 を reserve に、 * 3 を select に、 + を decide に、1と2をAとBに置き換えたものです。
図3の式の中に出てくる関数 reserve, select, decide は、それぞれ、「1つのホテルを予約する」、「1つのホテルを選択して詳細を表示する」、「2つのホテルの候補からどちらかに決定する」関数だと考えてください。また、変数AとBは、それぞれホテルAとホテルBを表すものとします。この図の式全体で、ホテルAとホテルBを選択して、その詳細情報を見ながら、どちらのホテルが良いか決めて、最後にホテルの予約をおこなう、という一連の流れを表しています。ここで大切なのは、「ホテルを選択する」というselect関数を限定継続 k として切りとっているので、select 関数の実行結果をもとに、ホテルを最終決定する前に、何度も処理を途中で中断させたり、続行させたりすることができるということです。
このセクションでは、プログラムの実行の流れを制御するための方法として、限定継続演算子について紹介しました。特に、図3では、この記事の冒頭で紹介したホテルの予約サイトの例を用いながら、shift/reset という演算子を使ってプログラム実行の流れを式に表すことができました。
この論文での提案内容
限定継続演算子を使えば、プログラムの処理の途中で中断したり、途中から再開したりすることができると説明してきました。では、途中で中断してしまった処理を、どこか遠く離れたところで再開しようとしたとき、本当にプログラムの整合性は取れているのでしょうか?今回、この記事で紹介する論文は、限定継続演算子を使ったプログラムに対して、「型」というものを使って整合性が取れているかどうか判断するための仕組みを作った、という内容になっています。
そもそも「型」というのは、コンピュータで扱うことができるデータの種類のことを指しています。例えば数学の教科書で y = ax + bという数式をみたら、きっと多くの人は y, a, x, b はそれぞれ実数だと想像するでしょう。一方で、 yi = axi + b という数式をみたら、きっと多くの人は i に対して「i 番目」という意味をもつ整数を想像するでしょう。このような、「実数」「整数」といったデータの種類のことを型と呼びます。そして、このような型の情報をもとにプログラムを検査し、プログラムが途中でよくない動きをしないかどうかを調べるシステムのことを、「型システム」といいます。プログラムを検査する仕組みの中でも、型システムは軽量で広く使われているものの一つです。
ここまでの説明では、限定継続演算子の代表例である shift/resetを例として取り上げていました。限定継続演算子には、これ以外にもいくつかの種類があります。この記事で取り上げた論文では、shift, control, shift0, control0 という代表的な 4 種類の限定継続演算子を利用しています(4 種類の限定継続演算子の違いに興味のある方は「付録」をご参照ください)。shift 以外の演算子は、より複雑な動作をするため、それに合わせて型システムもより複雑なものとなります。過去の研究では、shift/reset など個別の演算子に対する型システムは既に作られていますが、今回の研究ではそれを拡張して、4種類の限定継続演算子すべてに対応する型システムを作っています。
今後の展開
今回紹介した研究は、今後さまざまな方向に応用できる可能性があります。
まず、今回の研究は、4種類の限定継続演算子のための型システムの原理を示しただけで、プログラマが実際に使える形になっていません。将来的には、実際にプログラマが使えるようなツールを開発して、限定継続演算子の性質や、他のプログラムとの性能の比較などをすることで、より実用に近づけようとしています。
さらに、今回の研究のもっと先にある目標として、実行の流れを複雑に制御するようなプログラムを書きたいときに、誤りを自動で検知して教えてあげることで、プログラムを書く人の思考を助けるようなツールを構築したいと考えています。プログラムの間違いをできる限り早い段階で発見できるようになることで、重大な間違いや事故になる前に気がつくことができるかもしれません。また、よりプログラムを書く人の思考を助けることで、より多くの人がプログラムを書きやすくなるような手助けをしたいと考えています。
参考文献
- Chiaki Ishio, Kenichi Asai, Type System for Four Delimited Control Operators
https://dl.acm.org/doi/10.1145/3564719.3568691 - 石尾千晶, 浅井健一, 4 種類の限定継続演算子のための型システム
http://pllab.is.ocha.ac.jp/~asai/jpapers/ppl/ishio22.pdf - 型システム入門 プログラミング言語と型の理論
https://www.ohmsha.co.jp/book/9784274069116/ - shift/reset プログラミング入門
http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-j.pdf - 限定継続いろいろ (ブログ)
https://blog.miz-ar.info/2022/10/delimited-continuations/ - 型システム~プログラムの安全性を支える数学~(ブログ)
https://laborify.net/2018/12/09/igarashi type system/
付録:本研究で着目する4種類の限定継続演算子
限定継続演算子にもいろいろな種類がありますが、本研究では、限定されたある部分を「切り取る」演算子として特に使用される機会の多いshift, control, shift0, control0 の 4 種類の限定継続演算子に注目しています。
先ほど「切り取りを表す演算子の中から一番近いものを見つけて」ということを書きました。一方で、切り取りの演算子が二重三重になっている場合、直近の演算子による継続よりも外側にある継続まで視野に入れられることを考えます。これをメタ継続 と呼びます。メタ継続を考慮した限定継続演算子である shift0 や control0 では、内側の継続を切り取るか、外側の継続を切り取るか、といった判断は実行時になされるため、プログラムを実行するたびにシステムの動きが変わることがあります。もう少し具体的に言うと、shift0 や control0 では、継続を切り取る時に、直近の reset 演算子が残らないので、shift0 や control0 が呼ばれるたびに少しずつ外側の継続を切り取ることができるようになります。
なお、「プログラムを実行してみるまで、どこまで継続が切り取られるかがわからない」ことを、以下動的と呼びます。システムが動的であるということは、システムのその時の状態に応じて最適な動きを選択できることを意味しますので、うまく使えば「どのような状態でも状況を判断して効率よく動作するシステム」を構築することができます。
一方で、どのような処理の流れ(文脈)によって継続が切り取られたかを追跡することを呼び出し文脈と呼びます。呼び出し文脈を考慮した限定継続演算子である control や control0 においても、どこまで継続を切り取るかといった判断はプログラムの処理手順に応じて変動するため、プログラムの実行が動的であることがわかります。そのため、システムはどのように継続が切り取られたかを常に追跡する必要があります。
shift, control, shift0, control0 の 4 種類の限定継続演算子には、以下の図に示すような違いがあります。
メタ継続を考慮する shift0 と control0 では、上の図における青カッコがない場合を考慮することになります。呼び出し文脈を考慮する control と control0 では、上の図における赤カッコがない場合を考慮することになります。その結果として、これらの限定継続演算子では、プログラムを実行してみないとどのように継続が切り取られるかがわからない、ということを意味します。そして、例えば control や control0 では、プログラムから切り取ったある部分をどのような文脈で呼び出すかをシステムが追跡する必要があります。例えば shift0 や control0 では、切り取った部分の外側にある文脈をシステムが追跡する必要があります。これらの処理で追跡しているそれぞれの部分について、変数の型が何であるかを判断する必要があります。
問い合わせ先
大学へのお問合せはこちらをご覧ください〒112-8610 東京都文京区大塚2-1-1
TEL : 03-5978-5704
FAX : 03-5978-5705
責任者 : 情報科学科HP運営委員会 伊藤貴之
※このウェブサイトは情報科学科の学生によって制作されています。