Formalised Burrows-Wheeler Transform (Q7361861)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry BurrowsWheeler
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalised Burrows-Wheeler Transform |
AFP entry BurrowsWheeler |
Statements
17 January 2025
0 references
Louis Cheung
0 references
Christine Rizkallah
0 references
Formalised Burrows-Wheeler Transform (English)
0 references
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.
0 references
