efp_plus Function

public pure function efp_plus(a, b) result(c)

Exact bin-wise integer addition, REGULARISED (not merely carried). Order-invariant BIT-FOR-BIT: efp_plus(a,b)%v == efp_plus(b,a)%v, and a running fold acc = efp_plus(acc, x_i) over any permutation of the x_i converges to the SAME raw bins (not merely the same reconstructed real) – test_efp_order_invariant asserts this on %v(:) directly, per the plan’s §9.2.

efp_carry alone is NOT sufficient here: it only bounds each bin’s MAGNITUDE (|e(n)| < 2**P), and a magnitude-bounded but mixed-sign bin vector is a REDUNDANT (non-unique) representation of a given value – e.g. [e2=1, e3=-(2**P-100)] and [e2=0, e3=100] both represent the value 100, but differ bit-for-bit. Two different accumulation orders can land on different members of that redundant family even though the represented value is identical. efp_regularize additionally forces every bin to share the overall sign, which – like ordinary sign-magnitude fixed-radix representations – IS unique for a given value, closing that gap. Non-finite propagation: c%poison = a%poison + b%poison, so a poisoned operand on EITHER side stays poisoned in the result (see efp_t’s docstring) – purely additive, so it composes correctly through any accumulation order, matching the order-invariance this function otherwise guarantees.

Arguments

Type IntentOptional Attributes Name
type(efp_t), intent(in) :: a
type(efp_t), intent(in) :: b

Return Value type(efp_t)


Calls

proc~~efp_plus~~CallsGraph proc~efp_plus efp_plus proc~efp_regularize efp_regularize proc~efp_plus->proc~efp_regularize proc~efp_carry efp_carry proc~efp_regularize->proc~efp_carry

Source Code

   pure function efp_plus(a, b) result(c)
      !! Exact bin-wise integer addition, REGULARISED (not merely
      !! carried).  Order-invariant BIT-FOR-BIT:
      !! `efp_plus(a,b)%v == efp_plus(b,a)%v`, and a running fold
      !! `acc = efp_plus(acc, x_i)` over any permutation of the `x_i`
      !! converges to the SAME raw bins (not merely the same reconstructed
      !! real) -- `test_efp_order_invariant` asserts this on `%v(:)`
      !! directly, per the plan's §9.2.
      !!
      !! `efp_carry` alone is NOT sufficient here: it only bounds each
      !! bin's MAGNITUDE (`|e(n)| < 2**P`), and a magnitude-bounded but
      !! mixed-sign bin vector is a REDUNDANT (non-unique) representation
      !! of a given value -- e.g. `[e2=1, e3=-(2**P-100)]` and
      !! `[e2=0, e3=100]` both represent the value `100`, but differ
      !! bit-for-bit.  Two different accumulation orders can land on
      !! different members of that redundant family even though the
      !! represented value is identical.  `efp_regularize` additionally
      !! forces every bin to share the overall sign, which -- like
      !! ordinary sign-magnitude fixed-radix representations -- IS
      !! unique for a given value, closing that gap.
      !! Non-finite propagation: `c%poison = a%poison + b%poison`, so a
      !! poisoned operand on EITHER side stays poisoned in the result (see
      !! `efp_t`'s docstring) -- purely additive, so it composes correctly
      !! through any accumulation order, matching the order-invariance
      !! this function otherwise guarantees.
      type(efp_t), intent(in) :: a, b
      type(efp_t) :: c
      c%v = a%v + b%v
      call efp_regularize(c%v)
      c%poison = a%poison + b%poison
   end function efp_plus