The Berlekamp–Welch decoder #
Let w : ι → F be a received word that differs from the values i ↦ p (α i) of a polynomial p
of degree less than k at no more than e of the distinct points α i. The Berlekamp–Welch
decoder [WB86], [GRS19] looks for a monic
error locator E of degree e and a polynomial Q of degree less than e + k with
Q (α i) = w i * E (α i) at every point: the key equations
(Cslib.Code.BerlekampWelch.IsSolution). They have a solution, with E vanishing at the errors
and Q = p * E (Cslib.Code.BerlekampWelch.exists_isSolution). Conversely, if 2 e + k ≤ n,
then for every solution Q - p * E has degree less than e + k and vanishes at the at least
n - e ≥ e + k points without errors, so Q = p * E and p is the quotient Q /ₘ E
(Cslib.Code.BerlekampWelch.IsSolution.divByMonic_eq).
The decoder Cslib.Code.berlekampWelch takes a solution (E, Q), and returns the quotient
Q /ₘ E after checking, as in [GRS19], that E divides Q and that the
values of the quotient are within distance e of w; it fails, returning none, when there is
no solution or a check fails. The checks make it sound for every received word: an output p
has degree less than k, its values are within distance e of w, and p * E solves the key
equations together with E (Cslib.Code.degree_lt_of_berlekampWelch_eq_some,
Cslib.Code.hammingDist_le_of_berlekampWelch_eq_some,
Cslib.Code.exists_isSolution_mul_of_berlekampWelch_eq_some). In particular, it fails on a
received word with no polynomial of degree less than k within distance e
(Cslib.Code.berlekampWelch_eq_none_of_forall_lt_hammingDist). With distinct points and
2 e + k ≤ n it is also complete: it returns p whenever the values of p are within distance
e of w (Cslib.Code.berlekampWelch_eq_some), so its outputs are exactly those polynomials
(Cslib.Code.berlekampWelch_eq_some_iff). Reed–Solomon codes of dimension k are therefore
uniquely decoded up to (n - k) / 2 errors, the largest number below half their minimum distance
n - k + 1, and the decoder reports failure beyond that radius when no codeword is close.
The key equations are a system of n linear equations in the 2 e + k unknown coefficients of
E and Q; in the literature they are solved by Gaussian elimination. This module proves the
correctness of the decoder only: Cslib.Code.berlekampWelch chooses a solution noncomputably,
and no running time is formalized.
Main definitions #
Cslib.Code.BerlekampWelch.IsSolution: solutions of the key equations.Cslib.Code.berlekampWelch: the Berlekamp–Welch decoder.
Main results #
Cslib.Code.BerlekampWelch.exists_isSolution: the key equations have a solution.Cslib.Code.BerlekampWelch.IsSolution.eq_mul,Cslib.Code.BerlekampWelch.IsSolution.divByMonic_eq: every solution yields the polynomial.Cslib.Code.degree_lt_of_berlekampWelch_eq_some,Cslib.Code.hammingDist_le_of_berlekampWelch_eq_some,Cslib.Code.exists_isSolution_mul_of_berlekampWelch_eq_some: soundness of the decoder.Cslib.Code.berlekampWelch_eq_none_of_forall_lt_hammingDist: the decoder fails when no polynomial is close.Cslib.Code.berlekampWelch_eq_some: the decoder corrects up toeerrors when2 e + k ≤ n.Cslib.Code.berlekampWelch_eq_some_iff,Cslib.Code.berlekampWelch_eq_none_iff: when2 e + k ≤ n, the decoder returns exactly the polynomials within distancee.Cslib.Code.berlekampWelch_eq_some_of_mem_reedSolomon: unique decoding of Reed–Solomon codes.
References #
- L. R. Welch, E. R. Berlekamp, Error correction for algebraic block codes
- [V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory] [GRS19]
(E, Q) solves the Berlekamp–Welch key equations for the received word w with evaluation
points α, e errors and dimension k: the error locator E is monic of degree e, Q has
degree less than e + k, and Q (α i) = w i * E (α i) at every point.
- monic : E.Monic
The error locator
Eis monic. The error locator
Ehas degree exactlye.The polynomial
Q, which stands forp * E, has degree less thane + k.The key equations:
Q (α i) = w i * E (α i)at every point.
Instances For
The quotient Q /ₘ E of a solution of the key equations has degree less than k.
If the received word w is within distance e of the values of a polynomial p of degree
less than k, the key equations have a solution: E is the product of X - α i over the
points i where w is wrong, times a power of X that brings its degree to e, and
Q = p * E.
Correctness of the key equations. With distinct points, if 2 e + k ≤ n and the received
word w is within distance e of the values of a polynomial p of degree less than k, every
solution (E, Q) of the key equations has Q = p * E.
With distinct points, if 2 e + k ≤ n and the received word is within distance e of the
values of a polynomial p of degree less than k, every solution (E, Q) of the key equations
gives p = Q /ₘ E.
The Berlekamp–Welch decoder for e errors and dimension k with evaluation points α:
for a solution (E, Q) of the key equations for the received word w, the quotient Q /ₘ E if
E divides Q and the values of the quotient are within distance e of w, and none when a
check fails or the key equations have no solution. The solution is chosen noncomputably; this
definition makes no claim about how it is found.
Instances For
Soundness of the Berlekamp–Welch decoder. Whatever the received word, an output p of the
decoder comes with an error locator E such that (E, p * E) solves the key equations.
Soundness of the Berlekamp–Welch decoder. Whatever the received word, an output of the
decoder has degree less than k.
Soundness of the Berlekamp–Welch decoder. Whatever the received word w, the values of an
output of the decoder are within distance e of w.
Failure detection. If the values of no polynomial of degree less than k are within
distance e of the received word w, the Berlekamp–Welch decoder returns none.
The Berlekamp–Welch decoder corrects e errors when 2 e + k ≤ n: with distinct points,
if the received word w is within distance e of the values of a polynomial p of degree less
than k, the decoder returns p.
The outputs of the Berlekamp–Welch decoder when 2 e + k ≤ n: with distinct points, the
decoder returns p exactly when p has degree less than k and its values are within distance
e of the received word.
Failures of the Berlekamp–Welch decoder when 2 e + k ≤ n: with distinct points, the
decoder returns none exactly when the values of no polynomial of degree less than k are within
distance e of the received word.
Unique decoding of Reed–Solomon codes. With distinct points, if 2 e + k ≤ n and the
received word w is within distance e of a codeword c of the Reed–Solomon code of dimension
k, the Berlekamp–Welch decoder returns a polynomial of degree less than k whose values are
c.