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 special numbers:

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 1/0 and -1/0 as exact infinity. This also keeps the tradition that "x/y" (in which x and y are both integers) is a rational, and the syntax of an inexact constant contains a dot.

For the same reason, the syntax of "indeterminate" should be "0/0" (exact) and "nan.0" (inexact). The names +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. IMO, orthogonality is a character of Scheme and is always wanted. Another 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, if exactness is also considered) 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 case: (+ 0.0 -0.0) evals to +0.0

Other computation rules should be straight forward.

Cheers,
Chongkai Zhu