2021年度振り返り
2020年度に引き続き、今年度も大きくは初心者プログラミング教育と限定継続演 算子の研究の２本立てで研究を進めています。今年は、初心者プログラミング 教育の方から書こうと思います。初心者プログラミング教育
ゲームプログラミング教材の作成
今年、これまでと大きく異なる研究となったのは、ゲームプログラミングの教 材を作ったことでしょう。これまで OCaml Blockly を使えば、初心者でもい ろいろなプログラムを作ることができると思ってはいましたが、その用途は情 報科学科の関数型言語の授業と LA のゲームプログラミングの授業だけでし た。これを「誰でもそのサイトを読んで遊びさえすれば、いろいろなプログラ ミングを学ぶことができる」ようにしようと、ゲームプログラミングのチュー トリアルサイトを作りました。
このサイトを開くと、基本的なところから手取り足取り操作方法を教えてもら いながら、ゲームプログラミングを学ぶことができます。操作方法の説明は、 文章でも書いていますが、実際にチュートリアルを動かしてみると、吹き出し が出てきて、それに従って操作しさえすれば誰にでもできるようになっていま す。これを使えば、
まだユーザテストをできていないので使いやすさは未知数です。来年度になっ たらユーザテストをして、そこでのコメントをもとに改良していきたいと思っ ています。また、今回はゲームプログラミングでしたが、中高の数学を学べる ようなサイトなど、より多くのサイトを作っていきたいです。興味のある人、 大募集中です。
対戦ゲームフレームワークの作成
LA のゲームプログラミングの授業では単独ゲームを作っていますが、今年は対戦ゲームを作れるようにライブラリの拡張を行いました。使っているUniverse ライブラリは、もともと対戦ゲームもサポートしていましたが、 Unix のソケット通信を使っていて、必ずしも使いやすいものではありませんでした。それを web ベースに改良して、誰でも比較的、簡単に対戦ゲームを作れるようにしました。
これを使って情報科学科向けの集中講義を開いて、皆で対戦ゲームを作っても 良いと思っています。また、今はまだテキストエディタでプログラムを作らな くてはなりませんが、これを OCaml Blockly とつなげると、初心者でも対戦 ゲームを作れるようになるのではないかと夢はふくらんでいます。さらに、対 戦ゲーム用のチュートリアルサイトも作れると良いですね。
OCaml ステッパのモジュール対応
関数型言語の授業で使っている OCaml ステッパ、昨年、モジュールのサポー トを開始しましたが、今年、それをまとめることができました。ステップ実行 というのは、プログラムを一歩ずつ実行していくことですが、そこにモジュー ルが入ってくると、モジュールの中で定義されたものなのか外で定義されたも のなのかを区別しなくてはなりません。例えば、Tree モジュールの中の insert 関数は、Tree モジュールの中にいるときは insert と書けば良いです が、モジュールを出たら Tree.insert と書かなくてはなりません。このよう な「変数の出入り」を上手に扱うことでステッパを定式化することができまし た。
来年度の関数型言語の授業では、この新しい OCaml ステッパを使用予定です。 さらに、このステッパを web 対応した上で OCaml Blockly と組み合わせて、 OCaml Blockly で作ったプログラムをそのまま web 上でステップ実行できる ようにならないかと思っています。関数型言語の授業、ますます便利になって いきます！
Mikiβ の相互再帰サポート
次第に内容が「初心者プログラミング」を離れつつありますが、今年は Mikiβ の相互再帰サポートも行いました。Mikiβ というのは、研究室で開発 している「型システムの定義を与えると、対応する GUI を作ってくれる」と いう夢のようなプログラムです。プログラミング言語の型システム以外にも、 自然演繹の証明木用の GUI も作ることができます。しかし、これまでは型の 相互再帰をサポートできていませんでした。それを generic プログラミング の考え方を取り入れることで扱えるように改良しました。
技術的には、OCaml の GADT (generalized algebraic data type) を使った り、一部、動的な型付けが必要になったりと、いろいろ面白いことがありまし た。現在は、型システムの定義を OCaml プログラムの形で与えなくてはなり ませんが、さらに、それを web インタフェースでできるようにしようと考慮 中です。これができると、好きな型システム（証明体系）を web 上で簡単に 作れるようになります。戸次先生の課題も、そこでやると楽になるかも（！？）。
限定継続演算子の研究
４種類の限定継続演算子に対する型システム
昨年度は、４種類の限定継続演算子の中から control/prompt に対する最も一 般的な型システムを構築しました。今年度は、この研究をさらに進めて、４種 類の限定継続演算子全てに対する最も一般的な型システムを構築しました。こ のうち３種類についてはすでに知られているものでしたが、最後のひとつはこ こで新たに作られたものです。また、これとは別に４種類の限定継続演算子に 対する抽象機械も導出しています。
これらの研究により、４種類の限定継続演算子全てについて CPS による意味 論と抽象機械、型システムを確立できたと考えています。これで、ようやくさ らに進んだ話題について研究を進めていくことができるようになります。手始 めに、限定継続演算子の階層について検討を始めたいと思っています。
代数的効果とハンドラの基礎理論
４種類の限定継続演算子の研究は、代数的効果とハンドラの基礎理論にも大き な影響を与えています。同様の考え方で、代数的効果とハンドラについても多 くのことがわかるのです。今年度は、実際に代数的効果とハンドラに対する 筋のよい CPS 意味論と抽象機械、型システムを与えました。これにより、こ れまでどうもわかりにくかった代数的効果とハンドラが扱いやすくなることを 期待しています。
CPS 変換の正当性の証明
一方、各種の CPS 意味論を定義すると、その正当性が気になります。昨年度 に引き続いて、限定継続演算子の中でも control/prompt について、その CPS 変換の正当性の証明に取り組みました。しかし、どうしても最後の一歩を乗り 越えることができずに、いまだ証明は完成しないままです。定理証明系を使っ た証明は、テストでは得られない 100% の絶対的な正当性を得られますが、そ の分、証明は難しく、そこを切り崩せないと行き詰まることもあります。
乗り越えられていない最後の一歩は、control/prompt の CPS 変換に出てくる 「呼び出し文脈」と呼ばれるものに関する性質です。「論理関係」と呼ばれる ものを使って証明することになるのだろうと思いますが、いくら考えてもうま くいかず、そもそも論理関係を使った証明はどのようにするものだったかとい う基本に立ち戻らざるを得なくなりました。
現在は少し休憩中で、証明は止まったままですが、これはあきらめたというこ とではありません。むしろその逆で、鋭気を養って、基礎から勉強し直して、 来年度には最後の一歩を乗り越えたいと考えています。
reflection の証明
今年度は、さらに理論的な研究として、４種の限定継続演算子の中から shift/reset を取り上げ、その型付きの CPS 変換が reflection と呼ばれる 良い性質を持つことの証明を行いました。これは高度に理論的な話題で、まだ 完全に証明が終わってはいないのですが、地道に論文をひとつひとつ読み解く ことで、その基礎が固まったと思っています。
ここでの難しさは、証明の方法ではなく、そもそもどのように変換を定義した ら良いのかという部分です。このように定義すると、ここでうまくいかない、 また別の方法で定義すると、別の場所でうまくいかない、という感じになり、 最後までうまくいくことを見通して定義するにはどうすれば良いかを考えるこ とになります。この手の研究では、細かいところまで含めて全てを着実に一歩 一歩進めていくことが大事です。今年度の研究で、十分に基礎は固まったと思 うので、これも来年度に大成させたいと考えています。
正当性の証明から正しいコンパイラを導出
少し変わったトピックとして、今年度は「コンパイラが満たすべき性質」から 「正しく動作するコンパイラ」を導出するという研究も行いました。コンパイ ラが満たす性質というのは「コンパイル結果は、もとのプログラムと同じ動作 をする」ということですが、これを定理証明系 Agda で表現します。その上 で、この性質の証明を考えることで、正しく動くコンパイラを導出しようとい うものです。
なかなか面白い考え方で、かつエレガントなので、当初は、この枠組を使って 限定継続命令用の正しいコンパイラを導出しようと考えていました。ところ が、詳しく見ていくうちにうまくいかないところが現れたため、限定継続用に 応用するのは難しそうということがわかってきました。そのため、この研究は 中断中ですが、でも、背景にある考え方を深く学ぶことができました。こうい う経験は、研究内容が変わっても役に立ってくるものです。