| 研究概要 |
本研究では,項書換え系(TRS)からの逆計算プログラムの生成に取り組んでおり,バグのないプログラムによる効率的な逆計算をめざしている.また,let構文などを持つ関数型言語(主にStandard ML)を自然に表現できる条件付きTRSの表現を解析し,実用の関数型プログラムの逆計算プログラム生成をめざす.
今年度は以下の研究を行った.
・構成子TRSを対象とした逆計算コンパイラの部分逆計算への応用として,部分逆計算コンパイラとしてまとめ,国際会議で発表した.
・すでに示されている最内戦略が有効である条件のもとで,順計算/逆計算の両方のプログラムを組み合わせた場合でも最内戦略が有効であることを明らかにし,部分逆計算の結果とともに発表した.
・生成したプログラムを動作させるためのナローイング計算の停止性証明の十分条件として,すでに提案していた依存対法を依存グラフ法に拡張した.実装については,単純な戦略に基づいた停止性証明ツールを実装したが,ナローイングの停止性証明の自動化は書換えの場合よりも戦略が複雑であるので次年度の課題とする.
・条件付きTRSからTRSへの紐解き変換については,計算の効率化の特徴であるようなlet文に対応した部分は保持しながら書換え規則を最適化する変換を提案し,国内のシンポジウムで発表した.この手法には条件付きTRSの解析や関数型プログラムの最適化への応用が期待でき,さらに研究を行う余地がある.
なお,解が複数個存在する場合の非決定的な逆計算のための全解探索インタープリタについては,本年度に同グループで試作した計算戦略の評価実験用のツールを基に次年度に開発を行う.
|
