# 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)).
```

Lectures / Modules / Homeworks / Syllabus