著者

坂口 和彦 亀山 幸義

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.10, no.1, pp.14-28, 2017-01-06

---

本研究は,対話的定理証明器Coqの有限型と有限ドメイン関数に関する既存ライブラリを改良し,従来のライブラリを用いた証明をほとんど変更することなく,その証明から抽出されるプログラムの効率を大幅に改善したものである.CoqのSSReflect/Mathematical Componentsライブラリは,有限型と有限ドメイン関数をサポートするライブラリfintypeとfinfunを提供し,これらのデータに対する証明の手間を大幅に削減することに成功している.しかし,その証明からプログラム抽出の手法で作成したプログラムは,多くの場合において非常に効率が悪いという問題がある.本研究では,fintypeやfinfunを改善したライブラリを実装した.このライブラリを用いて作成した証明から抽出したOCamlコードは,既存ライブラリの場合と比べて非常に高速である.例として,行列積の計算では,計算時間をおよそO(n5)からO(n3)へ改善できたことを示す.また,既存のSSReflectライブラリを用いたCoqの証明は,ほとんど書き換えることなく本研究のライブラリを用いた証明となる.例として,GonthierらのFeit-Thompson定理の約17万行におよぶ形式証明が,わずか10行以下の修正で,本研究のライブラリを用いた証明にできたことを示す.