Coq

Coq: 形式的証明支援システムの概要

Coqは、形式的な証明を支援するシステムの一つであり、その中心にはGallinaと呼ばれるプログラミング言語があります。このシステムは、フランスのフランス国立情報学自動制御研究所のPI.R2チームが中心となり、エコール・ポリテクニークやフランス国立工芸院、パリの大学などとの共同開発によって実現されています。Hugo Herbelinが実質的な開発者として名を馳せています。

名称の変更と今後の展望

2023年10月11日に、Coqはその名称をThe Rocq Proverに変更すると発表し、関連するコードベースやウェブサイトが改訂されました。この変更によって、今後の開発や機能の拡張が期待されます。

特徴と機能

Coqは、1984年にThierry CoquandとGérard Huetによって創始されたCalculus of Constructions（CoC）という高階型システムに基づいています。このシステムの根底には、カリー＝ハワード同型対応の考え方があり、正しい証明は正しい型を持つラムダ式として表現されるのです。1991年からは、Christine Paulin-Mohringが開発したCalculus of Inductive Constructions（CIC）が用いられ、帰納的構造も直接的に扱えるようになりました。

Coqには次のような機能が搭載されています。

• - 主張を操作する能力
• - 証明の機械的検査機能
• - 形式的証明の探索支援
• - 依存型を利用したプログラミング
• - 検証済みプログラムの実行可能な形式での抽出

中でも証明の自動化機能は増強されており、「omegaタクティク」はプレスバーガー算術の大部分を解決できる能力を持っています。このような機能の一環として、以下の成果が特筆されます。

• - 2004年に、Georges GonthierとBenjamin Wernerが発表した四色定理の完全な機械化された証明。
• - 2006年にリリースされたC言語コンパイラCompCert、これにはCoqを用いた証明が含まれています。
• - 2012年、Georges Gonthierと彼のチームによるFeit-Thompson定理の証明。

CoqはGNU LGPLライセンスで配布されているため、誰でも自由に利用することが可能です。

Ssreflect拡張について

Georges Gonthierのチームは、Coqの拡張として「Ssreflect」（small scale reflectionの略）を開発しています。この拡張は、Reflectionや多くのタクティクの改良を提供し、証明の保守性を高めるためのコーディング慣習も取り入れています。

Ssreflectは次のような特徴を持っています。

• - 証明の保守性を向上させるための機能
• - 自動生成される識別子の指定を行えなくし、バージョンアップによる問題を防ぐ機能
• - 明示的に証明の枝を完結させることで、軽微な証明を自動化し、修正が必要な範囲を明確にする機能
• - 検証済みの判定機を用いるreflection技術に基づくタクティク
• - 限定された集合上の演算子を効率よく扱う機能
• - 代数に関するライブラリの提供

SsreflectはCeCill-BとCecill-2.0というデュアルライセンスの下で配布されており、最新のバージョンはCoq 8.4に対応しています。

まとめ

Coqは型理論に基づく証明支援システムとして、形式的な数学やコンピュータ科学の分野で広く利用されています。新たな名称変更と機能の追加により、今後もその発展が期待され、研究や実用における役割が一層重要になるでしょう。

もう一度検索