Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Float が仮数と指数で表現されていることを示す #1050

Merged
merged 1 commit into from
Nov 4, 2024
Merged

Float が仮数と指数で表現されていることを示す #1050

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions LeanByExample/Reference/Type/Float.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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` を表示させると気が付きませんが、これは表示の際に数値が丸められているためです。
-/

Expand Down