Copyright	(c) Wanja Chresta 2018
License	GPL-3
Maintainer	wanja dot hs at chrummibei dot ch
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Math.Algebra.Code.Linear

Contents

Code-Vectors and codewords
Decoding
Code transformers
Special codes and their generators
Helper functions
Reexported finite fields from Math.Algebra.Field

Description

Naive implementation of coding theory linear codes and error correcting codes over arbitrary fields, including finite fields. Goes well with the HaskellForMath library and its finite field implementations in Math.Algebra.Field. To use extension fields (fields of prime power, i.e. \( F_{p^k} \) with \(k>1\), use one of the exported finite fields in Math.Algebra.Field.Extension like F16 and its generator a16.

As theoretical basis, Introduction to Coding Theory by Yehuda Lindell is used. It can be found at http://u.cs.biu.ac.il/~lindell/89-662/coding_theory-lecture-notes.pdf

Usage

>>> :set -XDataKinds
>>> c <- randomIO :: IO (LinearCode 7 4 F5)
>>> c
[7,4]_5-Code
>>> generatorMatrix c
( 1 0 1 0 0 2 0 )
( 0 2 0 0 1 2 0 )
( 0 1 0 1 0 1 0 )
( 1 0 0 0 0 1 1 )
>>> e1 :: Vector 4 F5
( 1 0 0 0 )
>>> v = encode c e1
>>> v
( 1 0 1 0 0 2 0 )
>>> 2 ^* e4 :: Vector 7 F5
( 0 0 0 2 0 0 0 )
>>> vWithError = v + 2 ^* e4
>>> vWithError
( 1 0 1 2 0 2 0 )
>>> isCodeword c v
True
>>> isCodeword c vWithError
False
>>> decode c vWithError
Just ( 1 0 2 2 2 2 0 )

Notice, the returned vector is NOT the one without error. The reason for this is that a random code most likely does not have a distance >2 which would be needed to correct one error. Let's try with a hamming code

>>> c = hamming :: BinaryCode 7 4
>>> generatorMatrix c
( 1 1 0 1 0 0 0 )
( 1 0 1 0 1 0 0 )
( 0 1 1 0 0 1 0 )
( 1 1 1 0 0 0 1 )
>>> v = encode c e2
>>> vWithError = v + e3
>>> Just v' = decode c vWithError
>>> v' == v
True

Synopsis

data LinearCode (n :: Nat) (k :: Nat) (f :: *) = LinearCode {
- generatorMatrix :: Generator n k f
- checkMatrix :: CheckMatrix n k f
- distance :: Maybe Int
- syndromeTable :: SyndromeTable n k f
}
type Generator (n :: Nat) (k :: Nat) = Matrix k n
type CheckMatrix (n :: Nat) (k :: Nat) = Matrix (n - k) n
codeFromA :: forall k n f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => Matrix k (n - k) f -> LinearCode n k f
codeFromAD :: forall k n f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => Maybe Int -> Matrix k (n - k) f -> LinearCode n k f
standardForm :: forall n k f. (Eq f, Fractional f, KnownNat n, KnownNat k, k <= n) => Generator n k f -> Generator n k f
standardFormGenerator :: forall n k f. (Eq f, Fractional f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Generator n k f
type Vector = Matrix 1
encode :: forall n k f. Num f => LinearCode n k f -> Vector k f -> Vector n f
isCodeword :: forall n k f. (Eq f, Num f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Vector n f -> Bool
hasError :: forall n k f. (Eq f, Num f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Vector n f -> Bool
weight :: forall f m. (Eq f, Num f, Functor m, Foldable m) => m f -> Int
codewords :: forall n k f. (KnownNat n, KnownNat k, k <= n, Num f, Eq f, FinSet f) => LinearCode n k f -> [Vector n f]
allVectors :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => [Vector n f]
fullVectors :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => [Vector n f]
hammingWords :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => Int -> [Vector n f]
lighterWords :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => Int -> [Vector n f]
syndrome :: forall n k f. Num f => LinearCode n k f -> Vector n f -> Syndrome n k f
decode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Ord f, Num f) => LinearCode n k f -> Vector n f -> Maybe (Vector n f)
syndromeDecode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Ord f, Num f) => LinearCode n k f -> Vector n f -> Maybe (Vector n f)
calcSyndromeTable :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> SyndromeTable n k f
recalcSyndromeTable :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> LinearCode n k f
type SyndromeTable n k f = Map (Syndrome n k f) (Vector n f)
dualCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> LinearCode n (n - k) f
dualCodeD :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => Maybe Int -> LinearCode n k f -> LinearCode n (n - k) f
permuteCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> Matrix n n f -> LinearCode n k f
extendCode :: forall n k f r. (KnownNat n, KnownNat k, KnownNat r, k <= n, 1 <= r, k <= (n + r), Num f, Ord f, FinSet f) => LinearCode n k f -> LinearCode (n + r) k f
trivialCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f
simplex :: forall k p s. (KnownNat s, KnownNat k, IntegerAsType p, 1 <= (s ^ k), k <= (s ^ k), 1 <= ((s ^ k) - k), k <= ((s ^ k) - 1), Size (Fp p) ~ s) => LinearCode ((s ^ k) - 1) k (Fp p)
hamming :: (KnownNat m, 2 <= m, m <= (2 ^ m), m <= ((2 ^ m) - 1), 1 <= ((2 ^ m) - m)) => LinearCode ((2 ^ m) - 1) (((2 ^ m) - m) - 1) F2
golay :: LinearCode 23 12 F2
type BinaryCode n k = LinearCode n k F2
randomPermMatrix :: forall g n r. (KnownNat n, Num r, RandomGen g) => g -> (Matrix n n r, g)
codeLength :: forall n k f. KnownNat n => LinearCode n k f -> Int
rank :: forall n k f. KnownNat k => LinearCode n k f -> Int
eVec :: forall n f. (KnownNat n, Num f) => Int -> Vector n f
e1 :: forall n f. (KnownNat n, Num f) => Vector n f
e2 :: forall n f. (KnownNat n, Num f) => Vector n f
e3 :: forall n f. (KnownNat n, Num f) => Vector n f
e4 :: forall n f. (KnownNat n, Num f) => Vector n f
e5 :: forall n f. (KnownNat n, Num f) => Vector n f
e6 :: forall n f. (KnownNat n, Num f) => Vector n f
e7 :: forall n f. (KnownNat n, Num f) => Vector n f
e8 :: forall n f. (KnownNat n, Num f) => Vector n f
e9 :: forall n f. (KnownNat n, Num f) => Vector n f
e10 :: forall n f. (KnownNat n, Num f) => Vector n f
char :: forall c f. (KnownNat c, c ~ Characteristic f) => Proxy f -> Int
type F2 = Fp T2
type F3 = Fp T3
type F5 = Fp T5
type F7 = Fp T7
type F11 = Fp T11
type F4 = ExtensionField F2 ConwayF4
type F8 = ExtensionField F2 ConwayF8
type F16 = ExtensionField F2 ConwayF16
type F9 = ExtensionField F3 ConwayF9

Documentation

data LinearCode (n :: Nat) (k :: Nat) (f :: *) Source #

A \([n,k]\)-Linear code over the field f. The code parameters f,n and k are carried on the type level. A linear code is a subspace C of \(f^n\) generated by the generator matrix.

Constructors

LinearCode

Fields

generatorMatrix :: Generator n k f
Generator matrix, used for most of the operations
checkMatrix :: CheckMatrix n k f
Check matrix which can be automatically calculated from the standard form generator.
distance :: Maybe Int
The minimal distance of the code. This is the parameter \(d\) in \([n,k,d]_q\) notation of code parameters. The problem of finding the minimal distance is NP-Hard, thus might not be available.
syndromeTable :: SyndromeTable n k f
A map of all possible syndromes to their error vector. It is used to use syndrome decoding, a very slow decoding algorithm.

Instances

(KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => Bounded (LinearCode n k f) Source #
Instance details Defined in Math.Algebra.Code.Linear Methods minBound :: LinearCode n k f # maxBound :: LinearCode n k f #
(Eq f, Fractional f, KnownNat n, KnownNat k, k <= n) => Eq (LinearCode n k f) Source #
Instance details Defined in Math.Algebra.Code.Linear Methods (==) :: LinearCode n k f -> LinearCode n k f -> Bool # (/=) :: LinearCode n k f -> LinearCode n k f -> Bool #
(KnownNat n, KnownNat k, KnownNat (Characteristic f)) => Show (LinearCode n k f) Source #
Instance details Defined in Math.Algebra.Code.Linear Methods showsPrec :: Int -> LinearCode n k f -> ShowS # show :: LinearCode n k f -> String # showList :: [LinearCode n k f] -> ShowS #
(KnownNat n, KnownNat k, 1 <= k, (k + 1) <= n, k <= n, Eq f, FinSet f, Num f, Ord f, Random f) => Random (LinearCode n k f) Source #
Instance details Defined in Math.Algebra.Code.Linear Methods randomR :: RandomGen g => (LinearCode n k f, LinearCode n k f) -> g -> (LinearCode n k f, g) # random :: RandomGen g => g -> (LinearCode n k f, g) # randomRs :: RandomGen g => (LinearCode n k f, LinearCode n k f) -> g -> [LinearCode n k f] # randoms :: RandomGen g => g -> [LinearCode n k f] # randomRIO :: (LinearCode n k f, LinearCode n k f) -> IO (LinearCode n k f) # randomIO :: IO (LinearCode n k f) #

type Generator (n :: Nat) (k :: Nat) = Matrix k n Source #

A Generator is the generator matrix of a linear code, not necessarily in standard form.

type CheckMatrix (n :: Nat) (k :: Nat) = Matrix (n - k) n Source #

A CheckMatrix or parity matrix is the dual of a Generator. It can be used to check if a word is a valid code word for the code. Also, \[ \forall v \in f^k: cG \cdot H^\top = 0 \] i.e. the code is generated by the kernel of a check matrix.

codeFromA Source #

Arguments

:: (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f)
=> Matrix k (n - k) f	Elements of A where top-left is (1,1) and bottom right (k,n-k)
-> LinearCode n k f

Generate a linear \( [n,k]_q \)-Code over the field f with the generator in standard form (I|A), where the given function generates the \( k \times (n-k) \)-matrix A. The distance is unknown for this code and thus decoding algorithms may be very inefficient.

codeFromAD Source #

Arguments

:: (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f)
=> Maybe Int	Distance of the code. Give Nothing if it is unknown
-> Matrix k (n - k) f	Elements of A where top-left is (1,1) and bottom right (k,n-k)
-> LinearCode n k f

Generate a linear \( [n,k,d]_q \)-Code over the field f with the generator in standard form (I|A), where the given function generates the \( k \times (n-k) \)-matrix A.

standardForm :: forall n k f. (Eq f, Fractional f, KnownNat n, KnownNat k, k <= n) => Generator n k f -> Generator n k f Source #

Uses Gaussian eleminiation via rref from Matrix to find the standard form of generators.

standardFormGenerator :: forall n k f. (Eq f, Fractional f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Generator n k f Source #

The standard from generator of a linear code. Uses standardForm to calculate a standard form generator.

Code-Vectors and codewords

type Vector = Matrix 1 Source #

For convenience, Vector is a one-row Matrix

encode :: forall n k f. Num f => LinearCode n k f -> Vector k f -> Vector n f Source #

Get the codeword generated by the given k-sized vector.

isCodeword :: forall n k f. (Eq f, Num f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Vector n f -> Bool Source #

Check if the given candidate code word is a valid code word for the given linear code. If not, the party check failed.

hasError :: forall n k f. (Eq f, Num f, KnownNat n, KnownNat k, k <= n) => LinearCode n k f -> Vector n f -> Bool Source #

Check if the given candidate code word has errors, i.e. if some element changed during transmission. This is equivalent with not isCodeword

weight :: forall f m. (Eq f, Num f, Functor m, Foldable m) => m f -> Int Source #

The hamming weight of a Vector is an Int between 0 and n

codewords :: forall n k f. (KnownNat n, KnownNat k, k <= n, Num f, Eq f, FinSet f) => LinearCode n k f -> [Vector n f] Source #

A list of all codewords

allVectors :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => [Vector n f] Source #

List all vectors of length n over field f

fullVectors :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => [Vector n f] Source #

List all vectors of length n with non-zero elements over field f

hammingWords :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => Int -> [Vector n f] Source #

List of all words with given hamming weight

lighterWords :: forall n f. (KnownNat n, FinSet f, Num f, Eq f) => Int -> [Vector n f] Source #

List of all words with (non-zero) hamming weight smaller than a given boundary

Decoding

syndrome :: forall n k f. Num f => LinearCode n k f -> Vector n f -> Syndrome n k f Source #

Give the syndrome of a word for the given code. This is 0 if the word is a valid code word.

decode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Ord f, Num f) => LinearCode n k f -> Vector n f -> Maybe (Vector n f) Source #

Synonym for syndromeDecoding, an inefficient decoding algorithm that works for all linear codes.

syndromeDecode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Ord f, Num f) => LinearCode n k f -> Vector n f -> Maybe (Vector n f) Source #

Uses the exponential-time syndrome decoding algorithm for general codes. c.f: https://en.wikipedia.org/wiki/Decoding_methods#Syndrome_decoding

calcSyndromeTable :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> SyndromeTable n k f Source #

Return a syndrome table for the given linear code. If the distance is not known (i.e. minDist c = Nothing) this is very inefficient.

recalcSyndromeTable :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> LinearCode n k f Source #

Replace the syndromeTable of a code with a newly calculated syndrome table for the (current) generator. Useful to get a syndrome table for transformed codes when the table cannot be transformed, too.

type SyndromeTable n k f = Map (Syndrome n k f) (Vector n f) Source #

A syndrome table is a map from syndromes to their minimal weight representative. Every vector v has a syndrome \( S(v) \). This table reverses the syndrome function S and chooses the vector with the smallest hamming weight from it's image. This is a lookup table for syndrome decoding.

Code transformers

dualCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> LinearCode n (n - k) f Source #

The dual code is the code generated by the check matrix

This drops already calculated syndromeTables.

dualCodeD Source #

Arguments

:: (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f)
=> Maybe Int	The distance of the new code (if known) or Nothing
-> LinearCode n k f
-> LinearCode n (n - k) f

The dual code is the code generated by the check matrix.

This drops already calculated syndromeTables.

permuteCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f -> Matrix n n f -> LinearCode n k f Source #

Permute the rows of a code with a permutation matrix. The given permutation matrix must be a valid permutation matrix; this is not checked. This effectively multiplies the generator and check matrix from the right. Te distance of the resulting code stays the same.

This drops already calculated syndromeTables.

extendCode :: forall n k f r. (KnownNat n, KnownNat k, KnownNat r, k <= n, 1 <= r, k <= (n + r), Num f, Ord f, FinSet f) => LinearCode n k f -> LinearCode (n + r) k f Source #

Extend the given code \( c \) by zero-columns. Vectors \( v_{ext} \in c_{ext} \) have the form \( v = (v_1, \dots , v_n, 0, \dots, 0) \) . The distance of the extended code stays the same. This drops a calculated syndromeTable and makes it necessary to recalculate it if it's accessed.

Special codes and their generators

trivialCode :: forall n k f. (KnownNat n, KnownNat k, k <= n, Eq f, FinSet f, Num f, Ord f) => LinearCode n k f Source #

The trivial code is the identity code where the parity bits are all zero.

simplex :: forall k p s. (KnownNat s, KnownNat k, IntegerAsType p, 1 <= (s ^ k), k <= (s ^ k), 1 <= ((s ^ k) - k), k <= ((s ^ k) - 1), Size (Fp p) ~ s) => LinearCode ((s ^ k) - 1) k (Fp p) Source #

A simplex code is a code generated by all possible codewords consisting of 0's and 1's except the zero vector.

hamming :: (KnownNat m, 2 <= m, m <= (2 ^ m), m <= ((2 ^ m) - 1), 1 <= ((2 ^ m) - m)) => LinearCode ((2 ^ m) - 1) (((2 ^ m) - m) - 1) F2 Source #

The Hamming(7,4)-code. It is a [7,4,3]_2 code

golay :: LinearCode 23 12 F2 Source #

The _Golay_-code is a perfect [24,12,7]-code. It is the only other non-trivial perfect code and the only perfect code that is able to correct 3 errors.

Syndrome decoding on this code takes a very, very long time.

type BinaryCode n k = LinearCode n k F2 Source #

A binary code is a linear code over the field GF(2)

Helper functions

randomPermMatrix :: forall g n r. (KnownNat n, Num r, RandomGen g) => g -> (Matrix n n r, g) Source #

A random permutation matrix

codeLength :: forall n k f. KnownNat n => LinearCode n k f -> Int Source #

Convenience function to extract the length n from the type level

rank :: forall n k f. KnownNat k => LinearCode n k f -> Int Source #

Convenience function to extract the rank k from the type level.

eVec :: forall n f. (KnownNat n, Num f) => Int -> Vector n f Source #

Standard base vector [0..0,1,0..0] for any field. Parameter must be >=1

e1 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

First base vector [1,0..0]

e2 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

Second base vector [0,1,0..0]

e3 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e4 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e5 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e6 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e7 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e8 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e9 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

e10 :: forall n f. (KnownNat n, Num f) => Vector n f Source #

char :: forall c f. (KnownNat c, c ~ Characteristic f) => Proxy f -> Int Source #

Characteristic of a field. It takes a finite field type in the proxy value and gives the characteristic. This is done using type families To support new finite field types, you need to add a type instance for the type family Characteristic.