融合変換を模倣するプログラム生成変換の戦略

摘要

等号付せ一階述語論理に基づくプログラム生成変換GSは，一般の等式論理では扱うことのできない限量子や論理和を含む仕様を取り扱うことができる．GSは，実行不可能な仕様から実行可能なプログラムを生成できる場合があり，プログラムの自動生成に応用が期待できる。しかし，どのようなプログラムや仕様に対してプログラム生成が成功するかは全く不明であった．本稿では，プログラム融合変換として知られるDeforestationをGS が模倣できることを示す．