Email Gateway (Jan 17 2025 at 12:16): Email Gateway (Jan 17 2025 at 12:16):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce this new contribution. Having looked at Burrows–Wheeler myself, I know how difficult this must have been. Also, David J Wheeler was a professor in my department; he was a computer pioneer who among many other things invented the classic "jump to subroutine” instruction.
Formalised Burrows-Wheeler Transform, by Louis Cheung and Christine Rizkallah
Abstract
The Burrows-Wheeler transform (BWT) is an invertible lossless transformation that permutes input sequences into alternate sequences of the same length that frequently contain long localized regions that involve clusters consisting of just a few distinct symbols, and sometimes also include long runs of same-symbol repetitions. Moreover, there is a one-to-one correspondence between the BWT and suffix arrays. As a consequence, the BWT is widely used in data compression and as an indexing data structure for pattern search. In this formalization, we present the formal verification of both the BWT and its inverse, building on a formalization of suffix arrays.
https://www.isa-afp.org/entries/BurrowsWheeler.html
Larry
Last updated: Jan 30 2025 at 04:21 UTC