Chris Pollett>Old Classes>CS440, Fall 1997>Hw3

Homework #3 Due Friday, Oct.17

Problem 2 is due in class the other problems can be submitted by midnight. Read Paulson 171-192, 213-224, 242-246, 257-274.

1. Rewrite the structure Sequent from HW2 as a functor which takes a structure valseq with signature VALID =

sig
   val valid : sequent -> bool
end;

and returns a structure of the form

struct
  antecedent = what we had in HW2;
  succedent = what we had in HW2;
  valid x = valseq.valid x;
end;

Bonus.(5pts) Implement Wang's algorithm and pass it as a structure to the functor Sequent.

2. Consider

exception BadN;
fun comb(n,m) = if n<0 orelse m<0 orelse m>n then raise BadN |
	elseif m=0 orelse m=n then 1 | 
	elseif comb(n-1,m) + comb(n-1,m-1);

Prove by induction forall n,m >0 comb(n,m) = n!/((n-m)!m!).

3. Let

	datatype bin = O | I;

Define an abstract type stream = Stream of bin list which contains the value create of an empty stream and contains a function append which can append either an O or an I onto a stream and finally contains a function Slist which can output a stream as a list of 0's and 1's.

Prepared by Chris Pollett.