| 研究概要 |
単射性を持つ関数プログラムの逆計算プログラム生成コンパイラの開発およびウェブを介したサービス提供に向けて,本年度は以下の成果を得た.
● 関数が単射性を持つための十分条件をまとめた(国際会議に採択され,2010年4月に発表予定).本結果は,逆計算プログラム生成コンパイラを利用した条件であり,単射性が決定可能なクラスに属さない例についても単射性を持つことを証明できる例が存在することを確認した.
● 逆計算プログラム生成コンパイラの中間結果である条件付き項書換え系の規則の優先順位を決定する方法について考察した.本結果については次年度に論文にまとめる予定である.
● let構造をcase構造を持つ関数型プログラムへの応用を目的とし,逆計算コンパイラの枠組みの拡張を行った.本結果についても次年度に論文にまとめる予定である.
● 逆計算プログラム生成コンパイラのウェブサービスを行うためのサーバ環境およびプログラムのインタフェースについて検討し,その開発のための準備を行った.具体的には,制約付き項書換え系の停止性証明および定理自動証明ツールのウェブインタフェース開発の中で,本研究にも利用できる枠組みを想定し開発を行った.次年度に本枠組みに基づいた逆計算プログラム生成コンパイラのインタフェースを構築する.
● 単射性を持たない関数から生成された逆関数プログラムのインタープリタであるナローイング計算の停止性証明法を提案した.
本年度の取り組みにより,本研究の目的である逆計算プログラム生成のウェブサービスを提供するシステムを開発するための枠組みが整った.また,逆計算プログラム生成の関連研究が本年度に他のグループから発表されたことから,本研究を推進することで逆計算プログラム生成の分野に貢献できることを期待できる.
|
