Equations, Symbolic Algebra & Tensors

Bridging code and AI means mathematics is a language concern, not a library afterthought. Sema gives you three interlocking pieces: equation blocks that let you transcribe mathematical notation as syntax, an opt-in symbolic algebra layer, and a first-class native tensor type with stdlib math bindings.

equation blocks — notation is the syntax

One construct, not two hundred keywords: equation opens a block in which mathematical notation is the syntax, and the compiler lowers it to typed, pure, natively-executed code. The goal is transcription, not translation — an equation from a paper enters a Sema program shape-intact (quantifiers, big operators, gradients, s.t. constraints and all), with the efficient implementation (autodiff, numeric kernels, dense linear algebra) chosen under the hood.

equation ridge_loss(w: Vec[f64], X: Matrix[f64], y: Vec[f64], lam: f64) -> f64:
    n := rows(X)
    L(w) := (1/n) * Σ_{i ∈ 0..n} (⟨X[i], w⟩ - y[i])^2 + lam * ‖w‖_2^2
    return L(w)

equation fit(X: Matrix[f64], y: Vec[f64], lam: f64) -> Vec[f64]:
    return argmin_{w ∈ Reals(cols(X))} ridge_loss(w, X, y, lam)

def step(w: Vec[f64], lr: f64) -> Vec[f64] !{}:
    equation:
        g := ∇ridge_loss(w, data.X, data.y, 0.01)     # bindings flow outward
    return w - lr * g

equation all_feasible(plan: list[Route], cap: f64) -> bool:
    return ∀ r ∈ plan : load(r) ≤ cap ∧ ∃ d ∈ r.drivers : certified(d)

Two forms: the declaration form (equation name(...) -> T:) is a def sibling, and the inline form (equation: inside a def) is a statement suite whose := bindings flow into the enclosing scope.

Unicode and ASCII spellings are both canonical — a formatter may normalize between them, never reject. (Source formatting is planned; there is no sema fmt subcommand yet.)

The notation, by family

• Quantifiers: ∀ x ∈ D : P(x), ∃ x ∈ D : P(x), ∃! x ∈ D : P(x) (ASCII forall/exists/exists!). Domains must be finite/iterable (sets, lists, integer ranges a..b); an unbounded domain is a compile error, never a silent loop.
• Big operators: Σ_{i ∈ D} e, Π_{i ∈ D} e, ⋃/⋂, ∫_{a}^{b} f(x) dx (adaptive numeric); ASCII sum/prod/integral.
• Calculus: ∇f (forward-mode autodiff, exact to machine precision — never symbolic-guessed), ∂f/∂x, d/dx f(x), jacobian(f), hessian(f) (∇²), Δ Laplacian. A non-differentiable call site is a typed error, not a NaN.
• Optimization: min/max/argmin/argmax/sup/inf with binder subscripts and constraint tails — argmin_{x ∈ [0,1]} f(x) s.t. g(x) ≤ 0, h(x) = 0 (also subject to). Discrete domains solve exhaustively; continuous domains use bracketed 1-D search / projected gradient descent, with the method recorded in the result’s provenance.
• Sets and logic: ∈ ∉ ⊆ ⊂ ∪ ∩ \, set builder { x ∈ D : P(x) }, ¬ ∧ ∨ ⊕ ⇒ ⇔, ≤ ≥ ≠.
• Linear algebra: ⟨x, y⟩ inner product, ‖x‖/‖x‖_p norms, |x| absolute value, postfix ^T transpose, ⊙ Hadamard, ⊗ Kronecker/tensor, det/tr/rank/ker/im/dim, proj, f ∘ g composition, postfix ! factorial, C(n, k) binomial.
• Probability and information: E[X], Var/Cov/Corr, H(p), D_KL(p ‖ q), cross-entropy, over concrete samples/distribution vectors.
• Dynamics: Fix(f, x0) fixed-point iteration; f * g discrete convolution; lim numeric (Richardson) with a divergence error.
• Definitions: name := expr and name(params) := expr bind local values and functions; := is definitional.

Equation bodies are pure

Equation bodies derive the effect row !{}: calls resolve only to pure functions and other equations, and model.*/fs.*/generative calls inside are compile errors. Mathematics is the deterministic column of Sema’s guarantee map, and this purity is exactly what lets the compiler fuse, parallelize, and differentiate freely. Inside the block ^ is exponentiation; outside, nothing changes (there ^ stays bitwise xor — see Operators). Types flow in from the signature; shape mismatches are compile-time where shapes are static, and typed ShapeError at boundaries otherwise.

