4 ms·

They meant algebraic in the sense of https://en.wikipedia.org/wiki/Algebraic_operation https://en.wikipedia.org/wiki/Algebraic_operation.

bigbillheck 4y ago
Sure, but to be honest I'm a little bit boggled at the idea of a phd mathematician finding trig manipulation hard enough to be worth commenting on.
- eesmith 4y ago
  This review of Wildberger's book at https://philarchive.org/archive/FRADPR https://philarchive.org/archive/FRADPR says the point isn't that the PhD mathematician finds trig hard, but rather to beginners: > ... very becoming-numerate generation invests enormous effort in the painful calculation of the lengths and angles of complicated figures. Surveying, navigation and computer graphics are intensive users of the results. Much of that effort is wasted, Wildberger argues. The concentration on angles, especially, is a result of the historical accident that serious study of the subject began with spherical trigonometry for astronomy and long-range navigation, which meant there was altogether too much attention given to circles. ... > Having things done better is one major payoff, but equally important would be a removal of a substantial blockage to the education of young mathematicians, the waterless badlands of traditional trigonometry that youth eager to reach the delights of higher mathematics must spend painful years crossing Whether that's correct is different. https://handwiki.org/wiki/Rational_trigonometry https://handwiki.org/wiki/Rational_trigonometry seems to give a good description of opposing views.
  - bigbillheck 4y ago
    I don't have a particularly high opinion of John D. Cook but I still wouldn't call him a 'beginner'.
    - eesmith 4y ago
      I apologize. I misread the context of the thread. I mistakenly though you were commenting on Wildberger's reasoning for promoting rational trigonometry, rather than on Cook's decision to use that approach. If "formal verification" involves using a software-based proof assistant or automatic theorem prover then perhaps that easier to encode for those tools via rational trigonometry? Why not ask him directly?
- chriswarbo 4y ago
  Cook isn't proving results about trig functions/identities; they're proving results about software. Software can never correctly implement trig functions; it must always approximate, and that is the reason it's hard to verify. In contrast, arithmetic on rational numbers can be implemented exactly; at least, up to the memory limits of the machine (e.g. using pair of bignums for numerator/denominator)

bigbillheck 4y ago

Sure, but to be honest I'm a little bit boggled at the idea of a phd mathematician finding trig manipulation hard enough to be worth commenting on.

eesmith 4y ago
This review of Wildberger's book at https://philarchive.org/archive/FRADPR https://philarchive.org/archive/FRADPR says the point isn't that the PhD mathematician finds trig hard, but rather to beginners: > ... very becoming-numerate generation invests enormous effort in the painful calculation of the lengths and angles of complicated figures. Surveying, navigation and computer graphics are intensive users of the results. Much of that effort is wasted, Wildberger argues. The concentration on angles, especially, is a result of the historical accident that serious study of the subject began with spherical trigonometry for astronomy and long-range navigation, which meant there was altogether too much attention given to circles. ... > Having things done better is one major payoff, but equally important would be a removal of a substantial blockage to the education of young mathematicians, the waterless badlands of traditional trigonometry that youth eager to reach the delights of higher mathematics must spend painful years crossing Whether that's correct is different. https://handwiki.org/wiki/Rational_trigonometry https://handwiki.org/wiki/Rational_trigonometry seems to give a good description of opposing views.
- bigbillheck 4y ago
  I don't have a particularly high opinion of John D. Cook but I still wouldn't call him a 'beginner'.
  - eesmith 4y ago
    I apologize. I misread the context of the thread. I mistakenly though you were commenting on Wildberger's reasoning for promoting rational trigonometry, rather than on Cook's decision to use that approach. If "formal verification" involves using a software-based proof assistant or automatic theorem prover then perhaps that easier to encode for those tools via rational trigonometry? Why not ask him directly?
chriswarbo 4y ago
Cook isn't proving results about trig functions/identities; they're proving results about software. Software can never correctly implement trig functions; it must always approximate, and that is the reason it's hard to verify. In contrast, arithmetic on rational numbers can be implemented exactly; at least, up to the memory limits of the machine (e.g. using pair of bignums for numerator/denominator)