[Prev][Next][Index][Thread]
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
y).
Regards,
Yong