| 研究概要 |
本研究では,項書換え系(TRS)からの逆計算プログラムの生成に取り組んでおり,バグのないプログラムによる効率的な逆計算をめざしている.本年度も前年度に引続き,単射関数に注目し,決定的な計算を行う逆関数プログラムの生成に取り組んだ.
逆計算コンパイラが生成するプログラムは一般に停止性や合流性を持つとは限らない.また,紐解き変換がCTRSを近似したTRSを生成するという欠点から,逆計算の計算結果の集合に解ではない項が含まれるという問題があった.これを解決するために,変換で得られたTRSが停止性を持つ場合には,完備化手続きを適用することで合流性を持つTRSを得られることを示した.完備化手続きは合流性を持つTRSを生成する手続きであるが,必ずしも成功するわけではない.しかし,逆計算コンパイラで得られたTRSが停止性を持つ実用的な例で実験を行なったところ,実験した例すべてで完備化手続きが成功した.さらに,これまでの逆計算コンパイラの実装とインタフェースを整備した.
実験では従来の完備化システムを実装して用いた.しかし,ほとんどの例では再帰経路順序では等式の方向付けに失敗した.そこで,停止性証明ツールを利用した完備化システムを実現することで,完備化に成功した.
等価関係を利用して定義されるような関数を扱うTRSでは,項を最内戦略で評価する必要がある.従来の完備化ではそのようなTRSについては正しい結果が得られない.そこで,最内戦略で評価されるTRSに対する従来の完備化の枠組の正当性を保存するための十分条件も示した.
今年度の研究結果は年度内の発表は間に合わなかったが,すでに論文にまとめるまでに至っている.また,本成果は条件付きTRSからTRSへの紐解き変換の改善に相当し,今後,条件付きTRSの研究に役立つことが期待できる.
|
