著者

小澤 祐也 中野 圭介

雑誌

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

巻号頁・発行日

vol.12, no.2, pp.12, 2019-05-21

---

定理証明支援系Coqでは,無限に続くリストのような余帰納的構造を持つデータについての証明を,タクティクと呼ばれるコマンドを用いて進めることができる.ただ,Coqでは無限のデータや証明をそのまま扱うことはできないため,再帰的な表現による有限の形で表している.このような無限のデータや証明は再帰関数として表現されるため,意味のないループの形でないという,ガード条件の検査(guardedness check)が証明の最後に行われている.このため証明全体を走査するために時間がかかってしまうという問題や,途中でガード条件が成立しなくなっていてもユーザは証明の最後の検査まで気づくことができないという問題がある.Coqには証明途中でガード条件の検査を行うGuardedコマンドが存在するが,これもそれまでの証明全体を走査するために,タクティクごとに実行すると時間効率が悪い.そこで本発表では,Coqにおける余帰納的証明のガード条件の検査を証明中に少しずつ行い,ガード条件が成立しなくなった際,即座にユーザに知らせることができるような手法を提案する.本手法ではタクティクの実行ごとに新しく作られた部分の証明のみを取得し,その部分的な証明に対してガード条件の検査を行う.検査を行った後は,その時点での環境やゴールのIDなどの情報を保持しておき,次回のタクティク実行時のガード条件の検査に用いる.