Quotient of products

Average Accuracy: 82.4% → 94.4%

Time: 6.1s

Precision: binary64

Cost: 2512

\[ \begin{array}{c}[a1, a2] = \mathsf{sort}([a1, a2])\\ [b1, b2] = \mathsf{sort}([b1, b2])\\ \end{array} \]

Math

\[\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]

↓

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -\infty\right):\\ \;\;\;\;\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, \frac{-441252181048159}{88250436209631796779659651318894620729729809745361797646356310339459182198787453122058560031100937405340558296821374893066353027058699717113329784015217065825962377858834878767894752265396985241367417483713579073929216}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(a2, \mathsf{/.f64}\left(a1, b1\right)\right), b2\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 200000000000000013104522191493575712823499934020710488024152771323555056217860874303389432945676521361520476916974680482142243229285217375886207988634517594158208309292880167137262965343121750872846190603318440437028470611163773764115697127698584069380700520547655522189312\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)\\ \end{array} \]

FPCore

(FPCore (a1 a2 b1 b2) :precision binary64 (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)))

↓

(FPCore (a1 a2 b1 b2)
 :precision binary64
 (let* ((t_0 (/.f64 (*.f64 a1 a2) (*.f64 b1 b2))))
   (if (<=.f64 t_0 -inf.0)
     (/.f64 a1 (/.f64 b1 (/.f64 a2 b2)))
     (if (<=.f64
          t_0
          -441252181048159/88250436209631796779659651318894620729729809745361797646356310339459182198787453122058560031100937405340558296821374893066353027058699717113329784015217065825962377858834878767894752265396985241367417483713579073929216)
       t_0
       (if (<=.f64 t_0 0)
         (/.f64 (*.f64 a2 (/.f64 a1 b1)) b2)
         (if (<=.f64
              t_0
              200000000000000013104522191493575712823499934020710488024152771323555056217860874303389432945676521361520476916974680482142243229285217375886207988634517594158208309292880167137262965343121750872846190603318440437028470611163773764115697127698584069380700520547655522189312)
           t_0
           (*.f64 (/.f64 a2 b1) (/.f64 a1 b2))))))))

Target

Original	82.4%
Target	82.4%
Herbie	94.4%

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right) \]

Derivation

1. Split input into 4 regimes

2. if (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < -inf.0

   1. Initial program 0.0%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]

   2. Simplified 83.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right)} \]
      Proof

      [Start] 0.0	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]
      times-frac [=>] 83.7	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right)} \]

   3. Applied egg-rr 69.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)} \]
      Proof

      [Start] 83.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right) \]
      associate-*l/ [=>] 71.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, \mathsf{/.f64}\left(a2, b2\right)\right), b1\right)} \]
      associate-/l* [=>] 69.7	\[ \color{blue}{\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)} \]

   if -inf.0 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < -5.0000000000000002e-204 or 0.0 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < 2.0000000000000001e272

   1. Initial program 98.9%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]

   if -5.0000000000000002e-204 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < 0.0

   1. Initial program 81.1%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]

   2. Simplified 93.3%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right)} \]
      Proof

      [Start] 81.1	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]
      times-frac [=>] 93.3	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right)} \]

   3. Applied egg-rr 91.5%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), a2\right), b2\right)} \]
      Proof

      [Start] 93.3	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), \mathsf{/.f64}\left(a2, b2\right)\right) \]
      associate-*r/ [=>] 91.5	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b1\right), a2\right), b2\right)} \]

   if 2.0000000000000001e272 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2))

   1. Initial program 10.7%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]

   2. Simplified 74.2%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b2, \mathsf{/.f64}\left(a2, b1\right)\right)\right)} \]
      Proof

      [Start] 10.7	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right) \]
      associate-/l* [=>] 33.3	\[ \color{blue}{\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(b1, b2\right), a2\right)\right)} \]
      *-commutative [=>] 33.3	\[ \mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(b2, b1\right)}, a2\right)\right) \]
      associate-/l* [=>] 74.2	\[ \mathsf{/.f64}\left(a1, \color{blue}{\mathsf{/.f64}\left(b2, \mathsf{/.f64}\left(a2, b1\right)\right)}\right) \]

   3. Taylor expanded in a1 around 0 10.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b2, b1\right)\right)} \]

   4. Simplified 87.0%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)} \]
      Proof

      [Start] 10.7	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b2, b1\right)\right) \]
      times-frac [=>] 87.0	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a1, b2\right), \mathsf{/.f64}\left(a2, b1\right)\right)} \]
      *-commutative [=>] 87.0	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)} \]

3. Recombined 4 regimes into one program.

