Coursework 3 (20%)

  1. We define binary numbers (Bin) as sequences of Booleans. Load ex3.epi into Epigram and complete the definitions of
    The binary representations of one and six.
    Translates binary numbers to (Peano) natural numbers.
    Translates natural numbers to binary.
    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 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.

Thorsten Altenkirch
Last modified: Wed Nov 3 21:39:02 GMT 2004