Coursework 3 (20%)

1. We define binary numbers (Bin) as sequences of Booleans. Load ex3.epi into Epigram and complete the definitions of

   bone,bsix

   The binary representations of one and six.

   bin2nat

   Translates binary numbers to (Peano) natural numbers.

   nat2bin

   Translates natural numbers to binary.

   nat2natProp

   shows that bin2nat is inverse to nat2bin

   I didn't ask to show that the inverse of nat2natProp holds, i.e. that bin2nat (nat2bin bs) = bs. Can you see why? How could one adapt the representation of Bin such that this holds?
2. Introduce a representation of binary words of fixed length, i.e. define a type Word together with translations from and to Bin as defined above. Define addition for words (wadd).

The deadline for completing this coursework is Tuesday 6/12, 13:00. Once completed email the completed Epigram files to txa@cs.nott.ac.uk. There will be a short viva on your solution during the Tuesday lab after you have submitted it. Marks will be only be given after the viva.