From 20cf65910c4c4026e2e5817499ded491c81c0e59 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 4 Nov 2024 16:44:13 +0900 Subject: [PATCH] =?UTF-8?q?Float=20=E3=81=8C=E4=BB=AE=E6=95=B0=E3=81=A8?= =?UTF-8?q?=E6=8C=87=E6=95=B0=E3=81=A7=E8=A1=A8=E7=8F=BE=E3=81=95=E3=82=8C?= =?UTF-8?q?=E3=81=A6=E3=81=84=E3=82=8B=E3=81=93=E3=81=A8=E3=82=92=E7=A4=BA?= =?UTF-8?q?=E3=81=99=20Fixes=20#1049?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Type/Float.lean | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Reference/Type/Float.lean b/LeanByExample/Reference/Type/Float.lean index b244ddba..fb687d5b 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` を表示させると気が付きませんが、これは表示の際に数値が丸められているためです。 -/