Notes on fixed-points, with a sample evaluation.  Note that I reversed the
polarity of the if expression by making the first clause n==0 rather than
just n.

  SYNTAX 
  e ::= ... fix e

  OPERATIONAL SEMANTICS
  fix (\x:t.e) -> {fix (\x:t.e)/x}e   (FIX)

  e -> e'
  ---------------                     (FIX-CONG)
  fix e -> fix e'

  TYPING
  G |- e : t -> t
  --------------- (T-FIX)  note that the t in the function must be the same
  G |- fix e : t

  SAMPLE EVALUATION

    let incn = fix
      (\f:int->int->int. \x:int. \n:int. 
        if n==0 x (f x+1 n-1)) in
    incn 5 1

    -> (FIX)

    let incn = 
      (\x:int. \n:int. 
        if n==0 x ((fix (\f:int->int->int. \x:int. \n:int. 
                       if n==0 x (f x+1 n-1))) x+1 n-1)) in
    incn 5 1
    
    -> (LET)

      (\x:int. \n:int. 
        if n==0 x ((fix (\f:int->int->int. \x:int. \n:int. 
                       if n==0 x (f x+1 n-1))) x+1 n-1)) 5 1

    -> (APP)

    (\n:int. 
        if n==0 5 ((fix (\f:int->int->int. \x:int. \n:int. 
                       if n==0 x (f x+1 n-1))) 5+1 n-1)) 1
    

    -> (APP)

        if 1==0 5 ((fix (\f:int->int->int. \x:int. \n:int. 
                       if n==0 x (f x+1 n-1))) 5+1 1-1)

    -> (IF-TRUE)

      (now we're at the same place we were above, but with different
       x and n)

        (fix (\f:int->int->int. \x:int. \n:int. 
              if n==0 x (f x+1 n-1))) 5+1 1-1

    -> (FIX)

        (\x:int. \n:int. 
           if n==0 x ((fix (\f:int->int->int. \x:int. \n:int. 
                          if n==0 x (f x+1 n-1))) x+1 n-1)) 5+1 1-1

    -> (ADD*2)

        (\x:int. \n:int. 
           if n==0 x ((fix (\f:int->int->int. \x:int. \n:int. 
                          if n==0 x (f x+1 n-1))) x+1 n-1)) 6 0

    -> (APP*2)

        if 0==0 6 ((fix (\f:int->int->int. \x:int. \n:int. 
                       if n==0 x (f x+1 n-1))) 6+1 0-1)
    
    -> (IF-FALSE)

        6