Coq の有理数の定義では、ゼロの逆数がゼロに定義されていることに気付きました。(通常、ゼロによる除算は明確に定義されていない/合法的/許可されていません。)
Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0.
Proof. unfold Qeq. reflexivity. Qed.
なぜそうなのですか？
有理数の計算で問題が発生する可能性はありますか、それとも安全ですか?
1168 次
1 に答える
15
簡単に言えば、はい、絶対に安全です。
ゼロによる除算が明確に定義されていないと言うとき、実際に意味することは、ゼロには乗法逆数がないということです。特に、ゼロの乗法逆数を計算する関数を使用することはできません。ただし、他のすべての要素の乗法逆数を計算し、そのような逆数が存在しない場合 (たとえばゼロの場合) に任意の値を返す関数を作成することは可能です。これはまさにこの機能が行っていることです。
この逆演算子をどこでも定義できるということは、その引数がゼロとは異なることを明示的に主張することなく、それを計算する他の関数を定義できることを意味し、より便利に使用できます。実際、この関数が 0 を渡すと失敗する代わりに を返すようにしたら、どんなに苦痛になるか想像してみてくださいoption: コード全体をモナドにしなければならず、理解と推論が難しくなります。引数が非ゼロであることの証明を必要とする関数を作成する場合、同様の問題が発生します。
それで、キャッチは何ですか？さて、逆演算子を使用する関数について何かを証明しようとするとき、ゼロとは異なる引数を渡しているという明示的な仮説を追加するか、その引数が決してゼロになることはないと主張する必要があります。この関数に関する補題は、追加の前提条件を取得します。
forall q, q <> 0 -> q * (/ q) = 1
他の多くのライブラリはそのように構成されています。たとえば、MathComp の代数ライブラリの体公理の定義です。
特定の関数に必要な追加の前提条件を型レベルの制約として内部化したい場合があります。これは、たとえば、長さでインデックス付けされたベクトルgetと、境界内にある数値でのみ呼び出すことができる安全な関数を使用するときに行うことです。では、ライブラリを設計するときにどちらを採用するか、つまり、多くの追加情報を含む豊富な型を使用し、特定の関数への偽の呼び出しを防ぐ (長さインデックスの場合のように) か、この情報を除外するかをどのように決定しますか?明示的なレンマとしてそれを必要としますか（乗法逆の場合のように）？ここには明確な答えはありません。実際には、各ケースを個別に分析し、その特定のケースに適した代替案を決定する必要があります。
于 2015-03-26T18:42:28.680 に答える