情報科学 › 研究のための計算の実務 › NumPy で書く配列計算

固定幅整数の演算は 2ʷ を法として閉じる

命題 7.2（「NumPy で書く配列計算」§7） ・ ✓公理まで証明済み

  1. 任意の整数 vv に対し、v≡r(mod2w)v\equiv r\pmod{2^w} となる r∈Iwr\in I_w がただ 1 つ存在する。wrapw(v)=v\mathrm{wrap}_w(v)=v となるのは v∈Iwv\in I_w のとき、そのときに限る。
  2. a,b∈Iwa,b\in I_w について、a⊕b=a+ba\oplus b=a+b となるのは真の和 a+ba+b が IwI_w に属するとき、そのときに限る。⊖\ominus と a−ba-b、⊗\otimes と abab についても同じである。
  3. IwI_w の元を変数に代入し、+,−,×+,-,\times だけからなる式を ⊕,⊖,⊗\oplus,\ominus,\otimes で計算した結果は、同じ式を整数として計算した真の値 vv に対する wrapw(v)\mathrm{wrap}_w(v) に等しい。とくに、最終的な真の値が IwI_w に属していれば、途中の値が IwI_w を出ていても、結果は正しい。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 1 件、定義なども含めて 1 件）。

印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。

前提をたどる 証明が使う定理・定義（直接 1 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 2 問