Date: Thu, 17 Oct 2013 23:30:39 -0500

On 17 October 2013 23:13, Gabriel Dos Reis <gdr_at_[hidden]> wrote:

> | I suppose the other implication that is on the mind of many people

> but

>

| not being discussed is

> |

> | p != q => intptr_t(p) != intptr_t(q)

> |

> |

> | I'm not concerned about that, as p -> intptr_t(p) -> p has to result in a

> | matching pointer. I don't see how that is workable if the implication

> above

> | fails.

>

> Hmm, remember I am very slow. Please explain this for me in further

> details; I -think- I guess what you are saying but I would rather

> make sure you spell out for me how this is working on today's machines

> for which we need to make operator< a total ordering, and how they match

> (or differ from existing implementations.)

>

Proof by contradiction:

1. Suppose p != q => intptr_t(p) == intptr_t(q)

The guarantee for a pointer p of type T* is, if intptr_t is provided:

p equals (T*)(intptr_t)(p);

let x = intptr_t(p)

x must also equal (intptr_t)(q) because (intptr_t)(p) == (intptr_t)(q)

It is impossible for (T*)(x) != (T*)(x).

With substitution, (T*)(intptr_t)(p) != (T*)(intptr_t)(q) is also

impossible.

Therefore,

p != q => intptr_t(p) != intptr_t(q)

must be true.

Q.E.D.

> | I suppose the other implication that is on the mind of many people

> but

>

| not being discussed is

> |

> | p != q => intptr_t(p) != intptr_t(q)

> |

> |

> | I'm not concerned about that, as p -> intptr_t(p) -> p has to result in a

> | matching pointer. I don't see how that is workable if the implication

> above

> | fails.

>

> Hmm, remember I am very slow. Please explain this for me in further

> details; I -think- I guess what you are saying but I would rather

> make sure you spell out for me how this is working on today's machines

> for which we need to make operator< a total ordering, and how they match

> (or differ from existing implementations.)

>

Proof by contradiction:

1. Suppose p != q => intptr_t(p) == intptr_t(q)

The guarantee for a pointer p of type T* is, if intptr_t is provided:

p equals (T*)(intptr_t)(p);

let x = intptr_t(p)

x must also equal (intptr_t)(q) because (intptr_t)(p) == (intptr_t)(q)

It is impossible for (T*)(x) != (T*)(x).

With substitution, (T*)(intptr_t)(p) != (T*)(intptr_t)(q) is also

impossible.

Therefore,

p != q => intptr_t(p) != intptr_t(q)

must be true.

Q.E.D.

-- Nevin ":-)" Liber <mailto:nevin_at_[hidden]> (847) 691-1404

Received on 2013-10-18 06:31:20