symmetry log of sum of exp

Average Accuracy: 53.4% → 99.0%

Time: 16.8s

Precision: binary64

Cost: 25924

\[ \begin{array}{c}[a, b] = \mathsf{sort}([a, b])\\ \end{array} \]

Math

\[\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right) \]

↓

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{expm1.f64}\left(b\right)\right)\right)\\ \end{array} \]

FPCore

(FPCore (a b) :precision binary64 (log.f64 (+.f64 (exp.f64 a) (exp.f64 b))))

↓

(FPCore (a b)
 :precision binary64
 (if (<=.f64 (exp.f64 a) 0)
   (/.f64 b (+.f64 (exp.f64 a) 1))
   (log1p.f64 (+.f64 (exp.f64 a) (expm1.f64 b)))))

Derivation

1. Split input into 2 regimes

2. if (exp.f64 a) < 0.0

   1. Initial program 9.2%

      \[\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right) \]

   2. Taylor expanded in b around 0 100.0%

      \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right), \mathsf{/.f64}\left(b, \mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right)\right)} \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{log1p.f64}\left(\mathsf{exp.f64}\left(a\right)\right), \mathsf{/.f64}\left(b, \mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right)\right)} \]
      Proof

      [Start] 100.0	\[ \mathsf{+.f64}\left(\mathsf{log.f64}\left(\mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right), \mathsf{/.f64}\left(b, \mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right)\right) \]
      log1p-def [=>] 100.0	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{log1p.f64}\left(\mathsf{exp.f64}\left(a\right)\right)}, \mathsf{/.f64}\left(b, \mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right)\right) \]

   4. Taylor expanded in b around inf 100.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(1, \mathsf{exp.f64}\left(a\right)\right)\right)} \]

   if 0.0 < (exp.f64 a)

   1. Initial program 97.5%

      \[\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right) \]

   2. Applied egg-rr 96.1%

      \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right), \mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 97.5	\[ \mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right) \]
      add-sqr-sqrt [=>] 95.3	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)}\right) \]
      log-prod [=>] 96.1	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right), \mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)\right)} \]

   3. Simplified 98.1%

      \[\leadsto \color{blue}{\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{expm1.f64}\left(b\right)\right)\right)} \]
      Proof

      [Start] 96.1	\[ \mathsf{+.f64}\left(\mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right), \mathsf{log.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)\right) \]
      log-prod [<=] 95.3	\[ \color{blue}{\mathsf{log.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)\right)} \]
      rem-square-sqrt [=>] 97.5	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)}\right) \]
      log1p-expm1 [<=] 97.5	\[ \color{blue}{\mathsf{log1p.f64}\left(\mathsf{expm1.f64}\left(\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right)\right)} \]
      expm1-def [<=] 97.5	\[ \mathsf{log1p.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\right), 1\right)}\right) \]
      rem-exp-log [=>] 97.5	\[ \mathsf{log1p.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)}, 1\right)\right) \]
      associate--l+ [=>] 97.9	\[ \mathsf{log1p.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{\_.f64}\left(\mathsf{exp.f64}\left(b\right), 1\right)\right)}\right) \]
      expm1-def [=>] 98.1	\[ \mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \color{blue}{\mathsf{expm1.f64}\left(b\right)}\right)\right) \]

3. Recombined 2 regimes into one program.

4. Final simplification 99.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{expm1.f64}\left(b\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	98.7%
Cost	25924

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log.f64}\left(\mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), \mathsf{exp.f64}\left(b\right)\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	98.5%
Cost	19648

\[\mathsf{+.f64}\left(\mathsf{log1p.f64}\left(\mathsf{exp.f64}\left(a\right)\right), \mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\right) \]

Alternative 3
Accuracy	98.1%
Cost	19524

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), \frac{3602879701896397}{18014398509481984}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(a, \mathsf{exp.f64}\left(b\right)\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	97.5%
Cost	19396

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p.f64}\left(\mathsf{exp.f64}\left(b\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	97.6%
Cost	13636

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), \frac{3602879701896397}{18014398509481984}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log.f64}\left(\mathsf{+.f64}\left(2, \mathsf{+.f64}\left(\mathsf{+.f64}\left(a, b\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(b, b\right)\right)\right)\right)\right)\\ \end{array} \]

Alternative 6
Accuracy	97.0%
Cost	13252

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{exp.f64}\left(a\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{+.f64}\left(\mathsf{exp.f64}\left(a\right), 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, \frac{1}{2}\right), \mathsf{log.f64}\left(2\right)\right)\\ \end{array} \]

Alternative 7
Accuracy	56.4%
Cost	6852

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, -155\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, \frac{1}{2}\right), \mathsf{log.f64}\left(2\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	56.4%
Cost	6724

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, -1\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log.f64}\left(\mathsf{+.f64}\left(a, 2\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	56.3%
Cost	6724

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, -114\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log.f64}\left(\mathsf{+.f64}\left(b, 2\right)\right)\\ \end{array} \]

Alternative 10
Accuracy	56.3%
Cost	6724

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, -155\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(b, 1\right)\right)\\ \end{array} \]

Alternative 11
Accuracy	55.8%
Cost	6596

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, -135\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \frac{1}{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log.f64}\left(2\right)\\ \end{array} \]

Alternative 12
Accuracy	12.0%
Cost	192

\[\mathsf{*.f64}\left(b, \frac{1}{2}\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (a b)
  :name "symmetry log of sum of exp"
  :precision binary64
  (log (+ (exp a) (exp b))))