| Item type |
Trans(1) |
| 公開日 |
2017-01-06 |
| タイトル |
|
|
タイトル |
定理証明器Coqの効率的な有限ドメイン関数ライブラリ |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Efficient Finite-domain Function Library for the Coq Proof Assistant |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[通常論文] 対話的定理証明，Coq，SSReflect，有限型，有限ドメイン関数，プログラム抽出，証明のモジュール性 |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
筑波大学大学院コンピュータサイエンス専攻 |
| 著者所属 |
|
|
|
筑波大学大学院コンピュータサイエンス専攻 |
| 著者所属(英) |
|
|
|
en |
|
|
Department of Computer Science, University of Tsukuba |
| 著者所属(英) |
|
|
|
en |
|
|
Department of Computer Science, University of Tsukuba |
| 著者名 |
坂口, 和彦
亀山, 幸義
|
| 著者名(英) |
Kazuhiko, Sakaguchi
Yukiyoshi, Kameyama
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
本研究は，対話的定理証明器Coqの有限型と有限ドメイン関数に関する既存ライブラリを改良し，従来のライブラリを用いた証明をほとんど変更することなく，その証明から抽出されるプログラムの効率を大幅に改善したものである．CoqのSSReflect/Mathematical Componentsライブラリは，有限型と有限ドメイン関数をサポートするライブラリfintypeとfinfunを提供し，これらのデータに対する証明の手間を大幅に削減することに成功している．しかし，その証明からプログラム抽出の手法で作成したプログラムは，多くの場合において非常に効率が悪いという問題がある．本研究では，fintypeやfinfunを改善したライブラリを実装した．このライブラリを用いて作成した証明から抽出したOCamlコードは，既存ライブラリの場合と比べて非常に高速である．例として，行列積の計算では，計算時間をおよそO(n5)からO(n3)へ改善できたことを示す．また，既存のSSReflectライブラリを用いたCoqの証明は，ほとんど書き換えることなく本研究のライブラリを用いた証明となる．例として，GonthierらのFeit-Thompson定理の約17万行におよぶ形式証明が，わずか10行以下の修正で，本研究のライブラリを用いた証明にできたことを示す． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
We provide finite-domain function libraries in Coq, which improves the efficiency of code extracted from proofs without forcing one to rewrite the whole proofs which use existing libraries. The SSReflect/ Mathematical Components of Coq provide the libraries to support finite types (fintype) and finite-domain functions (finfun), which allow one to drastically reduce the burden of writing proofs. While useful in proving, they have a serious problem in the performance of code extracted from proofs. In this study, we improve the fintype and finfun libraries, and show that OCaml code extracted from proofs using our libraries are much more efficient than those using the SSReflect libraries, and that existing proofs using the SSReflect libraries can be ported to the proofs using our libraries with very little modification. As concrete evidence for that, we provide a matrix-multiplication benchmark, whose time complexity has been improved from O(n5) to O(n3) by our libraries. We also demonstrate that the 170,000-line proof of Feit-Thompson theorem has been successfully ported where we only have to rewrite less than 10 lines of the whole proof. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 10,
号 1,
p. 14-28,
発行日 2017-01-06
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1001005.pdf (538.6 kB)
