Section SystemT.

(* Define the recursion combinator *)

Fixpoint rec (A:Set) 
                    (n:nat)(f:A)(g: nat -> A -> A) :=
  match n with 
     0    => f
   | S p => g p (rec A p f g)
   end. 

(* Example 2.5 *)

Definition pd  :=
 (fun x:nat => 
    rec nat x 0 (fun n:nat => (fun y:nat => n))).

Eval compute in (pd 0).

Eval compute in (pd 123).

Variable x:nat.

Eval compute in (pd (S x)).

(* Example 2.6 *)

Definition double :=
  (fun x:nat => rec nat x 0 
                     (fun n:nat => 
                     (fun y:nat => S (S y)))).

Eval compute in (double 0).

Eval compute in (double (S x)).

Eval compute in (double 67).

(* Example 2.4 *)

Definition comp (A B C:Set) :=
(fun f: B -> C => 
  (fun g: A -> B =>
    (fun x:A => f (g x)))).


(* Example 2.8 *)

Definition Iter (A:Set) :=
 (fun f : (A ->A) => (fun n: nat => 
   rec (A->A) n (fun x:A => x) 
                        (fun m:nat => 
                           (fun g: (A->A)=>
                             (comp A A A f g))))).

Variable A:Set.
Variable f:A->A.
Eval compute in  (Iter A f 5).