Meeting Notes

Jump to bottom Edit New page

Zach Tatlock edited this page Oct 25, 2013 · 10 revisions

2013-10-25 @ 9:30am

2D conceptual framework:

(A) equiv over R vs. (B) float error reduced
A handled by CAS, B seems harder
prove equivalence over the reals?
yes
- prove error over floats reduced?
- yes
  - does no harm
  - most demanding case
  - probably produce slowest code
  - for critical software
- no
  - more aggressive error optimization
  - result "correct" over reals... but who cares?
  - perhaps this case makes least sense?
  - how to eval? who is this for?
no
- prove error over floats reduced?
- yes
  - so non-equiv real, but better error wrt to spec for float
  - seems weird! lets us use stuff that "works" but we can't prove
    - Akshay's complex differentiation trick
    - taylor series expansion
  - still appropriate for critical software?
- no
  - best effort
  - should produce fastest code (?)

TODO