TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Reduction.Tree

Finite, repeatedly rounded binary sums #

Each internal node uses Model.add, with one nearest-even rounding at that node. A finite execution certificate excludes exceptional inputs and overflow at every intermediate result. The error budget then follows from FloatLib's half-ULP theorem, including subnormal values. This API does not change Model.sum, which accumulates exactly and rounds only once.

Each finite addition also has relative error at most unitRoundoffAt fmt, with no underflow term, because a sum of two grid points below the normal range is exact. This discharges the local premise of the mixed and geometric reduction bounds for Model.add trees.

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.FiniteEval {fmt : FloatFormat} :
Numerics.ReductionTree (Model fmt) → Prop

All leaves and intermediate additions have real denotations.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.FiniteEval.isFinite_eval {fmt : FloatFormat} {t : Numerics.ReductionTree (Model fmt)} (h : FiniteEval t) :
    (Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id t).isFinite = true

    Finiteness of the root is part of a finite execution certificate.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.toReal_eval {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
    (Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id t).toReal = Numerics.ReductionTree.eval (fun (x y : ℝ) => roundAt fmt (x + y)) toReal t

    The rounded real interpretation agrees with encoded execution at each finite node.

    source
    noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.errorBudget {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) :
    ℝ

    The sum of half-ULPs at the actual intermediate additions.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_sum_le {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
      |(Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id t).toReal - (List.map toReal t.leaves).sum| ≤ errorBudget t

      No normal-range hypothesis is needed: each finite addition has an absolute half-ULP bound.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_eval_le {fmt : FloatFormat} {a b : Numerics.ReductionTree (Model fmt)} (hfmt : fmt.isIEEE = true) (ha : FiniteEval a) (hb : FiniteEval b) (hperm : a.leaves.Perm b.leaves) :
      |(Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id a).toReal - (Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id b).toReal| ≤ errorBudget a + errorBudget b

      Two finite schedules over the same inputs can differ by at most their combined budgets.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.allNodes_abs_toReal_add_sub_le {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
      Numerics.ReductionTree.AllNodes (fun (x y : Model fmt) => x.add y) id (fun (x y : Model fmt) => |toReal (x.add y) - (x.toReal + y.toReal)| ≤ unitRoundoffAt fmt * (|x.toReal| + |y.toReal|)) t

      Every finite addition in the tree has relative error at most unitRoundoffAt fmt, measured against the magnitudes of its two operands, with no underflow allowance.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_sum_le_mixedBudget {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
      |(Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id t).toReal - (List.map toReal t.leaves).sum| ≤ Numerics.ReductionTree.mixedBudget toReal (unitRoundoffAt fmt) 0 t

      A finite IEEE reduction tree satisfies the mixed-budget bound with relative allowance unitRoundoffAt fmt and zero absolute allowance, including subnormal intermediate results.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_sum_le_geometric {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
      |(Numerics.ReductionTree.eval (fun (x y : Model fmt) => x.add y) id t).toReal - (List.map toReal t.leaves).sum| ≤ ((1 + unitRoundoffAt fmt) ^ t.nodeCount - 1) * Numerics.ReductionTree.sumAbs toReal t

      A finite IEEE reduction tree with n additions has error at most ((1 + u)^n - 1) * Σ|xᵢ| for u = unitRoundoffAt fmt, with no normal-range hypothesis.