TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Reduction.Tree

Configured reduction schedules #

Decoding commutes with a reduction that rounds at every addition, independently of the storage plan. Nearest-even finite executions inherit the model's half-ULP error budget. The round-once collection API is separate.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_eval_tree {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (t : Numerics.ReductionTree (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) :
(Numerics.ReductionTree.eval (fun (x y : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) => x.add y mode) id t).toModel = Numerics.ReductionTree.eval (fun (x y : Formats.BinaryInterchange.Model format) => x.add y mode) id (Numerics.ReductionTree.map toModel t)

Decoding commutes with evaluating a schedule that rounds each addition in mode, for an addition capability whose reference operation is the configured model addition, as toModel_add requires.

source
theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_eval_tree_sub_sum_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (t : Numerics.ReductionTree (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (hformat : format.isIEEE = true) (hfinite : Formats.BinaryInterchange.Model.ReductionTree.FiniteEval (Numerics.ReductionTree.map toModel t)) :
|(Numerics.ReductionTree.eval (fun (x y : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) => x.add y) id t).toModel.toReal - (List.map (Formats.BinaryInterchange.Model.toReal ∘ toModel) t.leaves).sum| ≤ Formats.BinaryInterchange.Model.ReductionTree.errorBudget (Numerics.ReductionTree.map toModel t)

Configured nearest-even execution on an IEEE descriptor inherits the finite model's absolute error enclosure, for an addition capability whose reference operation is the configured model addition.