2007年01月22日計算機数理科学専攻・計算論講座
酒井研究室（酒井正彦教授、草刈圭一朗助教授）
信頼性が高くて効率の良いソフトウェアは、どのようにしたら作成できるか？これを解明するために、計算（特に関数型プログラム）が持つ基本的な性質の基礎研究を進めています。
一般にプログラムの性質を議論するためには、その意味を表すための数学的モデルが必要となります。関数型プログラムのモデルとしては、従来からλ算法や項書換え系が採用されています。しかしながら、関数型プログラムをより正確に表現するためには、この二つを組み合わせた高階項書換え系を議論したり、規則の適用の際の優先順位を考慮する必要があります。そこで、従来からのモデルや新しいモデルに対して、以下の事柄を中心に研究を行なっています。
- 効率的な計算を行うための計算順序を動的に決定するための計算戦略
- プログラムの持つ性質を自動証明するために必要となる完備化手続きや合流性・停止性の自動判定法
- 高信頼プログラムの自動生成
- プログラム変換による計算の効率化
これらの研究の一つとして我々のグループが開発した、プログラム生成系GeneSysの概略図を以下に示します。GeneSysは論理式で記述された仕様からプログラムを生成するための枠組であり、生成はGeneSysに用意されているいくつかの変換規則をユーザが指定することにより行われます。生成に成功した場合には、得られたプログラムが仕様を満たすことが保証されると言う利点があります。
