Chapter 7 Preview

Instead of a section-oriented preview, I'll give an object-oriented preview. The chapter covers three kinds of games, relates them, and proves things about them. The following shows the relationship and what is proved about whom (and where). Because of the relationship, all results are good for all three kinds of games. 
S = section
L = lemma
T = theorem
C = corollary

Parity Game: - NP and co-NP: S7.4 opening
|            - strategy improvement algorithm (gradient descent): S7.6
|            - [Jurdzinski's algorithm (fixpoint over "measure"): S7.5]
|
|<-- S7.3 L7.5
|
Mean Payoff Game: - "simple algorithm" (fixpoint over payoff): S7.3 T7.6
|
|<-- S7.4 L7.10
|
Discounted Payoff Game: - UP and co-UP: the bulk of S7.4, concluding at C7.14
                          (fixpoint over a decaying sequence)
We will flexibly elaborate on some topics and skip others as the class sways its collective mood.

Math Background

maximum (infinity) norm

A vector x has maximum norm 
  ||x||oo = MAX i:indexes. abs xi
The name "maximum" is self-explanatory. There is a technical reason it is also called "infinity".

It is called a norm because it satisfies some very general axioms (all things satisfying these axioms are called norms): 

  ||x||oo >= 0
  ||x||oo = 0  ==>  x is the zero vector
  ||r*x||oo = abs r * ||x||oo  for real number r
  ||x+y||oo <= ||x||oo + ||y||oo

What good is a norm? It allows you to define a sort of "distance" between two vectors x and y by 

  ||x - y||oo
and this "distance" will have most of the desired properties (non-negative, triangle inequality, etc.) because of the norm axioms.

Now what good is a "distance"? It is needed for the argument at the top of page 116. The existence of the limit and its being the unique fixed point comes from the Banach fixed point theorem, which requires a "distance".

lim inf, lim sup

In mean payoff games the notions of limit infinum/supremum are used. Here are three characterizations; I give all of them because you are bound to understand one:

Let 'a' be a sequence of numbers (e.g., a:nat -> real). 

  1. forall e>0. ("FG" a > liminf a - e) /\ ("GF" a < liminf a + e)
forall e>0. ("FG" a < limsup a + e) /\ ("GF" a > limsup a - e)

  2. liminf a = Meet s:(subsequences of a, convergent). lim s
limsup a = Join s:(subsequences of a, convergent). lim s

  3. liminf a = Join n:nat. Meet k>=n. ak
limsup a = Meet n:nat. Join k>=n. ak
Example. an = (1 + e^(-n/35)) * sin n
(the magic number 35 is there just to make the graph look nice) 
    limsup a
  = Meet n:nat. Join k>=n. (1 + e^(-k/35)) * sin k

      roughly (not rigorous): sine can be as high as 1;
      1 + e^(-k/35), for k>=n, is highest when k=n

  = Meet n:nat. 1 + e^-(n/35)      (lowest when n -> oo)
  = 1
You will see that although the "upper frontier" oscillates quite a bit, it slowly tends to 1, the limsup. Similarly the liminf is -1.

For mean payoff game, form 2 is the most useful because we can use it to rewrite the winning condition to something extremely familiar: (here 'an' stands for the _a_verage after n steps) 

    liminf a >= nu                         (#2)
  = (Join n:nat. Meet k>=n. ak)            (numbers are totally ordered)
  = exists n:nat. (Meet k>=n. ak) >= nu    (lattice theory)
  = exists n:nat. forall k>=n. ak >= nu    (temporalize)
  = FG a>=nu
"Eventually always maintain your GPA above nu"