packages feed

moonlight-linalg-0.1.0.0: src-laws/Moonlight/LinAlg/Effect/Harness/Decomposition.hs

module Moonlight.LinAlg.Effect.Harness.Decomposition
  ( qrReconstructsInputLaw,
    qrOrthonormalColumnsLaw,
    choleskyReconstructsSpdLaw,
    symmetricEigenReconstructsLaw,
    symmetricEigenOrthonormalLaw,
    symmetricEigenUncheckedPassesCertificationLaw,
    thinSvdReconstructsLaw,
    thinSvdOrthonormalFactorsLaw,
    thinSvdSingularValuesOrderedNonnegativeLaw,
  )
where

import Data.Bifunctor (first)
import Data.Vector.Storable qualified as S
import Moonlight.LinAlg
  ( choleskyDecomp,
    fromListMatrix,
    mult,
    qrDecompFullColumnRank,
    symmetricEigen,
    thinSvdFullColumnRank,
    toListMatrix,
    toListVector,
    transpose,
  )
import Moonlight.LinAlg.Effect.Harness.Core
  ( approxTolerance,
    assertApproxList,
    assertRightProperty,
    maxAbsDifference,
  )
import Moonlight.LinAlg.Internal.Eigen.Symmetric
  ( certifySymmetricEigenResult,
    symmetricEigenPairsDenseUnchecked,
  )
import Moonlight.LinAlg.Pure.Dense.Flat (mkDenseDoubleMatrixRowMajor)
import Test.Tasty.QuickCheck qualified as QC

newtype FullRankMatrix43 = FullRankMatrix43 [Double]
  deriving stock (Eq, Show)

newtype SpdMatrix3 = SpdMatrix3 [Double]
  deriving stock (Eq, Show)

newtype SymmetricMatrix3 = SymmetricMatrix3 [Double]
  deriving stock (Eq, Show)

newtype FullRankMatrix32 = FullRankMatrix32 [Double]
  deriving stock (Eq, Show)

instance QC.Arbitrary FullRankMatrix43 where
  arbitrary =
    FullRankMatrix43 <$> anchoredOrGenerated fullRankMatrix43Anchors generateFullRankMatrix43

instance QC.Arbitrary SpdMatrix3 where
  arbitrary =
    SpdMatrix3 <$> anchoredOrGenerated spdMatrix3Anchors generateSpdMatrix3

instance QC.Arbitrary SymmetricMatrix3 where
  arbitrary =
    SymmetricMatrix3 <$> anchoredOrGenerated symmetricMatrix3Anchors generateSymmetricMatrix3

instance QC.Arbitrary FullRankMatrix32 where
  arbitrary =
    FullRankMatrix32 <$> anchoredOrGenerated fullRankMatrix32Anchors generateFullRankMatrix32

anchoredOrGenerated :: [[Double]] -> QC.Gen [Double] -> QC.Gen [Double]
anchoredOrGenerated anchors generatedValues =
  QC.frequency
    [ (1, QC.elements anchors),
      (9, generatedValues)
    ]

generateFullRankMatrix43 :: QC.Gen [Double]
generateFullRankMatrix43 =
  fullRankMatrix43Entries
    <$> generatedTriple generatedNonZeroEntry
    <*> generatedTriple generatedEntry
    <*> generatedTriple generatedEntry

generateSpdMatrix3 :: QC.Gen [Double]
generateSpdMatrix3 =
  spdMatrix3Entries
    <$> generatedTriple (QC.choose (1.0, 3.0))
    <*> generatedTriple (QC.choose (-1.0, 1.0))

generateSymmetricMatrix3 :: QC.Gen [Double]
generateSymmetricMatrix3 =
  symmetricMatrix3Entries
    <$> generatedTriple generatedEntry
    <*> generatedTriple generatedEntry

generateFullRankMatrix32 :: QC.Gen [Double]
generateFullRankMatrix32 =
  fullRankMatrix32Entries
    <$> ((,) <$> generatedNonZeroEntry <*> generatedNonZeroEntry)
    <*> generatedTriple generatedEntry

generatedTriple :: QC.Gen value -> QC.Gen (value, value, value)
generatedTriple generatedValue =
  (,,) <$> generatedValue <*> generatedValue <*> generatedValue

fullRankMatrix43Entries :: (Double, Double, Double) -> (Double, Double, Double) -> (Double, Double, Double) -> [Double]
fullRankMatrix43Entries (d0, d1, d2) (l10, l20, l21) (r0, r1, r2) =
  [d0, 0.0, 0.0, l10, d1, 0.0, l20, l21, d2, r0, r1, r2]

spdMatrix3Entries :: (Double, Double, Double) -> (Double, Double, Double) -> [Double]
spdMatrix3Entries (d0, d1, d2) (l10, l20, l21) =
  symmetricMatrix3Entries
    (d0 * d0, l10 * l10 + d1 * d1, l20 * l20 + l21 * l21 + d2 * d2)
    (d0 * l10, d0 * l20, l10 * l20 + d1 * l21)

