eyeprolog

Hamming(7,4) error correction

Which bit of this received packet was flipped, and what was sent?

A Hamming(7,4) code protects four data bits with three parity bits, so a single flipped bit can be located and repaired. EyeProlog computes the syndrome, corrects the codeword, and proves each step from the received bits.

Run it in the playground · Source

The question

Seven bits arrive: 1 0 1 1 1 1 0. One of them was flipped by noise. Which one, what was the original codeword, and what are the four data bits?

The received word

received_bit(packet1, 1, 1).
received_bit(packet1, 2, 0).
received_bit(packet1, 3, 1).
received_bit(packet1, 4, 1).
received_bit(packet1, 5, 1).
received_bit(packet1, 6, 1).
received_bit(packet1, 7, 0).

Positions 1, 2 and 4 hold parity bits; positions 3, 5, 6 and 7 hold data.

The syndrome

syndrome_bit1(Code, S1) :-
  received_bit(Code, 1, B1),
  received_bit(Code, 3, B3),
  received_bit(Code, 5, B5),
  received_bit(Code, 7, B7),
  parity4(B1, B3, B5, B7, S1).

syndrome(Code, Syndrome) :-
  syndrome_bit1(Code, S1),
  syndrome_bit2(Code, S2),
  syndrome_bit4(Code, S4),
  (Weighteds2 is S2 * 2),
  (Weighteds4 is S4 * 4),
  (Partial is S1 + Weighteds2),
  (Syndrome is Partial + Weighteds4).

Each parity check covers the positions whose binary index has a given bit set. Read as a binary number, the three failed checks spell out the position of the error.

Correction

corrected_bit(Code, Position, Corrected) :-
  syndrome(Code, Position),
  received_bit(Code, Position, Bit),
  flip(Bit, Corrected).

corrected_bit(Code, Position, Bit) :-
  syndrome(Code, Errorposition),
  (Position \= Errorposition),
  received_bit(Code, Position, Bit).

Flip the bit the syndrome points at; keep every other bit.

The answer

eyeprolog examples/hamming-code.pl

syndrome(packet1, 5).
errorBit(packet1, 5).
correctedCodeword(packet1, [1, 0, 1, 1, 0, 1, 0]).
decodedPayload(packet1, [1, 0, 1, 0]).
status(packet1, single_bit_corrected).
reason(packet1, "Hamming syndrome identifies the flipped bit position").

Checks 1 and 4 fail and check 2 passes, so the syndrome is 1 + 4 = 5. Bit 5 is flipped back, and the data bits are 1 0 1 0.

The reason

eyeprolog --proof examples/hamming-code.pl

step(corrected_bit(packet1, 5, 0),
     rule(15),
     ['Code' = packet1, 'Position' = 5, 'Corrected' = 0, 'Bit' = 1],
     [syndrome(packet1, 5), received_bit(packet1, 5, 1), flip(1, 0)]).

Bit 5 becomes 0 because the syndrome is 5, the received bit 5 is 1, and flipping 1 gives 0. The syndrome has its own step, built from the three parity checks over the received bits.

The check

condition('C1', resolution, ok, 28).
condition('C5', re_decision, ok, 18).
steps(46).
verified(28).
recomputed(18).
trusted(0).
claims(6).
verdict(checked).

28 steps replay against the program, and the checker recomputes all 18 parity and arithmetic steps itself. The correction is fully certified.

Try it

Make bit 5 correct (0) and flip bit 3 instead. The syndrome becomes 3, and the same codeword [1, 0, 1, 1, 0, 1, 0] is recovered.
Fix bit 5 and change nothing else. The syndrome is 0: the codeword and payload are still derived, but errorBit/2 and status/2 give no answer.
Flip two bits at once. What does the syndrome point at now, and why can Hamming(7,4) not correct two errors?

Learn more in The Art of EyeProlog, Chapter 14.

This site is open source. Improve this page.