[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