|
本研究の目的である単射関数の逆化を実現するために，本年度は逆化コンパイラで生成された書換え系を決定化する手法の開発に取り組んだ．一般には，逆化で得られた関数定義は適用に関して決定的でないため，関数の計算を保持しながら，関数定義を部分的に具体化することで決定的にする変換を提案した．具体的には，ナローイング計算を用いて関数定義を展開し，計算結果を得られる可能性がある展開に必要な具体化を関数定義に適用することで，関数に期待された計算を保持しながら関数定義を部分的に具体化する．この方法は必ずしも関数定義を決定的にできるわけではないが，逆化の評価に利用されるベンチマークに逆化を適用した際には，結果の関数定義が決定的でない場合に，決定的な定義に変換できることを確認した．
一方，提案手法でも決定的にできない例も存在する．そのような例の中には提案手法では本質的に決定的にできない場合もある．そのような場合の決定化手法を開発するため，文脈自由文法を中間結果として利用する逆化手法の改良も行った．
関数型言語の計算モデルである項書換え系を対象とした逆化では，出力を項書換え系にするために紐解き変換（unraveling）を適用することができる．しかし，紐解き変換は条件付き項書換え系から項書換え系への近似的な変換であり，一般には計算に関して健全ではない．逆化で得られたプログラムの性質を解析するために紐解き変換で項書換え系へ変換して性質を解析できるように，紐解き変換が健全になる十分条件を明らかにした．その十分条件を既存の結果，および条件付き項書換え系から項書換え系への別の変換と比較を行い，既存の結果をまとめた論文を出版するに至った．
|
