無限大を含む算術（x_arith）

Int = Z = {..., -1, 0, 1, 2, 3, ...}、XInt = Int + {∞, -∞} とする。他に全体集合T（total, universal, あるいはterm）を考えて、すべての領域はTの部分集合だとする。圏論で定式化したいなら、Tを固定して、モノ射 X→T だけを考えたスラント圏（ほぼsubobjectsの圏）を考えればいいだろう（たぶん実際はもっと工夫が必要）。

X, YとかがTの部分領域だとして、射として部分関数 f:X⊃→Y を考える。D(f)⊆X をfの定義域、U(f)⊆X をfの未定義域とする。dom(f) = X = D(f)+U(f)（直和）となる。別に集合E, Fを準備して、Eを例外の値、Fをエラーの値とする。exceptionもerrorもEだから、faultのつもりでerrorの集合はFとした。EもFも単元集合としても本質は失わない。

f:X⊃→Y は、X→Y+E に持ち上げることができて、直和に関するモノイダルスタンピング・モナドになるだろう。このモナドのKleisli圏Kをとりあえず作ると、XやYはKの対象になる。射は、D(f)で値を計算し、U(f)では例外を起こすような関数。

次に、Kの射を T→T の部分関数とみなす。dom(f)⊆T で、K内で考えれば dom(f)でfは完全に定義されるが、dom(f)の外では定義されない。dom(f)の外ではFの値をとるとして、T→Tに拡張する。この定式化で算術的例外（エラーではない）とbadargランタイムエラーはだいたいモデル化できるだろう。だいたいだけどね。

ここからは、プログラミング上の問題：

まず、T上で定義された述語をいくつか定義した。T→B（Bは真偽値集合）。

• XInt上の述語も定義すべきかどうか悩む。これは実用上、使い勝手の問題だけど。
• ゼロ除算はbadarithのエラーとするか、自前の例外とするか悩む。標準算術じゃないから自前の例外。
• エラー（ランタイムエラー）は、すべてbadargとするのが良さそうだが、それをすると、ソースコードが煩雑になるから、なにかエラーが出ればそれでいいとする。意味的には badarithだが、他のエラーのこともあるのだ。このへんの匙加減はホーントに難しいな。ソースがあるのが前提なら、あまり神経質にならんでもいいが、ソースなしのときにも親切なエラー報告をするとなると辛いものがある。

現実的な妥協点としては、ソースがないときのことは考えなくてもいいんじゃないのかな。「ソース見て調べろ」と。