A compression algorithm attempts to reduce the size of a file of data
by taking advantage of redundancy.
Typically there are two function compress and decompress
which act on a list of values - often bytes or characters.
The desirable properties of a compression algorithm include:
of the compress function should be smaller than the input for wide range
of input data. We will not be checking this - it is probably best done
The original data should be recovered exactly by the function decompress.
for all inputs l
We consider a number of popular algorithms, we present an implementation
in ML and a proof that the algorithm is correct, i.e. that
decompress is the inverse of compress.