Compute — a CAS at run time

laws.md is about the build: what the compiler folds and rewrites while it turns .hb into C#. This page is about afterwards — a running program that wants to simplify, differentiate, prove or solve an expression it only has as a string, using the same laws.

A CAS per file

-- Maths.hb
open Prelude.Calculus
model Maths {
  law cancel = u − u = 0
}

A file whose scope sees at least one law gets a static member — in its own generated class, or, on a model path, in a <File>.Compute.g.cs class beside the models (the one exception, HB0002, is under Build-time checks below):

public static MLambda.Hilbert.Algebra.Compute Compute { get; }

The member carries the laws as .hb text and parses them lazily, once — on the first read of Compute, never in the class’s static initialiser — so calling one of the file’s formulas costs no parse at all.

Maths.Compute fires only the laws Maths.hb declares or opens — nothing another file of the same project happens to open, and nothing invented. Precisely:

R(F) = own(F) ∪ ⋃_{o ∈ opens(F)} R(o)

Laws are document-wide at build time (laws.md); Compute is per-file — A.hb that opens only Prelude.Arithmetic gets a Compute that cannot resolve a derivative, even sitting beside a B.hb that opens Prelude.Calculus in the same project. The input to every operation is expressions only — text, not a model or a fn.

Maths.Compute.Derivate("sin(x²)", "x");   // Resolved(cos(x²) · 2 · x, steps)

A file with no laws in scope gets no Compute member at all.

Build-time checks

Compute is a reserved name: once a file sees a law, its generated class already carries a Compute member, so a fn or def whose C# method name would be Compute is a build error — a method name capitalises only the first letter of the .hb name, so compute collides while cOMPUTE (method COMPUTE) does not — and a whole file named Compute.hb is refused the same way — the check is a name reservation only, not a recursion analysis, because Compute never reads a fn/def body. On a model path (a library of frame/process/learner/trained models) the CAS instead lives beside the models as <File>.Compute.g.cs, unless one of the file’s own models already claims the file’s class name — then no Compute is emitted, and the build prints HB0002 as a warning, not a fault. Two different files whose generated classes would collide on one name in one namespace are refused at build with a diagnostic naming both files.

The laws text a generated Compute will parse is parsed at build time first. It is printed back from the syntax tree, so a spelling the printer writes and the parser refuses is a build error naming the file — never an exception the first time a running program reads Compute. A term law and an equation law that share a name are refused at build too (and by Compute.Of), since a rw step naming it could mean either.

Operations

Expressions are Hilbert text; results print back through the same printer as .hb source (ToString()), and steps is the ordered list of law names that fired.

Operation	Input	Result
`Simplify(e)`	expression	`Rewritten(value, steps)`
`Derivate(e, x)`	expression, variable	`Resolved(value, steps)` \| `Unresolved(residue, steps)` — a `∂` was left
`Integrate(e, x)`	expression, variable	`Resolved` \| `Unresolved` — an `∫` was left
`Substitute(e, x, v)`	expression, variable, expression	`Rewritten` — free `x` replaced by `v`, then simplified
`Function(λ)`	lambda	a compiled `Function` delegate
`Evaluate(λ, args…)`	lambda, values	`Value` = `Function(λ)(args…)`
`Proof(t)`	theorem with `by`	`Checked(steps)` \| `Failed(step, left, right, reason)`
`Demonstrate(t)`	theorem without `by`	`Demonstrated(steps, theorem)` \| `NotFound(closest)`
`Equivalent(a, b)`	two expressions	`bool` — `Demonstrate("theorem _ : a = b")` found a proof
`Solve(eq, x)`	equation, variable	`Solved(x, value)` \| `Unsolved(closest)`

Maths.Compute.Simplify("x · 1 + 0");                          // Rewritten(x, [unit, zero])
Maths.Compute.Derivate("x²", "x");                             // Resolved(2·x, [power, self, unit, power_one])
Maths.Compute.Substitute("x · 1", "x", "a + 1");                // Rewritten(a + 1, …)

Derivate builds ∂ e / ∂ x and rewrites it; Integrate builds ∫ e d x. You can also hand a ∂ u / ∂ x or ∫ u d x term straight to Simplify. Substitute refuses with ComputeSyntaxException when replacing a name would let a free variable of the replacement be captured by a lambda’s own parameter — Substitute("(y) ↦ x + y", "x", "y") is refused; substituting z for x there is fine. A ∂ … / ∂ y or ∫ … d y binds y the same way, so Substitute("∂ (x · y) / ∂ y", "x", "y") is refused as well. The variable of Derivate, Integrate, Substitute and Solve must be a variable: π, e, or a nullary def the scope knows is a constant, and naming one is a ComputeSyntaxException.

Every result prints as .hb text (ToString(), and so $"{result}"): Rewritten, Resolved and Unresolved print their term, Demonstrated its theorem, Solved x = t, Failed the step, the reason and both sides, NotFound/Unsolved the closest goal as left = right, and Checked its steps as [unit, zero].

Proof and Demonstrate

A theorem with steps is checked; a theorem without steps is searched for, and what the search finds is written back as steps you can check:

Maths.Compute.Proof("theorem t : x · 1 + 0 = x by rw [unit, zero]");       // Checked([unit, zero])
Maths.Compute.Demonstrate("theorem t : x · 1 + 0 = x");                    // Demonstrated([unit, zero], "…by rw […]")

