|
| 1 | +/- |
| 2 | +Copyright (c) 2026 TorchLean |
| 3 | +Released under MIT license as described in the file LICENSE. |
| 4 | +Authors: TorchLean Team |
| 5 | +-/ |
| 6 | + |
| 7 | +module |
| 8 | + |
| 9 | +public import NN.Spec.Core.Tensor.Factorizations |
| 10 | + |
| 11 | +/-! |
| 12 | +# Factorization examples — shared helpers |
| 13 | +
|
| 14 | +Small `Float`-valued helpers used by the matrix-factorization examples (`Cholesky`, `QR`). These |
| 15 | +examples are *executable sanity checks*: each one reconstructs the original matrix from its factors and |
| 16 | +asserts (via `#eval`) that the maximum entrywise reconstruction error is below a tolerance, so the build |
| 17 | +fails if a factorization is wrong. |
| 18 | +
|
| 19 | +These run over `Float` (the executable 64-bit runtime scalar), which is the precision the |
| 20 | +factorizations target for Gaussian-process / kernel-method use. |
| 21 | +-/ |
| 22 | + |
| 23 | +@[expose] public section |
| 24 | + |
| 25 | + |
| 26 | +namespace NN.Examples.Factorization |
| 27 | + |
| 28 | +/-- Build an `m × n` `Float` matrix tensor from a row-major nested list. Missing entries are `0`. -/ |
| 29 | +def mkMat {m n : Nat} (rows : List (List Float)) : Spec.Tensor Float (.dim m (.dim n .scalar)) := |
| 30 | + Spec.ofMatFn (fun i j => (rows.getD i.val []).getD j.val 0.0) |
| 31 | + |
| 32 | +/-- Maximum entrywise absolute difference between two `m × n` matrices. -/ |
| 33 | +def maxMatErr {m n : Nat} (A B : Spec.Tensor Float (.dim m (.dim n .scalar))) : Float := |
| 34 | + (List.finRange m).foldl (fun acc i => |
| 35 | + (List.finRange n).foldl |
| 36 | + (fun a j => max a (Float.abs (Spec.get2 A i j - Spec.get2 B i j))) acc) 0.0 |
| 37 | + |
| 38 | +/-- Matrix product `A · B` (thin wrapper over `matMulSpec`). -/ |
| 39 | +def mm {m n p : Nat} (A : Spec.Tensor Float (.dim m (.dim n .scalar))) |
| 40 | + (B : Spec.Tensor Float (.dim n (.dim p .scalar))) : Spec.Tensor Float (.dim m (.dim p .scalar)) := |
| 41 | + Spec.matMulSpec A B |
| 42 | + |
| 43 | +/-- Matrix transpose. -/ |
| 44 | +def tr {m n : Nat} (A : Spec.Tensor Float (.dim m (.dim n .scalar))) : |
| 45 | + Spec.Tensor Float (.dim n (.dim m .scalar)) := |
| 46 | + Spec.Tensor.matrixTransposeSpec A |
| 47 | + |
| 48 | +/-- Read a vector tensor back out as a `List Float` (for display). -/ |
| 49 | +def vecToList {n : Nat} (v : Spec.Tensor Float (.dim n .scalar)) : List Float := |
| 50 | + (List.finRange n).map (fun i => Spec.Tensor.toScalar (Spec.get v i)) |
| 51 | + |
| 52 | +/-- Squared Frobenius distance `Σ_{i,j} (A_ij - B_ij)²` between two `m × n` matrices. -/ |
| 53 | +def frobSqErr {m n : Nat} (A B : Spec.Tensor Float (.dim m (.dim n .scalar))) : Float := |
| 54 | + (List.finRange m).foldl (fun acc i => |
| 55 | + (List.finRange n).foldl |
| 56 | + (fun a j => let d := Spec.get2 A i j - Spec.get2 B i j; a + d * d) acc) 0.0 |
| 57 | + |
| 58 | +/-- Shared tolerance for reconstruction-error assertions. -/ |
| 59 | +def tol : Float := 1e-6 |
| 60 | + |
| 61 | +/-- |
| 62 | +Compiled **positive** assertion: print `name: OK (err)` when `err < tol`, otherwise raise an |
| 63 | +`IO` error so the build/`#eval` fails. Running this through `#eval` evaluates with the compiler |
| 64 | +(fast), unlike `#guard`, which forces slow kernel reduction of the whole factorization. |
| 65 | +-/ |
| 66 | +def assertLt (name : String) (err : Float) (tolerance : Float := tol) : IO Unit := |
| 67 | + if err < tolerance then |
| 68 | + IO.println s!"{name}: OK (err = {err})" |
| 69 | + else |
| 70 | + throw (IO.userError s!"{name}: FAIL (err = {err} ≥ tol = {tolerance})") |
| 71 | + |
| 72 | +/-- |
| 73 | +Compiled **negative-control** assertion: succeeds only when `err ≥ threshold`, i.e. when a property |
| 74 | +that *should not* hold is correctly detected as violated. Gives the metric teeth — a reviewer can see |
| 75 | +the same `maxMatErr`/residual that reports `0` on a valid factorization reports a large value on an |
| 76 | +invalid one, so the positive checks are not vacuous. |
| 77 | +-/ |
| 78 | +def assertGe (name : String) (err : Float) (threshold : Float := 0.5) : IO Unit := |
| 79 | + if err ≥ threshold then |
| 80 | + IO.println s!"{name}: OK (correctly rejected, err = {err} ≥ {threshold})" |
| 81 | + else |
| 82 | + throw (IO.userError s!"{name}: FAIL (err = {err} < {threshold}; expected the property to fail)") |
| 83 | + |
| 84 | +/-- |
| 85 | +Compiled **negative-control** assertion that a reconstruction *fails*: succeeds when the error is not |
| 86 | +below `tol` — including the `NaN` produced when a hypothesis is violated (e.g. Cholesky of a |
| 87 | +non-positive-definite matrix takes `√(negative)`). Documents that the success hypotheses (SPD pivots, |
| 88 | +full column rank) are genuinely necessary. |
| 89 | +-/ |
| 90 | +def assertReconFails (name : String) (err : Float) (tolerance : Float := tol) : IO Unit := |
| 91 | + if err < tolerance then |
| 92 | + throw (IO.userError s!"{name}: FAIL (unexpectedly reconstructed, err = {err} < {tolerance})") |
| 93 | + else |
| 94 | + IO.println s!"{name}: OK (correctly failed, err = {err})" |
| 95 | + |
| 96 | +end NN.Examples.Factorization |
0 commit comments