83

Isabelle/HOL 証明アシスタントには、Coq と比較して弱点と長所がありますか?

4

3 に答える 3

82

私は Coq に精通しており、Isabelle/HOL の経験はあまりありませんが、少しはお役に立てるかもしれません。おそらく、Isabelle/HOL の経験が豊富な他のユーザーが、これを改善するのに役立つ可能性があります。

2 つのシステムには 2 つの大きな相違点があります。それは、基礎となる理論と相互作用のスタイルです。それぞれの場合の主な違いの概要を簡単に説明します。

理論

Coq と Isabelle/HOL はどちらも、強力で非常に表現力豊かな高階ロジックに基づいています。ただし、これらのロジックはいくつかの機能で異なります。

依存型

Coq の論理は従属型理論であり、帰納的構造の微積分(略してCIC ) として知られています。ここでの「依存型」とは、Coq の型が通常の値を参照できることを意味します。たとえば、次のmult型の行列乗算関数を書くことができます。

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p

この関数の型は、2 つの行列を入力として取り、1 つが dimensionn x mで、もう 1 つが dimensionm x pであり、dimension の行列を返すことを示していますn x p。一方、Isabelle/HOL の理論には従属型がありません。multしたがって、上記と同じ型の関数を書くことはできません。代わりに、あらゆる種類の行列に対して機能する関数を作成し、適切な種類の引数を受け取ったときにこの関数の特定のプロパティを事後的に証明する必要があります。言い換えれば、Isabelle/HOL で作業する場合、Coq 型で明示されている特定のプロパティを別の定理としてアサートする必要があります。

依存型は興味深いものもありますが、一般的にどの程度有用かは明らかではありません。私の印象では、それらを使用するのは非常に複雑であり、特定のプロパティを型レベルで表現することと、それらを個別の定理として使用することの利点は、この追加の複雑さに値しないと感じている. 個人的には、明確な理由がある場合は依存型を使用することを好みます。

推論の基本原則

デフォルトでは、Coq の理論には、排除中間の法則(つまり、非構成的に推論する能力)、拡張性 (たとえば、等しい結果を生成する関数が自体は等しい)、および選択の公理。一方、Isabelle/HOL では、そのような原則が組み込まれています。

理論的には、これは大きな問題ではありません。なぜなら、Coq のロジックは、人々がこれらの推論原理を追加の公理として安全に追加できるように設計されているからです。とはいえ、Isabelle/HOL でこの種の推論を行う方が簡単であるという印象があります。ロジックはそれらをサポートするためにゼロから構築されているからです。

(このような基本原則を Coq のロジックから除外する理由は何なのか疑問に思うかもしれません。動機は哲学的なものです。Coq のコア ロジックでは、証明は実行可能なプログラムと見なすことができ、ロジックに建設的な風味を与えます。除外されたものを拒否する理由たとえば、中間は、選言の証明が、またはのどちらが真かA \/ Bを示すビットを返すプログラムに対応するということです; したがって、除外された中間は、存在し得ないすべての数学的問題を決定するプログラムに対応します。この問題については、もう少し詳しく説明します。)AB

相互作用のスタイル

Coq と Isabelle/HOL はどちらもインタラクティブな定理証明者です。それらは、それらについての定義と証明を書くための言語です。これらの証明はコンピューターによってチェックされ、間違いがないことが確認されます。どちらのシステムでも、何かを証明する方法を説明するコマンドを与えることで、証明を書き留めます。ただし、これが各システムで発生する方法は異なります。

Isabelle/HOL は、一般的に言えば、「プッシュボタン」証明自動化のサポートがより成熟しています。たとえばsledgehammer、定理を証明しようとするいくつかの外部自動定理証明器とソルバーを呼び出す有名な戦術が付属しています。omegaCoq には、またはなどの多くの強力な証明自動化プロシージャも付属していますcongruenceが、それらは一般的には適用できません。また、Isabelle/HOL で 1 つのコマンドで解決できる多くの定理は、Coq でより明示的な証明を必要とします。

もちろん、この便利さには代償が伴います。Isabelle/HOL では、システムが自分で多くのことをしようとするため、自分の証明を制御するのが難しいと言われています。これは、単純な定理を証明する場合には問題になりませんが、証明の自動化が十分に強力ではなく、定理証明者にさらに詳細に進める方法を伝える必要がある場合に問題になります。

ユーザー定義の証明自動化手順をサポートする場合、状況は少し異なります。Coq には、 Ltac として知られる証明を書くためのタクティック言語が付属しています。これは、独自のプログラミング言語です。Ltac にはいくつかの設計上の問題がありますが、ユーザーはかなり複雑な証明自動化手順を軽量な方法でエンコードできます。より重いタスクの場合、Coq ではユーザーが Coq の実装言語である OCaml でプラグインを作成することもできます。対照的に、Isabelle/HOL では、Ltac のような高レベルの自動化言語はなく、ユーザーがカスタム証明自動化手順をプログラムできる唯一の方法は、プラグインを使用することです。

于 2015-05-11T04:13:33.103 に答える
13

質問で「Isabelle/HOL」と正確に書かれているので、Isabelle で使用されている HOL ロジックについて説明します。これは、Coq との比較に使用するのに最適だと思います。私は型システムとロジックの専門家ではありませんが、ここで述べていることは、少なくともおおよそは正しいと思います。これも確かに好みの問題です;-)そして私の答えは主観的かもしれません.

最も大きな違いは、型システムとロジックにあります。

強さは、ML ファミリーの関数型言語を知っている人にとってはより自然なものであり (SML を知っている人にとってはなおさらです)、問題を解決するために実用的なアプローチを使用します。基礎。その型システムは Hindley Milner の型システムに近く、デフォルトで終了します (ユーザーが変更しない場合)。

一方、Coq はより厳密で、直感的なロジックを使用します。いくつかの順序を持​​つ特殊な型システムがあり、扱いが難しく、状況によっては終了しない可能性のある型の依存関係を許可します。また、Isabelle では直接不可能な証明からプログラムを抽出することもできます (これは比較的非効率的かもしれません)。

于 2015-05-10T22:36:42.617 に答える