TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Quantization.Directed

Directed relational quantization #

These specifications characterize rounding toward negative and positive infinity as selection of the lower or upper representable neighbor. They permit duplicate encodings of the same scalar and therefore remain relational even when the selected mathematical value is unique.

The selected neighbor must be finite. These relations do not specify an overflow result when the required finite neighbor does not exist.

source
def FloatLib.Numerics.Quantization.Directed.towardNegative (system : NumericalSystem) [Preorder system.Scalar] :
Spec Unit system.Scalar system.Code

Relational specification for rounding toward negative infinity.

Instances For
    source
    def FloatLib.Numerics.Quantization.Directed.towardPositive (system : NumericalSystem) [Preorder system.Scalar] :
    Spec Unit system.Scalar system.Code

    Relational specification for rounding toward positive infinity.

    Instances For
      source
      theorem FloatLib.Numerics.Quantization.Directed.towardNegative_isFinite {system : NumericalSystem} [Preorder system.Scalar] {input : system.Scalar} {code : system.Code} (hcode : towardNegative system () input code) :
      system.IsFinite code

      A downward-directed result has a finite denotation.

      source
      theorem FloatLib.Numerics.Quantization.Directed.towardPositive_isFinite {system : NumericalSystem} [Preorder system.Scalar] {input : system.Scalar} {code : system.Code} (hcode : towardPositive system () input code) :
      system.IsFinite code

      An upward-directed result has a finite denotation.