Coursework 3 (20%)
- 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?
- 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.
Thorsten Altenkirch
Last modified: Wed Nov 3 21:39:02 GMT 2004