[Datetime-SIG] PEP 495: What's left to resolve
Alexander Belopolsky
alexander.belopolsky at gmail.com
Tue Sep 8 21:45:16 CEST 2015
On Tue, Sep 8, 2015 at 1:06 PM, Tim Peters <tim.peters at gmail.com> 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. :-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/datetime-sig/attachments/20150908/189a4370/attachment.html>
More information about the Datetime-SIG
mailing list