2022年度振り返り
昨年度の振り返りを書いてから、もう一年、たちましたか。早いですね。 今年度の成果は、何と言っても懸案だった reflection の証明が 完成したことでしょう。そこから書き始めようと思います。限定継続演算子の研究
reflection の証明、完成
昨年度の振り返りでは懸案として残っていた shift/reset に対する型付き reflection の性質の証明、完成しました（！）。shift/reset のような限定 継続演算子の意味は、それを継続渡し形式（CPS 形式）に変換（CPS 変換）す ることで得られます。reflection というのは、その変換についての性質で、 一言でいうと「変換前と変換後には一対一の対応がある」ということです。 この手の高度に理論的な研究ではよくあることですが、出来上がってみると、 すでに存在していた型なしの reflection の証明ととても近いものとなりまし た。なので、最初から全てを理解できていたら、もっと楽にゴールできていた かも知れないのですが、なかなかそうはいかないのが現実です。 でも、苦労した甲斐があって、reflection の性質と、そこに出てくる変換前 後の言語、そしてその中間に位置するカーネルと呼ばれる言語の間の関係が 「とても」よく理解できました。これは、大きな財産と思います。特に、カー ネル言語の意味を理解できたのは、次に述べる CPS 変換の正当性の証明や、 今後、考えていきたい選択的な CPS 変換などにも影響を与えそうです。
control/prompt に対する CPS 変換の正当性の証明は未完
一方、もうひとつ残っていた懸案事項は持ち越しです。限定継続演算子の中で も control/prompt と呼ばれるものについて、CPS 変換の正当性の証明を試み ていたのですが、こちらは完成しませんでした。前期の大学院の授業をこの問 題の解明に当てて、ひとつずつ順番に説明して理解を深め、各部の証明を皆に も手伝ってもらいながら、解決を目指したのですが、ゴールにはたどり着けま せんでした。 でも、その過程で理解は確実に深まったと思います。（途中で、ぼくが 2006 年に書いた関連する論文の証明が間違っていたことも判明しました（汗）。） 特に、ゴールに辿り着くためには、もう一度、CPS 変換をしてあげないとだめ そうという見通しを得られたのは大きかったです。現在は、まずはこの方針に 従って 2006 年の証明を正すことから始め、それを control/prompt の CPS 変換の証明につなげていきたいと考えています。その際、reflection の証明 で得られた理解も役に立ちそうです。
４種類の限定継続演算子に対する型システム
昨年度の振り返りで、４種類の限定継続演算子全てに対する最も一般的な型シ ステムを構築したことを書きましたが、この成果はその後、国際学会に採択さ れ、最優秀論文賞を受賞しました。 https://2022.splashcon.org/home/gpce-2022#Best-Paper-Award ここでのメインの成果は、もちろん４種類の限定継続演算子全てに対して型シ ステムを作ったことですが、それに加えて、これまでに考えられていた種々の 限定継続演算子に対する型システムとの比較をきちんと行ったことも大きかっ たかなと思います。この比較により、今回、提案している型システムが実際に これまでの型システムを包含していることがわかり、さらに選択的な CPS 変 換や CPS 階層に対する型システムなどにもつながっていく成果になったよう に思います。
shift/reset を使ったプログラムの性質の証明
上記の研究に加えて、今年度は新しい試みとして、限定継続演算子 shift/reset を使ったプログラムに関する証明を試みました。手始めに、 shift/reset を使った reverse プログラムを例にとって、実行前後でリスト の長さが変化しないことを証明してみました。ポイントは、mondaic にプログ ラムを書いて、途中の式について成り立つべき性質を書いていくところです。 考えなくてはならないところは残っていますが、意外ときれいに証明が書けた かなと思っています。 shift/reset を使ったプログラムの性質の証明なんて誰もしていないかと思っ たら、驚いたことに PPL の発表で複数、似たようなことをしている人がいる ことを発見しました。少し、スピードを上げて研究を進めていかなくてはなり ませんね。 こんな感じで、相変わらず、限定継続演算子の研究には力を入れています。昨 年、11 月の研究室 20 周年記念パーティのときにも話しましたが、 限定継続演算子の世界をクリアにすることは、 研究室の使命と考えて頑張って進めています。
初心者プログラミング教育
研究室のもうひとつの柱である教育系についても 引き続きいろいろ進めています。OCaml ステッパの ref 対応
昨年度の研究で OCaml ステッパのモジュール対応を行いましたが、今年度は、 さらに ref のサポートを行いました。ref というのは、関数型言語の授業の 最後で扱う「書き換え可能なセル」です。これのサポートは、それほど難しく はなく、基本的には「その時点でのメモリの状況」を保持するようにするだけ です。でも、それをどうやってユーザに見せるのか、また、ステッパをインク リメンタルにするにはどうすれば良いのかで工夫が必要でした。 ref がサポートできたことで、関数型言語で扱う構文はほぼ全部、サポートで きたことになります。これで、ステッパの開発は一段落です。実際に授業の中 で、学生が最短路問題をステッパで動かしながらデバッグしているのをみると、 なかなかの完成度になってきたなと感じます。 今年は、さらにステッパのデモページも作りました。web インタフェースがあ ると宣伝もしやすくなります。ところが、このデモページ、プログラムの色付 けのところでとても苦労させられました。ステップ実行の結果は、もちろん、 きれいにシンタックスがハイライトされた形で表示したいわけですが、色をつ ける部分の指定が猛烈に面倒なのです。正規表現を使って指定するのですが、 そもそも対応する括弧など正規表現では表せないものに色をつけているので、 作った正規表現は読めたものではありません。何年かしたら、何が書いてある のか全くわからなくなりそうで恐ろしいです。（これ専用の領域専用言語を設 計すると良いのかもしれません。）
Mikiβ の web インタフェース
Mikiβ で表示する証明木の定義は、これまで OCaml で書かなくてはなりませ んでしたが、ついにその web インタフェースが完成しました。これで、ユー ザは OCaml のプログラムを一切、書くことなく証明木の定義を書くことがで きます。これで、各種の型システム（証明体系）をどんどん作れるかと思いき や、意外と web インタフェースでの定義の入力は面倒であることがわかって きました（笑）。その辺、もっと使い込んで、どうなっていたら使いやすいの かを洗い出していきたいところです。 また、予想された通り、tex で出力してほしいという要望があちこちから出た ので、それの実装も進めています。来年度は、より使いやすくするのを目指し て完成度を上げて、うまくいったら戸次研で使われている CCG の証明木とか も載せられるようにならないかと目論んでいます。
OCaml Blockly を使った教材
昨年度から作っているゲームプログラミングのチュートリアルのページは、 １年生を募って、実際に使ってもらうという実験を行いました。自習だけで全 てを理解してもらうのはちょっと難しかったのですが、あれこれ手助けをしな がら進めたら、なんとかゲームを動かすところまでいくことができました。 これ、理解が難しかった原因は、OCaml Blockly の機能の問題ではなく、そこ に書かれている文章がどのくらいわかりやすいかという問題でした。つまり、 読ませる文章を上手に作る必要がある、別の言い方をすると作家になる必要が あるようです。これ、なかなかハードルが高くて、どうしようかと考えあぐね ていますが、めげずに色々と手を加えて、来年度もまた実験ができたらと思っ ています。 これとは別に、今年度は中学１年生の数学で出てくる一次式を題材にして、そ れを OCaml Blockly で遊びながら学ぶページも作成しました。まだ、各単元 ごとにばらばらに作っている状態ですが、これを上手にまとめてひとつのサイ トにできたらと思っています。ここでも、うまい文章を作る必要がありそうで す。誰か、物語を書くようにシナリオを書いてくれないかなぁ。
対戦ゲームの授業
最後に、これは研究室の活動というわけではないですが、２年生を対象にして 対戦ゲームを作る授業を久しぶりに行いました。15 名ほどの２年生が参加し てくれて、６チームに分かれていろいろな対戦ゲームを作りました。 やはり、実際に使ってもらうと違います。Universe ライブラリの不具合も見 つかり慌てることも多々ありましたが、おかげでライブラリの完成度は上がっ たように思います。また、デバッグがしにくいなどの問題点もみつかりまし た。各時点での世界の状況や、送られたメッセージを見られるようにするな ど、いろいろな解決法を探るのは面白そうです。