Coq

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索
Coq
Coq logo.png
CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png
作者 フランス国立情報学自動制御研究所, パリ第7大学, エコール・ポリテクニーク, パリ第11大学, リヨン高等師範学校
初版 4.10 (1989年)
最新版 8.4 / 2012年8月12日(2年前) (2012-08-12
プログラミング言語 OCaml
対応OS マルチプラットフォーム
対応言語 多言語対応
種別 定理証明支援系
ライセンス GNU LGPL 2.1
公式サイト The Coq Proof Assistant
テンプレートを表示

Coqは証明支援システムの一つで、プログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所PI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニークフランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。

特徴[編集]

CoqはCalculus of Constructionsという高階型システム(Thierry CoquandGérard Huetが1984年に創始したもので、英語ではCoCと略せてシステム名Coqに至る)に基づく。正しい証明は正しく型がつくラムダ式であるというカリー=ハワード同型対応を利用しているので、Coqの証明言語は型付きラムダ計算の一種である。1991年以降Coqが用いているCalculus of Constructionsの変種は、Christine Paulin-Mohringによるもので、帰納的構成を直接含み、Calculus of Inductive Constructions (CIC)という名前がついている。

Coqには

  • 主張を操作する機能
  • 主張の証明を機械的に検査する機能
  • 形式的証明の探索を支援する機能
  • 依存型を用いたプログラムを記述する機能
  • 実行可能な検証済みプログラムを抽出する機能

がある。

加えてCoqには証明の自動化機能が増えている。中にはomegaタクティクというものがあり、プレスバーガー算術の大部分を決定できる。

Coqの最大の達成の中には、

  • 四色定理: Georges GonthierとBenjamin Wernerによって、完全に機械化された証明が2004年に完了した。
  • CompCert: C言語のコンパイラで、Coqによって開発され証明がつき、2006年にリリースされた。[1]
  • Feit-Thompson定理英語版: Georges Gonthierと彼のグループによって、2012年9月に証明が完了した。[2]

がある。

CoqはGNU LGPLライセンスで配布されているフリーソフトウェアである。

Ssreflect拡張[編集]

Georges GonthierのチームがSsreflect(small scale reflectionの略)というCoqの拡張を開発している。拡張はreflection用の機能にとどまらず、Coqの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。 Ssreflectの機能には下のようなものがある。

  • 保守性を高めるための機能
    • Coqが自動生成した識別子をユーザが指定できなくなって、Coqのバージョンアップによって証明が通らなくなることを防止する機能
    • 証明の枝を完結させることを明示して、軽微な証明を自動で行わせられる上に、証明が通らなくなったときに修正するべき範囲がわかりやすくなる機能
  • 主張を直接証明する代わりに、Coq内で検証済みの判定機を実行するreflectionという技法に特化した証明タクティク
  • 有限集合上の和や積などの大きな演算子を扱う機能
  • 代数のライブラリ

SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く。[3]

脚注[編集]

関連項目[編集]

外部リンク[編集]