| 研究実績の概要 |
本研究では，1階項書き換えに基づくパターンによるプログラム変換の枠組みを拡張し，高階関数を取り扱えるようにすることで，より柔軟で強力なプログラム自動変換の枠組みを実現することを目指した．Yamadaによって提案された単純型付き項書き換えシステム(Simply Typed Term Rewriting System ,以下 STTRS)を理論的基礎とし，STTRSの等価性を検証するため，Toyama(1991)の項書き換えシステムの等価変換を拡張し，STTRSの等価変換を提案した．STTRSの等価変換の理論的正しさの証明において，1階の項書き換えシステムでは自明に成立する新規導入関数の除去がSTTRSの枠組みでは自明に成立しないことを明らかにした．Aotoらによって提案された高階十分完全性の概念と，相対停止性を利用することにより，STTRSの枠組みで新規導入関数の除去を示すことができた．
STTRSにパターン変数を組み込んだSTTRSパターンの概念を導入し，STTRSパターンとSTTRSのパターンマッチングアルゴリズムを提案した．STTRSパターンマッチングアルゴリズムを利用することにより，変換パターンの適用したSTTRSに基づくプログラム変換の枠組みを実現することができる．
組化変換は余分な再帰呼出しの回数を減らすことにより，プログラムの効率の改善を目指す手法である．平成26年度は高階関数だけではなく，効率的な組化変換を書き換えの枠組みで実現するために，条件付き項書き換えシステム(Conditional Term Rewriting System， 以下 CTRS)を利用したプログラム変換の枠組みの実現を目指した．そのための第1歩としてTRSの等価変換を拡張し，CTRSの等価性を示す手法を提案し，プログラム変換に関する国際ワークショップWPTE 2014で報告した．
|
