Re: Type theory vs floating-point arithmetic

> Now, what I said about the disjointness of values in IEEE 32-bit and
> 64-bit representations
> can be rephrased in terms of coercions by pointing out that necessarily
> a coercion form
> 32-bit to 64-bit adds information, namely 29 extra bits of
> precision.(*)  We observe this
> by finding the coercion to be incoherent: c (f (x, y)) is not always
> equal to f' (c x, c y).
> Of course, one *could* make things coherent -- by defining each 32-bit
> operation f in
> terms of its 64-bit counterpart f', coercion and truncation:
>      f (x, y) = trunc (f' (extend x, extend y))
> However, this is correct only if  it is guaranteed that
>       f' (extend x, extend y)  = extend (trunc (f' (extend x, extend y)))

Dear all,

Let me rephrase the coherence requirement in coercive subtyping first.

If A is a subtype of B via a coercion c (A <_c B), then for any operation f
on B and x of A, f(x) is well-typed and equals to f (c(x)). In order to have
a coherent understanding (or interpretation), we require coherence, that is,
if there are two coercions c and c' from A to B, then c=c' (intensionally).

For products (i.e. A x B), we also have a subtyping rule:

            A1 <_c B1     and     A2 <_e B2
             A1 x A2    <_d    B1 x B2

  where the coercion d such that d(a1, a2) = (c(a1), e(a2)).

The coherence of this rule (among others) has been proved by me and Zhaohui
Luo in 2000.

If there is a coercion (called "extend") from 32-bit to 64-bit, then a
coercion (eg. d)from 32-bit x 32-bit to 64-bit x 64-bit can be automatically
generated, such that d(x, y) = (extend x, extend y).

And for any operation f on 64-bit x 64-bit, and any x and y of 32-bit, f(x,
y) is well-typed and its interpretation is the same as f (extend x, extend