2009-05-01 [長年日記]
λ. なぜ0で割ってはいけないのか? リンゴの分配から体の公理まで
こういうのいいよね。 ただ、「体の公理から0で割ってはいけないことを証明」という表現ちょっとは正確でないように思う。確かに、体の公理の「a≠0 ⇒ a×a-1=1」からガードを外すことは出来ないのだけど、この公理をそのままにしておいて 0-1 を適当に定義してしまうことには何の問題もないので。
参考
- Bergstra, J. A and Tucker, J. V. The rational numbers as an abstract data type