A little graph theory (The Handshaking Lemma)

[Jeremy Weissmann]

Dear all (and João specifically!),

   I recently read João's calculational proof of the Handshaking Lemma.  (Explanation to come.)  Here is a link:

     http://www.joaoff.com/2009/04/07/calculational-proof-handshaking-lemma/     .

I was in bed, groggily reading over it, when I came across this monstrous formula:

     (==a :  a in V  /\  odd.(d.a)  :  even.(d.a) )  ==  (==a :  a in V  /\  even.(d.a)  :  even.(d.a) )     .

I thought to myself,  "There must be a better way!" .   So I picked up my fountain pen, and a few seconds and surprises later, I was done!

   Before we begin, let me stress that I am not afraid of  'monstrous'  formulas, per se.  Sometimes we need the courage to deal with something messy!  But we should remember that the entire philosophy of programming, mathematics, and thought that Dijkstra and others created can be summarized:  "How not to make a mess of it." .   (EWD1304)   The calculational style was invented as a tool to help us keep our intellectual activity clean, but simply using that tool does not suffice to do so.  We have to exercise care, even in such an elegant framework as the calculational style.  (The flip-side of this moral is:  If even calculational arguments can get hairy, imagine how easy it is for traditional arguments to get hairy!)

* * *

   So, what is the Handshaking Lemma?  Well, it is a theorem from graph theory.  I'll explain the basic concepts very quickly.

   A graph consists of  'nodes' ,  and  'edges' ,  which are bags containing two nodes, possibly the same node twice.   (In the lingo, we are allowing  'loops'  and  'multiedges' .)   We can visualize simple graphs easily by drawing dots for the nodes, and lines between nodes representing edges.  I will use  'n'  and  'e'  as dummies of type  node  and  edge ,  respectively, and I write  'n in e'  to represent the boolean expression  'node n is contained in edge e' .

   One more ingredient is the notion of  'degree' .   We say that the degree of a node  n  is the number of edges which contain it.  Mathematically speaking:

(0)     deg.n  =  (+e : n in e : 1)     .

We say that a node has even (odd) degree if its degree is even (odd).

   We are now ready to state the Handshaking Lemma:  "A graph contains an even number of nodes of odd degree." .   One way to represent this theorem mathematically is:

(*)     even.(+n : odd.(deg.n) : 1)     ,

and João's exposition gives a proof using this formulation.

* * *

   I wish to take a different approach, because I see the theorem statement itself as being rather entangled.  João speaks at the end of his note about pulling rabbits out of hats, but the biggest rabbit here is the problem statement itself.  Who would ever think that a graph contains an even number of nodes of odd degree?!

   The answer is:  Someone who considered the sum of all the degrees in a graph.  Read on, and you'll see why.

   Now, from  (0)  we see that a degree is a sum.  And a great thing to do with sums is to sum them, because  +  is very compatible with  + !   So let's add up all the degrees in a graph, and calculationally explore:

     the sum of all the degrees

 =     { translation }

     (+n :: deg.n )

 =     {  (0)  }

     (+n :: (+e : n in e : 1))

 =     { quantifier trading }

     (+e :: (+n : n in e : 1))

 =     { by definition, there are two nodes in an edge }

     (+e :: 2 )

 =     { translation }

     2 * (the number of edges)     .

Thus we have proved:

(1)     the sum of all the degrees in a graph equals 2 times the number of edges     .

(The above calculation is the simplest proof of this fact I've ever seen.  All these years later, the simplicity and power of the calculational style can still thrill me.)   In particular, the sum of the degrees is even.

* * *

   Now the Handshaking Lemma follows almost immediately — because it has nothing to do with graph theory, just with properties of arithmetic.  With  x  ranging over any collection of integers:

     (+x :: x)

 =     { quantifier split }

     (+x : even.x : x)  +  (+x : odd.x : x)

 ≈     { recall that  ≈  stands for equality mod 2 }

     (+x : even.x : 0)  +  (+x : odd.x : 1)

 =     { arithmetic }

     (+x : odd.x : 1)     ,

that is:

(2)     (+x :: x)  ≈  (+x : odd.x : 1)     .

   Thus the Handshaking Lemma follows immediately from our two little theorems:

     (+n : odd.(deg.n) : 1)

 ≈     {  (2)  }

     (+n :: deg.n )

 ≈     {  (1)  }

     0     .

* * *

   In retrospect, we can see now why  (*)  was an unfortunate interface:   It was a crisp rendering of our theorem in a mathematical language with powerful, flexible operators... but it was not sufficiently disentangled.  This small example once again teaches me that the principles of careful thought, like disentanglement, are far more fundamental than our mathematical language.

   My two theorems each require only three small calculational steps, and every step seems to me either motivated, or a sweetly reasonable exploration.   (Actually, both of my theorems are just explorations.)   Compare this with the following hint (!) from João's proof:

The most reasonable thing to do is simplify the range;

this step prepares that simplification, because

(==a :  a in V  /\  odd.(d.a)  :  true)  is  true

and  ==  is reflexive.  Also,  even.1 == false .

* * *

   Note too that my proof makes almost no use of the predicates  'even'  and  'odd' ,  preferring to use the concepts of modular arithmetic instead.  Much of the bulk in João's proof is due to  'even'  and  'odd' .

   The predicate  'even'  is problematic.  It has nice enough properties, like:

     even.(x+y)  ==  even.x  ==  even.y     .

But evenness is a numerical concept, and  ==  is not as flexible an operator as are  + , * , ≈ ,  etc.   (Dan Grundy taught me to never overlook the great calculational power and flexibility of modular arithmetic.  I hope I have made him proud!)

+j