|
本年は、ポインタを持つ再帰データ型のための始代数理論を構築し、それを関数型言語に実装して有効性を確認することを行った。
これまでの研究からインデックス付き集合の圏の代数構造を用いて、高階抽象構文、高階書換え系、サイクルを持つデータ型といった様々な体系が、インデックスを適切に変更することによってモデル化できることが分かっている。本研究はこめアイデアを拡張し、先のインデックス集合として取られていた「変数」の集合を「ポインタ」の集合として捉え直し、ポインタの集合によってインデックス付けられた集合の圏で再帰データ型をモデル化するアプローチを取った。このために導入したアイデアはインデックスとして「構成するデータ型の形状」を取った点である。例えば、二分木型にサイクルと循環のポインタを導入するためには、木のノードの情報を取り除いた「木の形状」のみを持つ構造をインデックスとする。不正なポインタのないデータ型を構成することができた。
さらにこの理論によって得られたデータ型を関数型言語Haskellに実装を行った。Haskellの先進的な型機構を最大限に活用した。この目的のために「一般化代数データ型(GADT)」が適切であることを見出し、形状でインデックスされたデータ型を実現できた。この結果の論文は完成問近である。
また本年度は、執筆した論文「高階書換え系の停止性のための代数モデル」が日本ソフトウェア科学会第12回論文賞を受賞した。これは、長く未解決だった高階書換えの体系コンビナトリー簡約系の完全な代数モデルを与え、メタプログラミングシステムのための計算体系としてメタ書換えの完全な代数的な特徴付けの結果を得たことが高く評価されたものである。
|