Approximations are typed as approximations

Every solver result carries provenance (method, iterations, tolerance) in the journal. Because argmin over a non-convex objective is an approximation, results from iterative solvers are typed distinctly as Approx[T] (with .value / .residual / .converged) unless the domain is discrete-exhaustive. Sema does not launder an approximation as an exact answer.

Operators from the atlas that parse but have no v0 kernel fail at compile time with a typed math.NotImplemented diagnostic naming the atlas section — notation-complete, honestly partial.

Symbolic algebra

§ equations evaluate numerically; the symbolic layer adds the ability to manipulate expressions and return results in symbolic form — the CAS side of the vision, now real. Inside an equation, a string literal is a symbol, and arithmetic on a symbol builds a symbolic expression:

equation derivative() -> str:
    return diff("x"^2 + 3*"x", "x")            # -> "2*x + 3"

equation factored() -> str:
    return factor("x"^2 - 5*"x" + 6, "x")      # -> "(x - 2)*(x - 3)"

equation solutions() -> list[str]:
    return solve("x"^2 - 5*"x" + 6, "x")       # -> ["3", "2"]

Verbs: sym(name) (make a symbol), simplify, expand, diff (symbolic differentiation with product/chain/power rules and sin/cos/exp/ln/sqrt/ tan), factor and solve (linear + quadratic), subst. Symbolic values propagate automatically — the moment an operand is symbolic, +, -, *, /, ^, and unary - build a symbolic tree instead of a number. simplify canonicalizes and renders in descending polynomial degree; a symbolic value crosses back to the runtime as its rendered string.

Honesty bound

Solving is exact for linear and quadratic polynomials and returns a typed error otherwise — no silent wrong-branch simplification. Bounded conditional cancel and integrate (polynomials and perfect rational powers), exact rational-function limit, and Taylor series through order 12 return the result plus the real-domain conditions it depends on. General assumptions, transcendental/multivariate integration, and higher-degree factorization are the remaining CAS surface, not yet available.

Native tensors

Tensor is a first-class dense array with a shape ([] scalar, [n] vector, [r, c] matrix, higher-rank general) and an explicit dtype — f64, bool, or complex. The CPU backend is native; an accelerated backend (candle/wgpu — GPU when present) swaps in behind the same operations, so programs never change:

a = tensor([[1.0, 2.0], [3.0, 4.0]])
b = a + a                 # elementwise (NumPy/PyTorch-shaped)
c = a * 2.0               # scalar broadcast
d = matmul(a, a)          # matrix product, shape-checked
e = a ** 2.0              # elementwise power
z = zeros([2, 3]); i = eye(3); r = arange(10)
v = embed("a sentence")   # string -> vector, one call

Dimension safety. Shape is enforced: elementwise ops require matching shapes (scalars broadcast), matmul requires the inner dimensions to agree, and a mismatch is a typed ShapeError naming both shapes — “cannot elementwise-add tensors of shape [1, 2] and [2, 1]”. Tensors bridge the equation engine both ways: a Vec/Matrix result from an equation returns as a Tensor, and a Tensor flows into an equation.

Scientific number domains

Five checked scalar domains are built in as constructors — no import. Each is a bounded slice: what is listed works; everything else fails typed instead of silently approximating.

z = complex(3.0, 4.0)                 # abs(z) == 5.0, C99 branch cuts
w = math.sqrt(complex(-4.0, 0.0))     # principal branch
bounds = math.exp(interval(0.0, 1.0)) # certified enclosure of e^[0, 1]
q = quaternion(1.0, 0.0, 0.0, 0.0)    # Hamilton algebra, rotate/slerp
residue = modint(17, 5)               # canonical exact residue class
amount = decimal("12.345", precision=4, rounding="half_up")

complex carries signed-zero branch cuts through principal sqrt/exp/log/trig; interval results contain every represented real (1.5 in interval(1.0, 2.0) is a containment test); quaternion adds rotate(q, v) and shortest-path slerp; modint supports inverses and signed powers under same-modulus arithmetic; decimal makes precision and rounding an explicit context. All five interchange as tagged JSON and reject unaware foreign boundaries typed.

Linear algebra — dense, complex, sparse

Equation kernels expose checked det/solve/inv/qr/eigh plus reduced svd and scale-relative rank; matmul/matvec/solve also accept complex tensors (real operands promote exactly), and sparse(...) validates COO triplets into canonical duplicate-free CSR:

