On Tue, Sep 8, 2015 at 1:06 PM, Tim Peters <[email protected]> wrote:
> But I can never decide whether something really "fixes the hash > problem" without a lot more thought. > Let me try to outline a formal proof. Definitions: An aware datetime value t is called "regular" if t.utcoffset() does not depend on the value of the fold attribute. All other values are called "special". A binary relation "==" is defined by the following rules: (a) two special values s1 and s2 satisfy the "==" relation if they are the same (all component are equal) or they differ only by the value of fold; (b) for any special value s and regular value r, both r == s and s == r are False; and (c) for two regular values r1 and r2, r1 == r2 is equivalent to r1 - r1.utcoffset() and r2 - r2.utcoffset() having the same components. (Recall that according to PEP 495, dt - delta always has fold=0.) It will also be useful to define a "naive" equivalence: t1 ~ t2 if t1.tzinfo is t2.tzinfo and all their components except fold (year through microseconds) are equal. We will assume that ~ being an equivalence relation is well known. Lemma: The "==" relation defined above is an equivalence relation. Proof: We need to prove reflexivity (t == t for any t), symmetry (t1 == t2 => t2 == t1) and transitivity (t1 == t2 and t2 == t3 implies t1 == t3). Note that because of rule (b) it is enough to prove that == is equivalence separately for regular and special values. The complete proof is a rather tedious analysis of six propositions: three properties for each regular/special case. I'll present the two least trivial ones. 1. Let's show that == is transitive on the regular datetimes. Indeed, let r1, r2 and r3 are regular datetimes and o1, o2, and o3 are their utcoffset() values. Then r1 == r2 and r2 == r3 implies that r1 - o1 ~ r2 - o2 and r2 - o2 ~ r3 - o3, which in turn implies that r1 - o1 ~ r3 - o3 by transitivity of ~, which in turn implies r1 == r3 by transitivity of ~. QED. 2. Let's show that == is transitive on the special datetimes. This case is even simpler because s1 == s2 implies s1 ~ s2 (s1 and s2 differ only by fold), s2 == s3 implies s2 ~ s3 and thus s1 ~ s3 by transitivity of ~ and s1 == s3 by rule (a). Lemma: A function that is constant on equivalence classes satisfies the hash invariant. Proof: This is a tautology. Proposition: newhash(t) = oldhash(t.replace(fold=0)) satisfies the hash invariant. Proof: If t is special, its equivalence class consists of itself and a value with the complement value of fold. Since we force fold=0 before computing the hash values, it is trivially the same for both values in the same class. If t is regular, since oldhash is defined as a hash of t - t.utcoffset() components, the hash values of r1 and r2 are equal if r1 - r1.utcoffset() ~ r2 - r2.utcoffset() which follows from r1 == r2 by rule (c). > > So far, so good :-) > Except for headache. :-)
_______________________________________________ Datetime-SIG mailing list [email protected] https://mail.python.org/mailman/listinfo/datetime-sig The PSF Code of Conduct applies to this mailing list: https://www.python.org/psf/codeofconduct/
