TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Core.Representation

Encoded numerical formats #

EncodedFormat F assigns a code type and finite scalar domain to a format identity F. Codes can be machine words, limb records, blocks, codebook indices, or runtime-sized values.

FormatSemantics F supplies the denotation separately. A real-valued denotation can then be noncomputable while storage and arithmetic remain executable. Together the classes define a NumericalSystem; optional capabilities add laws and operations as needed.

These interfaces also cover representations without a radix/exponent description. For the radix-based generic-format approach, see Boldo and Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq (2011), https://doi.org/10.1109/ARITH.2011.40.

source
class FloatLib.Numerics.EncodedFormat (F : Type u) :
Type (max (v + 1) (w + 1))

Runtime storage and finite scalar domain associated with the format identity F.

  • Code : Type v

    Concrete runtime storage selected by F.

  • Scalar : Type w

    Ordinary finite semantic domain selected by F.

Instances
    source
    class FloatLib.Numerics.FormatSemantics (F : Type u) [EncodedFormat F] :
    Type (max u_1 u_2)

    Complete semantic interpretation of a format's runtime codes.

    Instances
      source
      @[reducible, inline]
      abbrev FloatLib.Numerics.FormatCode (F : Type u) [EncodedFormat F] :
      Type u_1

      Runtime storage selected by F.

      Instances For
        source
        @[reducible, inline]
        abbrev FloatLib.Numerics.FormatScalar (F : Type u) [EncodedFormat F] :
        Type u_2

        Ordinary finite semantic domain selected by F.

        Instances For
          source
          @[instance_reducible]
          def FloatLib.Numerics.FormatSemantics.ofFinite (F : Type u) [EncodedFormat F] (decode : FormatCode F → FormatScalar F) :
          FormatSemantics F

          Build format semantics when every stored code has an ordinary finite interpretation.

          Instances For
            source
            @[inline]
            def FloatLib.Numerics.denoteFormat (F : Type u) [EncodedFormat F] [FormatSemantics F] (code : FormatCode F) :
            NumericalValue (FormatScalar F)

            Complete interpretation of one code in F.

            Instances For
              source
              @[reducible]
              def FloatLib.Numerics.formatSystem (F : Type u) [EncodedFormat F] [FormatSemantics F] :
              NumericalSystem

              The general numerical system assembled from a format's storage and denotation.

              The wrapper is reducible so Lean can reuse structures on FormatCode F and FormatScalar F through NumericalSystem.Code and NumericalSystem.Scalar without forwarding instances.

              Instances For
                source
                @[reducible, inline]
                abbrev FloatLib.Numerics.FormatRepresents (F : Type u) [EncodedFormat F] [FormatSemantics F] (code : FormatCode F) (value : FormatScalar F) :
                Prop

                A format code represents the ordinary scalar value.

                Instances For
                  source
                  class FloatLib.Numerics.HasExactSemantics (F : Type u) [EncodedFormat F] [FormatSemantics F] :
                  Type (max (max u_1 u_2) (x + 1))

                  Optional rich exact semantics for a type-directed format.

                  This capability is proof-facing. Executable kernels should call concrete family decoders rather than project through exactSemantics in an arithmetic loop.

                  Instances