■
Coqで高精度計算サイト
高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。
それは大きな数を扱うことができないということである。
例えば10^10000000のような大変大きな計算を実行すると答えは無限∞になってしまう。
このため、例えば(10^100000000)^(1/100000000)のように結果が10になるような計算式でも、途中で大きな数が含まれてしまうので結果は誤った値になってしまう。
この問題を訂正すべく、Coqの有理数演算を使って、似たようなサイトを作ってみた。↓
ここでは、どんな大きな数でも扱うことができるだけでなく、有理数体上の様々な定理が形式手法(定理証明)によって保証されているのだ。
つまりどんな入力に対しても、計算間違いが存在しないということだ。
(ただ、演算は+,-,*,/ だけしかまだ実装していない)
もちろん、入力を受け付けたり、結果を出力したりする部分はOCamlで実装していて、また、通信や表示などはブラウザなど別のプログラムが行っている。サーバーおよびクライアントのハードウェアにも依存しており、それらの部分で誤りがある可能性はゼロではない。しかし、コアの部分の計算ロジックを定理証明の力を借りることにより、システム(サービス)の信頼性を飛躍的にあげることができるのだ。
2009-01-26 追記: Mac OS X の Safari
ブラウザで表示が変になる現象を修正しました。
ソースコードは以下
