dense-linalg-solvers

The dense-linalg-solvers worked example.

Run it from sema/:

sema check examples/dense-linalg-solvers
SEMA_STRICT=1 sema run examples/dense-linalg-solvers
sema assure examples/dense-linalg-solvers --grade silver

Source

src/main.sema

"""Bounded SVD-derived dense-real solvers with explicit numerical evidence.

`pinv` returns the Moore-Penrose pseudoinverse, `cond` returns the spectral
2-norm condition number, and `lstsq` returns
`(solution, residual_norm, numerical_rank, singular_values)`.
"""

import math

assure silver

equation rectangular_profile() -> any:
    matrix := [[2.0, 0.0, 0.0], [0.0, 4.0, 0.0]]
    return (pinv(matrix), pseudoinverse(matrix), cond(matrix), condition_number(matrix))

equation minimum_norm_fit() -> any:
    matrix := [[1.0], [1.0]]
    rhs := [1.0, 3.0]
    return (lstsq(matrix, rhs), least_squares(matrix, rhs))

equation singular_condition() -> any:
    return cond([[1.0, 0.0], [0.0, 0.0]])

test "rectangular pseudoinverse reverses the matrix shape":
    profile = rectangular_profile()
    inverse = profile[0]
    check shape(inverse) == [3, 2]
    check inverse[0][0] == 0.5
    check inverse[1][1] == 0.25
    check all(inverse == profile[1])
    check profile[2] == profile[3]
    check profile[2] == 2.0

test "least squares returns the minimum-norm solution and diagnostics":
    fits = minimum_norm_fit()
    fit = fits[0]
    check abs(fit[0][0] - 2.0) < 1e-12
    check abs(fit[1] * fit[1] - 2.0) < 1e-12
    check fit[2] == 1
    check abs(fit[3][0] * fit[3][0] - 2.0) < 1e-12
    check fit == fits[1]

test "rank deficiency has an explicit infinite condition number":
    check singular_condition() == math.inf

def main() -> dict !{}:
    profile = rectangular_profile()
    fit = minimum_norm_fit()[0]
    return {
        "pseudoinverse": profile[0],
        "condition_number": profile[2],
        "solution": fit[0],
        "residual_norm": fit[1],
        "rank": fit[2],
        "singular_values": fit[3],
        "singular_condition": singular_condition(),
    }

Reflected API

main

Bounded SVD-derived dense-real solvers with explicit numerical evidence.

pinv returns the Moore-Penrose pseudoinverse, cond returns the spectral 2-norm condition number, and lstsq returns (solution, residual_norm, numerical_rank, singular_values).

def main

def main() -> dict !{}

Returns dict

Effects !{}