| Item type |
Trans(1) |
| 公開日 |
2019-05-21 |
| タイトル |
|
|
タイトル |
定理証明支援系Coqにおける余帰納的証明のガード条件の漸進的検査 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Incremental Guardedness Check of the Co-recursive Proof in Coq Proof Assistant |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[発表概要，Unrefereed Presentation Abstract] |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
電気通信大学大学院情報理工学研究科情報・ネットワーク工学専攻 |
| 著者所属 |
|
|
|
東北大学電気通信研究所 |
| 著者所属(英) |
|
|
|
en |
|
|
Graduate School of Informatics and Engineering, The University of Electro-Communications |
| 著者所属(英) |
|
|
|
en |
|
|
Research Institute of Electrical Communication Tohoku University |
| 著者名 |
小澤, 祐也
中野, 圭介
|
| 著者名(英) |
Yuya, Ozawa
Keisuke, Nakano
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
定理証明支援系Coqでは，無限に続くリストのような余帰納的構造を持つデータについての証明を，タクティクと呼ばれるコマンドを用いて進めることができる．ただ，Coqでは無限のデータや証明をそのまま扱うことはできないため，再帰的な表現による有限の形で表している．このような無限のデータや証明は再帰関数として表現されるため，意味のないループの形でないという，ガード条件の検査（guardedness check）が証明の最後に行われている．このため証明全体を走査するために時間がかかってしまうという問題や，途中でガード条件が成立しなくなっていてもユーザは証明の最後の検査まで気づくことができないという問題がある．Coqには証明途中でガード条件の検査を行うGuardedコマンドが存在するが，これもそれまでの証明全体を走査するために，タクティクごとに実行すると時間効率が悪い．そこで本発表では，Coqにおける余帰納的証明のガード条件の検査を証明中に少しずつ行い，ガード条件が成立しなくなった際，即座にユーザに知らせることができるような手法を提案する．本手法ではタクティクの実行ごとに新しく作られた部分の証明のみを取得し，その部分的な証明に対してガード条件の検査を行う．検査を行った後は，その時点での環境やゴールのIDなどの情報を保持しておき，次回のタクティク実行時のガード条件の検査に用いる． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
In the proof assistant Coq, we can manipulate a proof of co-inductive structure data, such as infinite lists, using a command called tactic. Coq handles infinite data and infinite proofs by representing them in a finite form with (co-)recursion. To justify this approach, Coq checks that the guardedness of infinite data and proofs in which no co-recursive expressions are invalid like the non-productive infinite loop, when every proof is completed. Hence, there are problems that the check takes time since it scans the whole proof, and the user can not notice the guardedness became unsatisfied in the middle of the proof until the final guardedness check finished. Although Coq provides a Guarded command that checks the guardedness in the middle of the proof, it is inefficient for users to execute the command by each tactic during a proof. In this presentation, we propose a method to check the guardedness of the co-recursive proof incrementally and notify the user immediately when the guardedness condition gets violated. In our approach, we only observe a newly-generated part of the proof and check the guardedness condition every time applying a tactic. At that time, we also store some information such as the proof environment and the identifier of the current goal. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 12,
号 2,
p. 12-12,
発行日 2019-05-21
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1202008.pdf (103.1 kB)
