TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Elementary.Runtime

Natural exponential and logarithm for posits #

Each operation compares its exact mathematical result with the posit rounding boundaries. Adaptive rational enclosures resolve the comparisons, with termination proved in the format-independent numerics layer. No intermediate posit rounding occurs in expMinus1 or logPlus1.

The operation and domain rules follow the Posit Standard (2022), §§5.1 and 5.5.

source
def FloatLib.Floats.Formats.Posit.Model.Elementary.expRat (format : Format) (argument offset : ℚ) :
Model format

Round the exponential of a rational, optionally subtracting an exact offset first.

Instances For
    source
    def FloatLib.Floats.Formats.Posit.Model.Elementary.logRat (format : Format) (argument : ℚ) :
    Model format

    Round the natural logarithm of a positive rational; reject other arguments.

    Instances For
      source
      def FloatLib.Floats.Formats.Posit.Model.Elementary.applyExp {format : Format} (offset : ℚ) (value : Model format) :
      Model format

      Lift exponential evaluation and exact output subtraction, propagating NaR.

      Instances For
        source
        def FloatLib.Floats.Formats.Posit.Model.Elementary.applyLog {format : Format} (offset : ℚ) (value : Model format) :
        Model format

        Form the logarithm argument exactly before evaluation and one final rounding.

        Instances For
          source
          def FloatLib.Floats.Formats.Posit.Model.exp {format : Format} (value : Model format) :
          Model format

          Correctly rounded natural exponential. NaR propagates.

          Instances For
            source
            def FloatLib.Floats.Formats.Posit.Model.expMinus1 {format : Format} (value : Model format) :
            Model format

            Correctly rounded exp x - 1, with no intermediate rounding of the exponential.

            Instances For
              source
              def FloatLib.Floats.Formats.Posit.Model.log {format : Format} (value : Model format) :
              Model format

              Correctly rounded natural logarithm. Nonpositive inputs and NaR produce NaR.

              Instances For
                source
                def FloatLib.Floats.Formats.Posit.Model.logPlus1 {format : Format} (value : Model format) :
                Model format

                Correctly rounded log (1 + x), with no intermediate rounding of the addition.

                Instances For