-- SOLUTIONS TO EXERCISES 7


SKP = Solution's book for the exercises in KP's book.

OBS: You have to be aware that KP's book defines zero as a PRF
function with one argument while we define it with 0 arguments.  
Use comp(zero) in order to get the PRF that computes KP's zero
function (that is a function with an argument that always returns 0).


-- 7.1

See SKP pages 4--6.


-- 7.2

proj_m^n = \x1 .. xm .. xn -> xm
compos_m^n = \g f1 .. fm x1 .. xn -> g (f1 x1 .. xn) .. (fm x1 .. xn)

rec_n :: (N^n -> N) -> (N^(n+2) -> N) -> N^n -> N -> N
rec_n = \g h x1 .. xn x -> if (x == Zero) then
                              g x1 .. xn
                            else
                              h x1 .. xn (pred x) (rec_n g h x1 .. xn (pred x))
  where pred :: N -> N
        pred Zero = Zero
        pred (Succ n) = n


-- 7.3

rec_2 :: (Int -> Int) -> (Int -> Int -> Int -> Int) -> Int -> Int -> Int
proj_1^1 :: Int -> Int
compos_1^3 :: (Int -> Int) -> (Int -> Int ->Int -> Int) -> 
             Int -> Int -> Int -> Int
proj_3^3 :: Int -> Int -> Int -> Int

add :: Int -> Int -> Int
add = rec_2 proj_1^1 (compos_1^3 succ proj_3^3)


-- 7.4

See SKP pages 6--7.


-- KP 2.18

pred Zero     = compos_1^0(Zero)
pred (Succ n) = n

=> g = Zero
   h = \y z -> y = proj_1^2
   pred = rec_2 g h


mult x Zero     = Zero
mult x (Succ n) = add x (mult x n)

=> g = compos_1^0(Zero)
   h = \y z q -> add y q = compos_2^3 add proj_1^3 proj_3^3
   mult = rec_2 g h


-- KP 2.19

According to the exercise :

f 0 = 0
f n = n + (n-1) = 2*n - 1

According to the solutions :

f 0 = 0
f n = n + f (n-1) = n + (n-1) + (n-2) + .. + 0


-- 7.5

See SKP pages 8--9.


-- 7.6

append(xs,ys) == ys ++ xs in Haskell

append(xs,nil) = xs
append(xs,cons(y,ys)) = cons(y,append(xs,ys))


-- 7.7

See SKP page 9.