Relating the two semantics

• F^k is just iter F k, where iter is iterated function composition, defined by structural recursion on k.
• Usually fix-point iteration starts from ⊥. Here it is instead shown that you can start from an arbitrary function g.