Two tactics, both accepted by Proof:

by rewrite [a, b] — both sides are normalised with the listed laws and compared for equality.
by rw [a, ← b, c] — replay. Each step rewrites the first matching instance of one law’s pattern, on both sides, in order; the proof is Checked only once the sides meet after the last step.

Demonstrate always emits rw steps, so Proof(Demonstrate(t).Theorem) is Checked by construction whenever Demonstrate finds a proof — that is the round-trip property this module’s own test suite holds itself to (ComputeCase.Every_corpus_theorem_the_search_demonstrates_is_checked_by_proof, and DemonstrateCase). The theorem written back keeps the claim’s name and its ∀ binder. A claim whose folded sides are already one term (x = x, 1 + 1 = 2) needs no step: Demonstrate writes it back with no by, and Proof answers Checked([]) for a stepless claim that is already closed (and Failed for one that is not).

Both tactics fold before they match — the claim’s sides and every law’s sides, the same way at build time as in Proof — so y^(0 − 1) meets a law about x^(−1) as y^-1 against x^-1 in both, and a theorem the build establishes is one Proof checks over the same laws.

A theorem is a rule of the scope only once it is established there. A Compute parses its file’s laws and theorems together, and a theorem whose steps name a law outside that file’s scope — one another file opened — does not check there, so it is not a rule of that Compute even when the library’s build accepted it.

A step can run a law backwards (← name) only when doing so invents nothing: every variable of the law’s left side must already be bound by its right side, vars(l) ⊆ vars(r). law nil = x · 0 = 0 would have to invent an x read right to left, so it is never reversed — Demonstrate never offers ← nil, and Proof refuses it if you write it by hand.

Solve and equation laws

Solve searches for x = t with x not free in t. Ordinary term laws move sub-terms; only an equation law, written with ⇔, can move a whole equation — so without one, Solve cannot isolate a variable at all:

law sub_add = a + b = c ⇔ a = c − b
law div_mul = a · b = c ⇔ b = c / a

compute.Solve("2 · x + 3 = 7", "x");   // Unsolved(closest) — no transposition law is open
// with sub_add and div_mul open:
compute.Solve("2 · x + 3 = 7", "x");   // Solved("x", 2)

Functions

A lambda simplifies under the file’s scope, then compiles once to a delegate:

public delegate Value Function(Value x, params Value[] rest);

var f = Maths.Compute.Function("x ↦ x · 1");
f(1);           // 1
f([1, 2, 3]);   // [1, 2, 3]  — one Value, a vector, not three arguments

var g = Maths.Compute.Function("(x, y) ↦ x + y");
g(1, 2);        // 3

Value is a scalar or a tensor, implicit from double, int and double[] (Value.Of(double[,]) for rank 2). Calling a compiled function with the wrong number of arguments throws ArgumentException naming both counts. Scalar intrinsics (sin, exp, ln, …) lower to System.Math; a name Function does not know, or a ∂/∫ the file’s laws could not remove, is a ComputeSyntaxException raised when you call Function, not later when you call the delegate. A reduction such as minimum/maximum is not elementwise and has no value inside a compiled function, so it is refused the same way. A lambda that repeats a parameter name ((x, x) ↦ …), names no parameter (() ↦ 1), or names a parameter like a constant (e ↦ e + 1, or a nullary def the scope knows — every use would mean the constant) is refused too.

What a body lowers to is a deliberate subset of the language, checked when Function is called:

numbers, the lambda’s parameters, and the constants π and e;
unary − and the binary + − · / ^;
the elementwise intrinsics sin cos tan exp ln sqrt abs (and |x|, which is abs), floor ceil round sign, atan asin acos, sinh cosh tanh, and min/max of two arguments.

Anything else is refused with ComputeSyntaxException — a tensor literal ([x, 1]), a comparison (x < 1, x = 1), a reduction or shape query (minimum, rows, …), a call no intrinsic answers.

Integration prelude

Prelude.Integration is opt-in (open Prelude.Integration) and states antiderivatives as laws — constant, sum, constant factor, sin, cos, exp, and power. A guard cannot say n ≠ −1, so the prelude declares the reciprocal law before the power law and relies on first-match-wins against the literal −1:

law int_reciprocal = ∫ (x^(−1)) d x = ln(x)
law int_power       = ∫ (x^n) d x = x^(n + 1) / (n + 1) where x ∉ n

A symbolic n that turns out to be −1 only at run time is not caught — x^(n+1)/(n+1) divides by zero — and int_reciprocal’s ln(x) holds only for x > 0. Both are stated limitations of this prelude, not bugs: a rewrite rule cannot check a run-time sign.

Limits

A search (Demonstrate, Solve) is bounded, so it always terminates: depth ≤ 8, ≤ 10,000 goals visited, and a term may not grow past 2 · max(|l|, |r|) + 8. On a cap, NotFound/Unsolved carries the explored goal that came closest (smallest first, ties broken by depth). A Compute built by Of uses the defaults; WithLimits returns a copy searched within limits you choose:

var patient = Maths.Compute.WithLimits(new MLambda.Hilbert.Algebra.Limits(Depth: 12));