CSE 360 Homework 5

1. The following is an ML program that computes the factorial function. It uses a locally defined function to do this computation.

     fun fact n =
      let fun aux(0,acc) = acc
            | aux(m,acc) = aux(m - 1,m * acc)
       in aux(n,1)
      end;
   

   Write a lambda Prolog program in the style of the one for reverse given in Figure 5.15 that implements the factorial relation using a locally defined auxiliary predicate.

2. The following is an ML program that computes the Fibonacci program. It uses a locally defined function to do this computation.

   local fun iter(this,prev:int,count,n) =
             if count = n
             then this
             else iter(this+prev,this,count+1,n);
      in fun fib 0 = 0
           | fib n = iter(1,0,1,n);
    end;
   

   Write a lambda Prolog program in the style of the one for reverse given in Figure 5.15 that implements the Fibonacci relation using such a locally defined auxiliary predicate.

3. Which of the following formulas are provable and which are not? Attempt to verify this by hand before asking lambda Prolog to verify your conclusions.

   pi x\(sigma y\( p x => p y)).                              
   sigma x\(pi y\( p x => p y)).                              
   pi x\(pi y\(q x y => pi z\(q x z))).                       
   pi x\(sigma y\(q x y => pi z\(q x z))).                    
   sigma x\(pi y\(q x y => pi z\(q x z))).                    
   pi x\(pi y\(q x y => sigma z\(q x z))).                    
   (pi x\(pi y\(p x => q x y))) => pi x\(p x => pi y\(q x y)).
   (pi x\(p x => pi y\(q x y))) => pi x\(pi y\(p x => q x y)).