diff --git a/LeanByExample/Reference/Type/Float.lean b/LeanByExample/Reference/Type/Float.lean index b244ddb..fb687d5 100644 --- a/LeanByExample/Reference/Type/Float.lean +++ b/LeanByExample/Reference/Type/Float.lean @@ -13,10 +13,22 @@ import Mathlib.Data.String.Defs --# #eval (-42.0 : Float) -/- ## 誤差 +/- ## 内部実装 + +浮動小数点数は、[IEEE 754](https://ja.wikipedia.org/wiki/IEEE_754) に従い内部的には符号 `s ∈ {0, 1}` と仮数(significand) `c : ℕ` と指数 `q : ℤ` の三つ組で表されています。これは `(-1)ˢ × c × 2 ^ q` として解釈されます。 +-/ -浮動小数点数は、[IEEE 754](https://ja.wikipedia.org/wiki/IEEE_754) に従い内部的には符号 `s ∈ {0, 1}` と仮数(significand) `c : ℕ` と指数 `q : ℤ` の三つ組で表されています。これは `(-1)ˢ × c × 2 ^ q` として解釈されます。特に、2進数として表現されていることになるので、一般に `Float` で10進数を正確に計算することはできません。 +-- `64 = 1 * 2⁶` なので、仮数部は 1 で指数は 6 になる +#guard Float.toRatParts' 64.0 = some (1, 6) +-- `6 = 3 * 2¹` なので、仮数部は 3 で指数は 1 になる +#guard Float.toRatParts' 6.0 = some (3, 1) + +-- `0.5 = 1 * 2⁻¹` なので、仮数部は 1 で指数は -1 になる +#guard Float.toRatParts' 0.5 = some (1, -1) + +/- ## 誤差 +特に、浮動小数点数は2進数として表現されているので、一般に `Float` で10進数を正確に計算することはできません。 次のように `0.1 : Float` を表示させると気が付きませんが、これは表示の際に数値が丸められているためです。 -/