4. Final simplification 94.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right), -\infty\right):\\ \;\;\;\;\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right), \frac{-441252181048159}{88250436209631796779659651318894620729729809745361797646356310339459182198787453122058560031100937405340558296821374893066353027058699717113329784015217065825962377858834878767894752265396985241367417483713579073929216}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right), 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(a2, \mathsf{/.f64}\left(a1, b1\right)\right), b2\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right), 200000000000000013104522191493575712823499934020710488024152771323555056217860874303389432945676521361520476916974680482142243229285217375886207988634517594158208309292880167137262965343121750872846190603318440437028470611163773764115697127698584069380700520547655522189312\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	95.7%
Cost	2512

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(a1, a2\right), \mathsf{*.f64}\left(b1, b2\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -\infty\right):\\ \;\;\;\;\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, \frac{-7613526571406249}{76135265714062492815260799905274908678720522324960996303655519196976161646612703925512617702203205150197694658057880220183274764571899172238890525752442604840088107030909945545865544183516044127756246824056393584950668733792147460513643465745851293850216709399252168336576785859311828992}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 0\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b2\right), \mathsf{/.f64}\left(a1, b1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 200000000000000013104522191493575712823499934020710488024152771323555056217860874303389432945676521361520476916974680482142243229285217375886207988634517594158208309292880167137262965343121750872846190603318440437028470611163773764115697127698584069380700520547655522189312\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	82.2%
Cost	1110

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a2, \frac{-2995397108520247}{26046931378436930758124421057504913270096712196546516251547882077203270460225125279380594534654508948214569963255598595491753131461403769845169359579417304867559209294976619368996399554343023534097519594280807038990979484521392426918608896}\right) \lor \neg \mathsf{<=.f64}\left(a2, 1799999999999999988291959437090428727963002712946237386237988089314114797568\right) \land \left(\mathsf{<=.f64}\left(a2, 90000000000000007843102429419300317433183618530018679196110939888988490598528516192152653788175075844402778860506139422707209469952\right) \lor \neg \mathsf{<=.f64}\left(a2, 25000000000000000044583748714697959128640910640075348177675381942532375711947488390511717699821074024969224259055244558910951911507907155863438295813140861851533312\right) \land \mathsf{<=.f64}\left(a2, 619999999999999962621818879509338381386630634298752624957865845034283437883237656919705854742632550258793739482984829181444180138372200835436481781184421768711927593005769327927746740285720102401487777040822631219679491582907645952\right)\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b2\right), \mathsf{/.f64}\left(a1, b1\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	82.2%
Cost	977

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a1, -1400000000000000065242530044748976595767120133929127605989372641226155893852320819401874797099873997249447567234379685811444166332409657327904870936489700816822402178314242710659282088253077333657043630080184339898096943104\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b1\right), \mathsf{/.f64}\left(a1, b2\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(a1, -30000000000000002288930952327566100988489491283968\right) \lor \neg \mathsf{<=.f64}\left(a1, \frac{-3968087202183751}{203491651394038521547847039511757134922630564035519658215217828728150550470508791245160894801988351157926327837934364027279321339542216951915385621714197694277806322617004838820284371518304871360136871830318804992117027222823378335301632}\right) \land \mathsf{<=.f64}\left(a1, \frac{5639583590386471}{24519928653854221733733552434404946937899825954937634816}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b2\right), \mathsf{/.f64}\left(a1, b1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b2, \mathsf{/.f64}\left(a2, b1\right)\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	83.9%
Cost	976

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(b1, b2\right), a2\right)\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b2\right), \mathsf{/.f64}\left(a1, b1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(b1, -1050000000000000083451894193183225223380418638772480878139616948604628707926215895366211738206236283543061889990792898121254712840699179674325774269153280\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b1, \frac{-944473296573929}{4722366482869645213696}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b1, \frac{741219189357827}{49414612623855131433714684257548170666395666446323759364477870612165610246092613987295015552108672972457782681717971658054152523775828485563235693344906862773807964911271084317496803647971976645810490155877135026504396358257981615873560389562783094809768080203212590222737650052546509407272052614415528872877858335227904}\right):\\ \;\;\;\;\mathsf{/.f64}\left(a1, \mathsf{/.f64}\left(b1, \mathsf{/.f64}\left(a2, b2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b1, \frac{348449143727041}{696898287454081973172991196020261297061888}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 5
Accuracy	82.4%
Cost	448

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(a2, b2\right), \mathsf{/.f64}\left(a1, b1\right)\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (a1 a2 b1 b2)
  :name "Quotient of products"
  :precision binary64

  :herbie-target
  (* (/ a1 b1) (/ a2 b2))

  (/ (* a1 a2) (* b1 b2)))