| 研究概要 |
本研究では,項書換え系(TRS)からの逆計算プログラムの生成に取り組んでおり,バグのないプログラムによる効率的な逆計算をめざしている.本年度は特に,単射関数に注目し,決定的な計算を行う逆関数プログラムの生成に取り組んだ.
逆計算コンパイラが生成するプログラムは一般に停止性や合流性を持つとは限らない.また,紐解き変換がCTRSを近似したTRSを生成するという欠点から,逆計算の計算結果の集合に解ではない項が含まれるという問題があった.これを解決するために,加算・乗算プログラムの逆計算に取組み,一般には解決が難しい問題点であることを明らかにした.そこで,対象とするプログラムを単射関数に限定し,停止性と合流性を持つ逆計算プログラムを生成するための変換法を開発した.また,単射関数であるための規則の形式の十分条件も明らかにした.さらに,他研究の変換を紐解き変i換の代わりに導入することで,問題が生じないことも確認したが,その特徴を理論的に保証するためには元のプログラムがある構文的条件を満たす必要があった.さらに,乗算のように値が計算結果に反映されないような場合,すなわち,生成プログラムがTRSのクラスに入らない場合には,ナローイングによる計算が必ず停止しないことをインタプリタを用いた計算の実験で確認した.紐解き変換では停止性を失わないことが理論的に保証されているので,一般には紐解き変換が有効であり,条件を満たす場合には他研究の変換を導入することで,逆計算コンパイラの性能を高めた.これは,紐解き変換と他研究の変換の比較にも繋がる成果といえる.この結果については次年度に発表する予定である.
今年度は他に,以下の研究を行った.
・前年度に作成した逆計算コンパイラにウェブユーザインタフェースを与え,出力書式を本グループで既に作成したTRSインタプリタと一致させ,逆計算の実験を行った.
・逆計算コンパイラの後半の変換である紐解き変換(CTRSからTRSへの変換)を改良し,直感的にコーディングされた除算の再帰プログラムと一致した除算プログラムの自動生成に成功した.また,この結果をまとめ,国際ワークショップで発表した.
|
