Values of encoded numerical systems

An encoded numerical system may contain ordinary values, signed infinities, and exceptional bit patterns. These possibilities are not specific to IEEE floating point: posits have NaR, some low-precision formats reserve individual words, and fixed-point systems may have no exceptional values at all.

NumericalValue records this common semantic shape without prescribing a storage layout. The finite value type remains a parameter, so a system may denote real numbers, rational numbers, integers, complex numbers, or another exact mathematical domain.

inductive FloatLib.Numerics.ExceptionalValue : Type

Why an encoded word has no ordinary numerical value.

• nan (payload : Option Nat := none) : ExceptionalValue

  A NaN encoding, optionally carrying its representation-defined payload bits.

• notAReal : ExceptionalValue

  The single not-a-real value used by posit systems.

• reserved (payload : Option Nat := none) : ExceptionalValue

  A representation-specific reserved word, optionally retaining its encoded payload.

• undefined : ExceptionalValue

  An operation whose result is intentionally outside the scalar semantics.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqExceptionalValue : DecidableEq ExceptionalValue

def FloatLib.Numerics.instDecidableEqExceptionalValue.decEq (x✝ x✝¹ : ExceptionalValue) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instReprExceptionalValue : Repr ExceptionalValue

def FloatLib.Numerics.instReprExceptionalValue.repr : ExceptionalValue → Nat → Std.Format

inductive FloatLib.Numerics.NumericalValue (α : Type u) : Type u

The mathematical meaning of one encoded value.

The sign on infinity is true for negative infinity. Signed finite zero, when a format distinguishes it, should be retained by the finite semantic type. For example, FloatLib's exact Dyadic representation stores the sign of a zero mantissa.

• finite {α : Type u} (value : α) : NumericalValue α
• infinity {α : Type u} (negative : Bool) : NumericalValue α
• exceptional {α : Type u} (value : ExceptionalValue) : NumericalValue α

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqNumericalValue {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (NumericalValue α✝)

def FloatLib.Numerics.instDecidableEqNumericalValue.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : NumericalValue α✝) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.instReprNumericalValue.repr {α✝ : Type u_1} [Repr α✝] : NumericalValue α✝ → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprNumericalValue {α✝ : Type u_1} [Repr α✝] : Repr (NumericalValue α✝)

def FloatLib.Numerics.NumericalValue.map {α : Type u} {β : Type v} (f : α → β) : NumericalValue α → NumericalValue β

Apply a function to an ordinary value while preserving infinities and exceptional values.

@[simp]

theorem FloatLib.Numerics.NumericalValue.map_finite {α : Type u} {β : Type v} (f : α → β) (value : α) : map f (finite value) = finite (f value)

Mapping a finite value applies the supplied function to its mathematical payload.

@[simp]

theorem FloatLib.Numerics.NumericalValue.map_infinity {α : Type u} {β : Type v} (f : α → β) (negative : Bool) : map f (infinity negative) = infinity negative

Mapping preserves an infinity, including its sign.

@[simp]

theorem FloatLib.Numerics.NumericalValue.map_exceptional {α : Type u} {β : Type v} (f : α → β) (value : ExceptionalValue) : map f (exceptional value) = exceptional value

Mapping preserves an exceptional value because it has no ordinary payload to transform.

def FloatLib.Numerics.NumericalValue.finite? {α : Type u} : NumericalValue α → Option α

Extract the ordinary value, returning none for infinity or an exceptional encoding.

def FloatLib.Numerics.NumericalValue.isFinite {α : Type u} : NumericalValue α → Bool

Whether this semantic value is ordinary and finite.

@[simp]

theorem FloatLib.Numerics.NumericalValue.finite?_finite {α : Type u} (value : α) : (finite value).finite? = some value

Extracting the payload of a finite observation succeeds.

@[simp]

theorem FloatLib.Numerics.NumericalValue.finite?_infinity {α : Type u} (negative : Bool) : (infinity negative).finite? = none

Infinity has no finite payload.

@[simp]

theorem FloatLib.Numerics.NumericalValue.finite?_exceptional {α : Type u} (value : ExceptionalValue) : (exceptional value).finite? = none

An exceptional observation has no finite payload.

@[simp]

theorem FloatLib.Numerics.NumericalValue.isFinite_finite {α : Type u} (value : α) : (finite value).isFinite = true

A finite constructor is recognized as finite.

@[simp]

theorem FloatLib.Numerics.NumericalValue.isFinite_infinity {α : Type u} (negative : Bool) : (infinity negative).isFinite = false

Infinity is not finite.

@[simp]

theorem FloatLib.Numerics.NumericalValue.isFinite_exceptional {α : Type u} (value : ExceptionalValue) : (exceptional value).isFinite = false

An exceptional observation is not finite.

@[simp]

theorem FloatLib.Numerics.NumericalValue.map_id {α : Type u} (x : NumericalValue α) : map id x = x

Mapping the identity function leaves every numerical value unchanged.

@[simp]

theorem FloatLib.Numerics.NumericalValue.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : NumericalValue α) : map g (map f x) = map (g ∘ f) x

Successive maps fuse into a single map of the composed function.

@[simp]

theorem FloatLib.Numerics.NumericalValue.finite?_map {α : Type u} {β : Type v} (f : α → β) (x : NumericalValue α) : (map f x).finite? = Option.map f x.finite?

Extracting a finite payload commutes with mapping its scalar value.