I have also considered infinities in Scheme and have some different ideas:

1. We need both exact (rational) infinity and inexact infinity, that is, four specail number:

1/0 -1/0 +inf.0 -inf.0

The first two are rational and thus exact.

Even if this SRFI won't specify exact infinity, it should not use the "syntax of numerical constants" 1/0 and -1/0 but +inf.0 and -inf.0 instead, so that a latter SRFI can use the two as exact infinity. Such a syntax also keep the tradition that "x/y" (in which x and y are both syntax of integers) is a rational, and the syntax of an inexact contains a dot.

For the same reason, the syntax of "indeterminate" should be "0/0" (exact) and "nan.0" (inexact). The name of +inf.0, -inf.0 and nan.0 were borrowed from PLT scheme.

There are two rationales for adding rational infinity: aesthetic and utilitarian. Aesthetically, the exact infinity and inexact infinity together keeps the distinction (between exact and inexact) orthogonal to the dimension of type. Another The rationale is utility. For example, interval arithmetic will need exact infinity.

2. Since we have both positive infinity and negative infinity, we are forced to have two (or four) zeroes: positive and negative. IMO, this model is more preferable than the "limit".

For example, in PLT Scheme:

Language: Textual (MzScheme, includes R5RS).
> (/ -0.0)
-inf.0
> (/ 0.0)
+inf.0
> (/ +0.0)
+inf.0
> (+ 0.0 -0.0)
0.0

The only compromise is the last one. ( 0.0 is the same as +0.0)

Other comutation rules should be straight forward.

Cheers,
Chongkai Zhu