formal semantics of numeric constants

[willc@tekchips.crl]

Someone said they'd be interested in seeing a formal semantics for numeric
constants.  I'd like to see a semantics for numeric constants added to RnRS,
but I think a formal semantics is overkill.  Anyway, here's my first shot
at what a formal semantics might look like.  Let me know of any bugs you
find -- it hasn't been tested, or even proofread!

For those who, like me, don't really want to read this thing, the idea is
that constants are inexact if they contain any of the following:

  an explicit inexactness prefix
  an at-sign indicating polar representation
  a decimal point
  a sharp sign indicating a "don't care" digit, as in 123##

A constant may also be inexact if it contains a negative exponent;
this is implementation-dependent.  Otherwise the constant is exact.

  Issue:  3@0     (inexact by above rules)
  Issue:  1e5     (exact by above rules)
  Issue:  1e-5    (implementation-dependent by above rules)




A denotational semantics for numeric constants

There are two properties of a numeric constant in Scheme
that matter:  its value (a complex number) and its exactness.
These properties correspond to the valuation functions V and
E below.

V [ <prefix R> <complex R> ]  =  V [ <complex R> ]

V [ <real1 R> @ <real2 R> ]
  =  V [ <real1 R> ] * (cos V [ <real2 R> ] + i sin V [ <real2 R> ])

V [ <real1 R> + i <real2 R> ] = V [ <real1 R> ] + i V [ <real2 R> ]

V [ <real1 R> - i <real2 R> ] = V [ <real1 R> ] - i V [ <real2 R> ]

V [ <real1 R> + i ] = V [ <real1 R> ] + i

V [ <real1 R> - i ] = V [ <real1 R> ] - i

V [ + i <real2 R> ] = i V [ <real2 R> ]

V [ - i <real2 R> ] = - i V [ <real2 R> ]

V [ + i ]  =  i

V [ - i ]  =  - i

V [ <uinteger 10> <suffix> ]  =  V [ <uinteger 10> ] * 10 ^ X [ <suffix> ]

V [ . <digit>+ #* <suffix> ]  =  (W [ . <digit>+ ] / 10) * 10 ^ X [ <suffix> ]

V [ <digit>+ . <digit>* #* <suffix> ]  =  W [ <digit>+ . <digit>* ] * 10 ^ X [ <suffix> ]

V [ <digit>+ #* . #* <suffix> ]  =  W [ <digit>+ #* ] * 10 ^ X [ <suffix> ]

V [ <uinteger1 R> / <uinteger2 R> ]  =  V [ <uinteger1 R> ] / V [ <uinteger2 R> ]

V [ + <ureal R> ]  =  V [ <ureal R> ]

V [ - <ureal R> ]  =  - V [ <ureal R> ]

V [ <digit R>+ #* # ]  =  R * V [ <digit R>+ #* ]

V [ <digit R>* <digit R> ]  =  R * V [ <digit R>* ] + Y [ <digit R> ]

V [ ]  =  0


W [ <digit>+ #* # ]  =  10 * W [ <digit>+ #* ]

W [ <digit>* <digit> ]  =  10 * W [ <digit>* ] + Y [ <digit> ]

W [ ]  =  0

W [ <digit(s)1>* . <digit(s)2>* ]  =  W [ <digit(s)1>* ] + W [ . <digit(s)2>* ]

W [ . <digit> <digit>* ]  =  (Y [ <digit> ] + W [ . <digit>* ]) / 10

W [ . ]  =  0


X [ <exponent marker> + <digit>+ ]  =  W [ <digit>+ ]

X [ <exponent marker> - <digit>+ ]  =  - W [ <digit>+ ]

X [ <exponent marker> <digit>+ ]  =  W [ <digit>+ ]


Y [ 0 ]  =  0
Y [ 1 ]  =  1
Y [ 2 ]  =  2
Y [ 3 ]  =  3
Y [ 4 ]  =  4
Y [ 5 ]  =  5
Y [ 6 ]  =  6
Y [ 7 ]  =  7
Y [ 8 ]  =  8
Y [ 9 ]  =  9
Y [ a ]  =  10
Y [ b ]  =  11
Y [ c ]  =  12
Y [ d ]  =  13
Y [ e ]  =  14
Y [ f ]  =  15




E [ <radix R> #e <complex R> ]  =  exact

E [ <radix R> #i <complex R> ]  =  inexact

E [ #e <radix R> <complex R> ]  =  exact

E [ #i <radix R> <complex R> ]  =  inexact

E [ <radix R> <complex R> ]  =  E [ <complex R> ]

E [ <real1 R> @ <real2 R> ]  =  inexact (issue: exception for <real R>@0 ?)

E [ <real1 R> + i <real2 R> ]  =  E [ <real1 R> ] % E [ <real2 R> ]

E [ <real1 R> - i <real2 R> ]  =  E [ <real1 R> ] % E [ <real2 R> ]

E [ <real1 R> + i ]  =  E [ <real1 R> ]

E [ <real1 R> - i ]  =  E [ <real1 R> ]

E [ + i <real2 R> ]  =  E [ <real2 R> ]

E [ - i <real2 R> ]  =  E [ <real2 R> ]

E [ + i ]  =  exact

E [ - i ]  =  exact

E [ <uinteger 10> <exponent marker> + <digit>+ ]  =  exact

E [ <uinteger 10> <exponent marker> - <digit>+ ]  =  unspecified

E [ . <digit>+ #* <suffix> ]  =  inexact

E [ <digit>+ . <digit>* #* <suffix> ]  =  inexact

E [ <digit>+ #* . #* <suffix> ]  =  inexact

E [ <uinteger1 R> / <uinteger2 R> ]  =  exact

E [ + <ureal R> ]  =  E [ <ureal R> ]

E [ - <ureal R> ]  =  E [ <ureal R> ]

E [ <digit R>+ #* # ]  =  inexact

E [ <digit R>* <digit R> ]  =  exact


exact % exact      =  exact
exact % inexact    =  inexact
inexact % exact    =  inexact
inexact % inexact  =  inexact


Exactness is not specified for constants such as:

    1000e-2

Otherwise numbers are inexact if they contain

  an explicit inexactness prefix
  an at-sign indicating polar representation
  a decimal point
  a sharp sign indicating a "don't care" digit