LAProof.accuracy_proofs.sum_acc

Floating-Point Summation Accuracy Theorems

This file establishes backward and forward error bounds for floating-point summation, in both list-based and ordinal-indexed forms.

Error Factors

Throughout, the accumulated relative error factor is \(g(n) = (1 + \mathbf{u})^n - 1\), where \(\mathbf{u}\) is the unit roundoff for the given floating-point type. It is defined in common.

Main Results

  • bSUM: Shows that the computed floating-point sum can be expressed as the exact sum of a slightly perturbed input list. Each input element is perturbed by a relative factor bounded by \(g(n-1)\), where \(n\) is the list length.
  • Fsum_backward_error: The ordinal-indexed analogue of bSUM, expressing the same backward error bound for functions indexed by finite ordinals.
  • fSUM: Bounds the absolute forward error of the computed sum by \(g(n) \cdot \sum |x_i|\), where \(n\) is the list length.
  • Fsum_forward_error: The ordinal-indexed analogue of fSUM.
  • sum_forward_error_permute: Shows that the forward error bound is stable under permutation of the input list, so the bound holds regardless of the order in which elements are summed.

Dependencies

This file relies on:
  • preamble, common: basic setup and shared definitions
  • sum_model: the floating-point summation model sumF and sumR
  • float_acc_lems: elementary floating-point accuracy lemmas

From LAProof.accuracy_proofs Require Import
  preamble
  common
  sum_model
  float_acc_lems.

Require LAProof.accuracy_proofs.mv_mathcomp.
Require Import Permutation.

Section WithNan.

Context {NAN : FPCore.Nans} {t : type}.

Notation g := (@g t).
Notation D := (@default_rel t).
Notation neg_zero := (@common.neg_zero t).

Backward Error: List Version

bSUM expresses the computed floating-point sum as the exact real sum of a slightly perturbed input list. Each element of the perturbed list differs from the corresponding input by a relative factor bounded by \(g(n-1)\), where \(n\) is the list length.

Theorem bSUM :
  ∀ (x : list (ftype t))
         (Hfin : Binary.is_finite (sumF x)),
  ∃ (x' : list R),
    size x' = size x ∧
    FT2R (sumF x) = sumR x' ∧
    (∀ n,
      (n < size x')%nat →
      ∃ delta,
        nth 0 x' n = FT2R (nth neg_zero x n) × (1 + delta) ∧
        Rabs delta ≤ g (size x' - 1)).

Backward Error: Indexed Version

Fsum_backward_error lifts bSUM to functions indexed by finite ordinals. The computed sum equals the exact sum of a perturbed family, with each element perturbed by a relative factor bounded by \(g(n-1)\).

Theorem Fsum_backward_error :
  ∀ [n] (x : 'I_n → ftype t)
         (Hfin : Binary.is_finite (mv_mathcomp.F.sum x)),
  ∃ (x' : 'I_n → R),
    FT2R (mv_mathcomp.F.sum x) = \sum_i x' i ∧
    (∀ i : 'I_n,
      ∃ delta,
        x' i = FT2R (x i) × (1 + delta) ∧
        Rabs delta ≤ g (n - 1)).

Forward Error: List Version

fSUM bounds the absolute forward error of the computed floating-point sum by \(g(n) \cdot \sum |x_i|\), where \(n\) is the list length and \(|x_i|\) denotes the componentwise absolute values of the inputs.

Theorem fSUM :
  ∀ (x : list (ftype t))
         (Hfin : Binary.is_finite (sumF x)),
    Rabs (sumR (map FT2R x) - FT2R (sumF x)) ≤
      g (size x) × sumR (map Rabs (map FT2R x)).

Forward Error: Indexed Version

Fsum_forward_error lifts fSUM to functions indexed by finite ordinals, giving the same \(g(n) \cdot \sum |x_i|\) bound for the absolute forward error of the indexed sum.

Lemma Fsum_forward_error :
  ∀ [n] (x : 'I_n → ftype t)
         (Hfin : Binary.is_finite (mv_mathcomp.F.sum x)),
    Rabs (\sum_i (FT2R (x i)) - FT2R (mv_mathcomp.F.sum x)) ≤
      g n × (\sum_i (Rabs (FT2R (x i)))).

Forward Error Under Permutation

sum_forward_error_permute' is an auxiliary lemma: when two lists are permutations of each other, the forward error bound for the computed sum of either list can be expressed using the length of the original list. Used internally by sum_forward_error_permute.

Lemma sum_forward_error_permute' :
  ∀ (x x0 : list (ftype t))
         (Hfin : Binary.is_finite (sumF x))
         (Hfin0 : Binary.is_finite (sumF x0))
         (Hper : Permutation x x0),
    Rabs ((sumR (map FT2R x0)) - FT2R (sumF x0)) ≤
      g (size x) × (sumR (map Rabs (map FT2R x0))).

sum_forward_error_permute shows that the forward error bound for the computed sum is invariant under permutation of the input. If two lists are permutations of each other, the absolute forward error for either computed sum is bounded by \(g(n) \cdot \sum |x_i|\) using the shared element set and length \(n\).

Theorem sum_forward_error_permute :
  ∀ (x x0 : list (ftype t))
         (Hfin : Binary.is_finite (sumF x))
         (Hfin0 : Binary.is_finite (sumF x0))
         (Hper : Permutation x x0),
    Rabs ((sumR (map FT2R x)) - FT2R (sumF x0)) ≤
      g (size x) × (sumR (map Rabs (map FT2R x))).

End WithNan.