2023年度振り返り
今年度も教育系と理論系の２本建で進めてきました。今年度は教育系から書こ うと思います。初心者プログラミング
ゲームプログラミングチュートリアル拡充
一昨年度から作成しているゲームプログラミングのチュートリアルは、ひと段 落を迎えて次のステップを考える時期に来ているのかなと思います。ただ単に 説明が書かれているだけでは読んでもらえるものは作れないということがわ かったので、大幅に説明を加えるとともに、絵もふんだんに取り入れました。 また、ヘルプボタンやヒントボタンなども設け、ユーザが道に迷わないように しました。これらを通して、以前よりはずっと読みやすくなったのではないか と期待しています。ただ、まだユーザ実験をできていないので、この先、実際 に使ってもらってどのような反応になるのかを見ていきたいところです。
１次関数の学習教材
一方、昨年度から研究室全員で作っている中学の１次関数の学習教材は、その 後、かずかずの改良を加えて、それらしいサイトにまとめることができました。 その成果をまとめて、PPL でぼくが（生まれて初めて）ポスター発表を行いま した。当初は、１次関数を学びながらプログラミングも学べるサイトを作る予 定だったのですが、中学生に理解してもらえる内容にしようとすればするほど プログラミングからは離れ、ほとんどプログラミングは出てこない（１次関数 に関する）ゲームのようになりました。
プログラミングがほとんど出てこないなら OCaml Blockly でやる意味はない ような気がしなくもないけど、今の時点では中学生に実際に使ってもらえるも のを作る方が重要と考えて、当面はこの方針で行ってみようと思います。今年 度、附属中学の２年生の研究室訪問を受け、そのつながりから１月に附属中学 の３年生の授業で、１次関数の教材とゲームプログラミングのチュートリアル を実際に使ってもらう機会を得ることができました。そのようなつながりを大 切にしながら、少しでも使ってもらえるものを作り、それを通してプログラミ ングとの関わりも考えていければと思っています。
学習教材は、引き続き、皆で作りためていきたいと思います。
ゲームプログラミングでの世界の表示
Universe ライブラリを使ったゲームプログラミングでは、世界の情報がどの ように更新されるかが重要になってきます。これまで、ゲームの動作がおかし かったときは、プログラムを一生懸命、眺めて原因を探るしか対処の方法があ りませんでした。今年度はそこに手を入れて、世界の情報をブラウザのコン ソールに表示できるように Universe ライブラリを改良しました。 さらに、特殊なキーを押すとゲームの実行を一時停止したり、ステップ実行し たりすることもできるようにしました。これで、現在の世界の状況がどうなっ ているか、一目瞭然になり、デバッグもしやすくなると期待しています。
世界の情報は、作るゲームによって形が異なります。それを表示するためには、 ユーザによって与えられた世界の情報（型）を文字列に変換する必要がありま す。しかし、そのような関数をユーザに書いてもらうわけにはいかないので、 ppx_deriving を使って世界の定義から自動でそのような関数を生成していま す。
現在の懸案は、これが OCaml Blockly では動かない、ということです。OCaml Blockly 上でも動かすためには、ppx_deriving の機能を js_of_ocaml で javascript に変換しなくてはいけないのですが、その方法が現在のところ見 つかっていません。本当は LA の授業でこの機能を使いたかったのですが、そ れが実現するのはもう少し先になりそうです。
カバレッジツールの活用
関数型言語の授業では、デザインレシピの使用を勧め、テストを書くことでプ ログラムの信頼性をあげています。こちらの目論見としては、テストを十分に していれば、学生さんたちは自分のプログラムの信頼性を肌で感じることがで きるだろうということです。ところが、今年度、bisect_ppx というカバレッ ジツールを使って学生さんの書いたテストプログラムを調べてみたところ、 書いているテストがいまひとつで、プログラムの信頼性は必ずしも上がっては いないかも知れないという疑惑が出てきました（汗）。
カバレッジツールというのは、テストプログラムを実行した時に、テストされ るプログラムのどの部分が実際に実行されたかを調べるツールです。プログラ ム中の全ての部分が実行されているなら、どの部分も少なくとも１度はテスト されたことになります。一方、実行されていない部分が存在すれば、そこは １度もテストされていないということになります。
このカバレッジツールを使って学生さんの書いたテストプログラムを調べてみ たところ、課題が難しくなってくるにつれてテストされていない部分がそれな りにあることがわかりました。特に、授業中盤の駅間距離を求める関数や、更 新関数、最短を分離する関数などでは、例えば県名が異なる駅のテストがまる まる抜けていることがあることがわかりました。今は、現状を把握しただけで すが、これをどのように授業に活かしていくかは今後の課題です。とりあえず、 次年度の関数型言語の授業ではカバレッジツールを学生さんが自由に使える環 境を用意する予定です。
Mikiβ その後
昨年、web インタフェースを作った Mikiβ、その後、ユーザインタフェース の改良を行なったり、いろいろな型システムや論理体系をのせてみたり、 tex インタフェースを作ってみたりと様々に手を加えてきました。その結果、 それなりに使えるシステムに仕上がり、次の段階に移ったと思っています。 この先は、もっといろいろなところで使ってみて、どのような改良が必要に なっていくのかを吟味する予定です。
手始めに、新３年生のゼミで読んでいる教科書の体系を全部、Mikiβにのせよ うとしています。実際に、本格的に使おうとするとあれこれ問題点が出てきま す。今のところ、どういうわけか Chrome だとうまく動かない（なぜ？？？） とか、規則の数の上限が今は 35 だけどそれでは足りない（！）などが上がっ てきています。これらひとつひとつを順に片付けて、完成度をあげていきたい と思います。
限定継続演算子の演算子
昨年度は教育系の方が見える形で研究が進みましたが、限定継続演算子の研究 も地道に着実に進めています。shift/reset に対する部分評価器の正当性の証明
2006 年にぼくが shift/reset に対する部分評価器の正当性の証明を行ったの ですが、昨年、それは間違っていることが判明しました。今年度は、その誤り の原因を特定し、部分評価器の定義を一部、変更することで、正当性の証明を 行いました。問題の根幹は、reset で囲まれた式は値とは限らないのに、値で あるとして証明を行なっていたところです。実際、それを逆手にとると、2006 年の部分評価器では無限ループを破棄してしまうような具体例を作ることがで きました。この問題を解決するために、reset で囲まれた式も let 文に残す ように変更を加えました。（shift についても同様の問題があり、そちらにも 対処しました。）これで、無限ループを破棄する事態は避けられ、部分評価器 の正当性も証明することができました。
この研究は、control/prompt に対する CPS 変換の正当性の証明とも関連して おり、昨年度は２度の CPS 変換を行わないと証明ができないのではないかと 予想していました。しかし、shift/reset に対する部分評価器の正当性の証明 を考えていると、２度 CPS 変換しても状況は良くならなさそうということが わかりました。むしろ、必要なのはメタ継続に関する naturality、つまり 「メタ継続 mk の下での実行」と「初期メタ継続の元で実行し、その結果を mk に渡す」のは同じ、ということのようです。これは parametricity から導 かれます。それをしっかり理解するために、久しぶりに Wadler の Theorem for free! を読み直して、ようやく自分で運用できるかも知れないレベルで理 解した気がしました。来年度は、この方向で control/prompt の CPS 変換の 正当性の証明ができないか、考えてみようと思います。
shift/reset を使ったプログラムに対する reasoning
すでに shift/reset を使ったプログラミングは普通な世の中になっています が（そんなことはないか（笑））、shift/reset を使ったプログラムに関する 性質を示すのは依然として簡単ではありません。昨年度から、モナドに述語を 加えた形でいろいろな性質を記述できないか検討してきましたが、なかなか難 しく思うようには進んでいません。
一方で、refinement 型を使った研究などが発表されるようになり、そちらと の関連を探ってみたところ、筋が良いと思っていたモナドに述語を入れるとい う方法は、ものを難しくしすぎているらしいということがわかってきました。 モナドではなく、型の方に述語を入れて、モナドはいじらないようにすると、 うまく書けるのではないかというのが今の見通しです。この方向でどうなるか を探ってみたいと思っています。