symmetricMatrix3Entries :: (Double, Double, Double) -> (Double, Double, Double) -> [Double]
symmetricMatrix3Entries (d0, d1, d2) (o01, o02, o12) =
  [d0, o01, o02, o01, d1, o12, o02, o12, d2]

fullRankMatrix32Entries :: (Double, Double) -> (Double, Double, Double) -> [Double]
fullRankMatrix32Entries (d0, d1) (l10, l20, l21) =
  [d0, 0.0, l10, d1, l20, l21]

generatedEntry :: QC.Gen Double
generatedEntry =
  QC.choose (-4.0, 4.0)

generatedNonZeroEntry :: QC.Gen Double
generatedNonZeroEntry =
  QC.elements [-4.0, -3.0, -2.0, -1.0, 1.0, 2.0, 3.0, 4.0]

fullRankMatrix43Anchors :: [[Double]]
fullRankMatrix43Anchors =
  [ [1.0, 0.0, 2.0, 0.0, 1.0, -1.0, 2.0, 1.0, 0.0, 1.0, -1.0, 1.0],
    [2.0, 1.0, 0.0, 1.0, 3.0, 1.0, 0.0, -1.0, 2.0, 1.0, 0.0, 1.0],
    [1.0, 2.0, 1.0, 2.0, 0.0, -1.0, 0.0, 1.0, 3.0, 1.0, -1.0, 0.0]
  ]

spdMatrix3Anchors :: [[Double]]
spdMatrix3Anchors =
  [ [6.0, 2.0, 1.0, 2.0, 5.0, 0.5, 1.0, 0.5, 4.0],
    [5.0, -1.0, 0.5, -1.0, 4.0, 1.0, 0.5, 1.0, 3.5],
    [9.0, 1.5, -0.5, 1.5, 7.0, 2.0, -0.5, 2.0, 6.0]
  ]

symmetricMatrix3Anchors :: [[Double]]
symmetricMatrix3Anchors =
  [ [4.0, 1.0, 2.0, 1.0, 3.0, 0.5, 2.0, 0.5, 5.0],
    [2.0, 0.0, 0.0, 0.0, 3.0, 0.0, 0.0, 0.0, 7.0],
    [1.0, 1.0e-6, 0.0, 1.0e-6, 1.0 + 1.0e-12, -1.0e-6, 0.0, -1.0e-6, 3.0]
  ]

fullRankMatrix32Anchors :: [[Double]]
fullRankMatrix32Anchors =
  [ [3.0, 0.0, 0.0, 2.0, 1.0, 1.0],
    [1.0, 2.0, 2.0, -1.0, 0.5, 3.0],
    [4.0, 1.0, 1.0, 3.0, -1.0, 2.0]
  ]

qrReconstructsInputLaw :: QC.Property
qrReconstructsInputLaw =
  QC.property qrReconstructsInputLawProperty

qrOrthonormalColumnsLaw :: QC.Property
qrOrthonormalColumnsLaw =
  QC.property qrOrthonormalColumnsLawProperty

choleskyReconstructsSpdLaw :: QC.Property
choleskyReconstructsSpdLaw =
  QC.property choleskyReconstructsSpdLawProperty

symmetricEigenReconstructsLaw :: QC.Property
symmetricEigenReconstructsLaw =
  QC.property symmetricEigenReconstructsLawProperty

symmetricEigenOrthonormalLaw :: QC.Property
symmetricEigenOrthonormalLaw =
  QC.property symmetricEigenOrthonormalLawProperty

symmetricEigenUncheckedPassesCertificationLaw :: QC.Property
symmetricEigenUncheckedPassesCertificationLaw =
  QC.property symmetricEigenUncheckedPassesCertificationLawProperty

thinSvdReconstructsLaw :: QC.Property
thinSvdReconstructsLaw =
  QC.property thinSvdReconstructsLawProperty

thinSvdOrthonormalFactorsLaw :: QC.Property
thinSvdOrthonormalFactorsLaw =
  QC.property thinSvdOrthonormalFactorsLawProperty

thinSvdSingularValuesOrderedNonnegativeLaw :: QC.Property
thinSvdSingularValuesOrderedNonnegativeLaw =
  QC.property thinSvdSingularValuesOrderedNonnegativeLawProperty