def linalg_tour() -> any !{}:
    a = tensor([[complex(2.0, 1.0), complex(0.0, 0.0)], [complex(0.0, 0.0), complex(1.0, -1.0)]])
    x = tensor([complex(1.0, 0.0), complex(0.0, 1.0)])
    equation:
        product := matvec(a, x)
        s := sparse(2, 2, [1, 0], [1, 0], [4.0, 2.0])
        applied := sparse.matmul(s, [1.0, 1.0])
        solved := sparse.solve(s, [2.0, 8.0])
    return (product, applied, solved)

Honesty bound

Dense kernels are validated through 16×16 conditioned systems with residual and orthogonality checks. sparse.solve densifies only square systems through 128×128 — beyond any bound you get a typed error, never a silent fallback — and sparse values exit equations as tagged records. Sparse-sparse products and true sparse factorizations are not yet available.

Statistics, distributions, and transforms

Population descriptive statistics, strict-simplex information measures (entropy/cross_entropy/kl_divergence/js_divergence, in nats), the complete scalar Normal family (normal_pdf/logpdf/cdf/sf/logcdf/ logsf/ppf/logppf — direct stable tails, never ln(cdf)), and rank-1 full convolution/cross_correlation:

equation stats_tour() -> any:
    return (mean([1, 2, 3]), entropy([0.25, 0.75]), normal_cdf(0.0, 0.0, 1.0), convolution([1.0, 2.0, 3.0], [4.0, 5.0]))

Number theory and interpolation

Exact bounded number theory, and Newton interpolation whose all-exact lane stays in QQ — exact rational results, not floats:

equation numbers_tour() -> any:
    return (prime_nth(25), prime_count(100), factorint(360), interpolate([0, 1, 2], [1, 3, 7], 1 / 2), polynomial_interpolate([0, 1, 2], [1, 3, 7]))

interpolate([0, 1, 2], [1, 3, 7], 1 / 2) returns exactly QQ(7, 4); any float input selects the strict finite-real lane instead. is_prime/factorint/ totient/divisors run through 2^32 - 1, prime_nth through index 100,000, prime_count through 2,000,000, plus 16,384-bit mod_inverse and generalized non-coprime crt.

Sets, logic, and the proof boundary

FiniteSet algebra (union/intersection/power_set/quantifiers) evaluates over explicit finite domains with reason-carrying three-valued Truth — no implicit Unknown-to-false coercion. The proof boundary never trusts its producer: prove_bezout emits a typed certificate that an independent checker replays, and lean.check runs real Lean 4.10 while honestly labeling results CheckedUntrusted — lean.is_verified stays false until the confined qualification contract is satisfied.

Standard-library math bindings

Rather than reimplement libm and collections per program, Sema surfaces the host (Rust) standard library under namespaces, adapted to its syntax. These are ordinary explicit imports:

• math — constants math.pi/math.e/math.tau/math.inf and elementwise functions cos/sin/tan/exp/ln/log/sqrt/abs/floor/ceil/tanh/… that apply to a scalar or a whole tensor (math.cos(t)).
• io — io.read_file/io.write_file/io.lines/io.exists/io.print/ io.println/io.eprint (paths relative to the project root; read/write return Result for expect/except).
• Collections — list/dict/set are native with the expected method set, plus free builtins enumerate/zip/map/filter/sorted/reversed/sum/ min/max/mean.

The full arithmetic operator set (+ - * / % and ** — exponentiation, right-associative, tighter than *) works over Int and Float, and elementwise on tensors; logarithms/roots/trig come from math.

import math

x = math.sqrt(2.0)
y = math.cos(a)            # applies elementwise to a whole tensor

Failure modes

• Unbounded quantifier domain → compile error.
• Non-differentiable point hit by ∇ → typed NotDifferentiable with the call path.
• Diverging ∫/lim/Fix → typed error with the residual trace.
• Solver non-convergence → Approx with .converged = false, never a bare number.
• Effectful call inside an equation → compile error (“lift the call out of the equation block”).
• Shape mismatch → typed ShapeError naming both shapes.
• Solving beyond quadratic / an atlas operator with no v0 kernel → typed error / math.NotImplemented.

See also

• Operators — why ^ is xor outside equations, power inside.
• Types — the numeric model and Tensor[T] prelude commitment.
• Modules — importing math / io.
• Multimodal guide — tensors and embeddings in practice.
• Scientific domains reference (generated) — every native math/equation function with signatures, from rational to sparse_linalg.