qrReconstructsInputLawProperty :: FullRankMatrix43 -> QC.Property
qrReconstructsInputLawProperty (FullRankMatrix43 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @4 @3 entries
    (qMatrix, rMatrix) <- qrDecompFullColumnRank matrixValue
    reconstructed <- mult qMatrix rMatrix
    pure (maxAbsDifference entries (toListMatrix reconstructed) <= approxTolerance)

qrOrthonormalColumnsLawProperty :: FullRankMatrix43 -> QC.Property
qrOrthonormalColumnsLawProperty (FullRankMatrix43 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @4 @3 entries
    (qMatrix, _) <- qrDecompFullColumnRank matrixValue
    transposedQ <- transpose qMatrix
    gramMatrix <- mult transposedQ qMatrix
    pure (assertApproxList identity3 (toListMatrix gramMatrix))

choleskyReconstructsSpdLawProperty :: SpdMatrix3 -> QC.Property
choleskyReconstructsSpdLawProperty (SpdMatrix3 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @3 entries
    lowerMatrix <- choleskyDecomp matrixValue
    transposedLower <- transpose lowerMatrix
    reconstructed <- mult lowerMatrix transposedLower
    pure (maxAbsDifference entries (toListMatrix reconstructed) <= approxTolerance)

symmetricEigenReconstructsLawProperty :: SymmetricMatrix3 -> QC.Property
symmetricEigenReconstructsLawProperty (SymmetricMatrix3 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @3 entries
    (eigenvalues, eigenvectors) <- symmetricEigen matrixValue
    diagonalMatrix <- fromListMatrix @3 @3 (diagonal3 (toListVector eigenvalues))
    weightedEigenvectors <- mult eigenvectors diagonalMatrix
    transposedEigenvectors <- transpose eigenvectors
    reconstructed <- mult weightedEigenvectors transposedEigenvectors
    pure (maxAbsDifference entries (toListMatrix reconstructed) <= approxTolerance)

symmetricEigenOrthonormalLawProperty :: SymmetricMatrix3 -> QC.Property
symmetricEigenOrthonormalLawProperty (SymmetricMatrix3 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @3 entries
    (_, eigenvectors) <- symmetricEigen matrixValue
    transposedEigenvectors <- transpose eigenvectors
    gramMatrix <- mult transposedEigenvectors eigenvectors
    pure (assertApproxList identity3 (toListMatrix gramMatrix))

symmetricEigenUncheckedPassesCertificationLawProperty :: SymmetricMatrix3 -> QC.Property
symmetricEigenUncheckedPassesCertificationLawProperty (SymmetricMatrix3 entries) =
  assertRightProperty $ do
    matrixValue <- first show (mkDenseDoubleMatrixRowMajor 3 3 (S.fromList entries))
    uncheckedResult <- first show (symmetricEigenPairsDenseUnchecked 3 matrixValue)
    _ <- first show (certifySymmetricEigenResult matrixValue uncheckedResult)
    pure True

thinSvdReconstructsLawProperty :: FullRankMatrix32 -> QC.Property
thinSvdReconstructsLawProperty (FullRankMatrix32 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @2 entries
    (uMatrix, sMatrix, vTMatrix) <- thinSvdFullColumnRank matrixValue
    usMatrix <- mult uMatrix sMatrix
    reconstructed <- mult usMatrix vTMatrix
    pure (maxAbsDifference entries (toListMatrix reconstructed) <= approxTolerance)

thinSvdOrthonormalFactorsLawProperty :: FullRankMatrix32 -> QC.Property
thinSvdOrthonormalFactorsLawProperty (FullRankMatrix32 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @2 entries
    (uMatrix, _, vTMatrix) <- thinSvdFullColumnRank matrixValue
    transposedU <- transpose uMatrix
    uGram <- mult transposedU uMatrix
    vMatrix <- transpose vTMatrix
    vGram <- mult vTMatrix vMatrix
    pure (assertApproxList identity2 (toListMatrix uGram) && assertApproxList identity2 (toListMatrix vGram))

thinSvdSingularValuesOrderedNonnegativeLawProperty :: FullRankMatrix32 -> QC.Property
thinSvdSingularValuesOrderedNonnegativeLawProperty (FullRankMatrix32 entries) =
  assertRightProperty $ do
    matrixValue <- fromListMatrix @3 @2 entries
    (_, sMatrix, _) <- thinSvdFullColumnRank matrixValue
    pure (orderedNonnegativeDiagonal2 (toListMatrix sMatrix))

identity2 :: [Double]
identity2 =
  [1.0, 0.0, 0.0, 1.0]

identity3 :: [Double]
identity3 =
  [1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0]

diagonal3 :: [Double] -> [Double]
diagonal3 values =
  case values of
    [d0, d1, d2] -> [d0, 0.0, 0.0, 0.0, d1, 0.0, 0.0, 0.0, d2]
    _ -> []

orderedNonnegativeDiagonal2 :: [Double] -> Bool
orderedNonnegativeDiagonal2 entries =
  case entries of
    [s0, z01, z10, s1] ->
      s0 >= 0.0 && s1 >= 0.0 && s0 >= s1 && assertApproxList [0.0, 0.0] [z01, z10]
    _ -> False