Arithmetic

The Hilbert compiler knows no algebraic identities of its own. A formula is emitted exactly as you wrote it — x · 1 stays a multiplication by one — until a law says otherwise. This module states the identities of a ring over the reals as laws, each oriented in the direction that makes a formula smaller, so that a document which opens it has those formulas reduced before code is generated.

A law is in force across the whole document once any file in it opens the module: every file compiled together with that file is reduced by the same laws. A compilation in which no file opens Prelude.Arithmetic keeps every · 1 and + 0 as written.

Matching is structural. The compiler does not assume that multiplication or addition commutes, so an identity that should apply on both sides is stated twice — unit for \(x \cdot 1\) and unit_left for \(1 \cdot x\). The derivative laws of Calculus rely on this module to tidy their results, and Prelude.Calculus opens it for you.

open Prelude.Arithmetic

Identities

Ten laws, each removing a neutral or absorbing element. They fire wherever their left-hand side appears, at any depth of a formula, and are applied repeatedly until none matches.

unit

law unit       = x · 1 = x

For all \(x \in \mathbb{R}\),

\[x \cdot 1 = x .\]

Fires on any product whose right operand is the literal one.

Intuition One is the multiplicative “do nothing”: scaling by it changes no value, so the factor is pure noise in the formula and in the emitted code. The law keeps x, so it is safe for tensors of any shape.

Use it when formulas are produced mechanically — derivatives (the product rule leaves ∂x/∂x · v, which becomes 1 · v), substituted parameters, templates — and you want the generated method free of * 1d. A literal one on the left needs unit_left.

symbolic-simplificationdifferentiationcode-generation

unit_left

law unit_left  = 1 · x = x

For all \(x \in \mathbb{R}\),

\[1 \cdot x = x .\]

Fires on any product whose left operand is the literal one.

Intuition The mirror of unit. Matching is structural and the compiler never assumes multiplication commutes, so \(1 \cdot x\) is a different term from \(x \cdot 1\) and needs its own law.

Use it when a leading one is left behind, as when Calculus’s product rule differentiates x · v and produces 1 · v. Like unit, it keeps its variable and is shape-safe.

symbolic-simplificationdifferentiationcode-generation

zero

law zero       = x + 0 = x

For all \(x \in \mathbb{R}\),

\[x + 0 = x .\]

Fires on any sum whose right operand is the literal zero.

Intuition Zero is the additive “do nothing”. A trailing + 0 usually marks a term that some earlier rewrite has already emptied, and this law removes the empty slot while keeping x and its shape.

Use it when you simplify sums produced by rewriting: after nil or constant turns a derivative term into zero, zero deletes it so 2x + 0 is emitted as 2x. A zero on the left needs zero_left.

symbolic-simplificationdifferentiationcode-generation

zero_left

law zero_left  = 0 + x = x

For all \(x \in \mathbb{R}\),

\[0 + x = x .\]

Fires on any sum whose left operand is the literal zero.

Intuition The mirror of zero, needed because addition is not assumed to commute: \(0 + x\) and \(x + 0\) are different terms to the matcher.

Use it when the emptied term is the first one, as in the derivative of y + x² with respect to x, where constant turns ∂y/∂x into a leading zero. It keeps its variable, so it is shape-safe.

symbolic-simplificationdifferentiationcode-generation

nil

law nil        = x · 0 = 0

For all \(x \in \mathbb{R}\),

\[x \cdot 0 = 0 .\]

Fires on any product whose right operand is the literal zero. The result is a plain zero with no shape of its own; see the note on shapes below.

Intuition Zero absorbs a product: whatever x is, the term contributes nothing. Removing it lets a whole sub-formula vanish, which is how the vanishing terms of the product rule disappear from a derivative.

Use it when derivatives must finish as clean formulas: \(\partial(2x + y)/\partial x\) only reduces to \(2\) because nil erases x · 0. Beware that it drops x’s shape — never rely on x · 0 to build a tensor of zeros where this module is open.

symbolic-simplificationdifferentiationcode-generation

nil_left

law nil_left   = 0 · x = 0

For all \(x \in \mathbb{R}\),

\[0 \cdot x = 0 .\]

Fires on any product whose left operand is the literal zero. Like nil, it replaces the whole product with an unshaped zero.

Intuition The mirror of nil: zero absorbs from the left as well, and since the matcher does not assume commutativity it needs its own law.

Use it when a derivative term becomes 0 · v, as when the product rule differentiates a constant factor such as 2 · x and produces 0 · x. Same shape caveat as nil: the result is a rank-0 zero.

symbolic-simplificationdifferentiationcode-generation

power_one

law power_one  = x^1 = x

For all \(x \in \mathbb{R}\),

\[x^1 = x .\]

Fires on any power whose exponent is the literal one. Differentiating \(x^2\) produces \(2 \cdot x^1\), and this law is what turns it into \(2x\).

Intuition A first power is the value itself; the exponent is bookkeeping left over from the power rule, which always writes \(u^{n-1}\) even when \(n = 2\). Without the law the generated code would call Math.Pow(x, 1d).

Use it when you differentiate quadratics or any \(x^2\) term, or substitute a parameter that happens to be one. It keeps x, so it is safe on tensors. There is deliberately no \(x^0 = 1\) companion (see below).

symbolic-simplificationdifferentiationcode-generation

neg_neg

law neg_neg    = −(−x) = x

For all \(x \in \mathbb{R}\),

\[-(-x) = x .\]

Fires on a double negation.

Intuition Flipping a sign twice leaves it where it started. Rewrites that each introduce a minus sign can stack two of them on one term, and this law collapses the pair.

Use it when sign-producing rules meet: differentiating −cos(x) applies negation and then cosine, and after unit the result would be \(-(-\sin x)\) without this law. It keeps its variable, so it is shape-safe.

symbolic-simplificationdifferentiationsign-normalisation

cancels

law cancels    = x − x = 0

For all \(x \in \mathbb{R}\),

\[x - x = 0 .\]

Fires when both operands of a subtraction are the same expression, written the same way. (x + 1) − x is not matched: the two sides are different terms. The result is an unshaped zero.

Intuition Anything minus itself is nothing. The match is syntactic, not algebraic: it recognises two identical terms, and does no expansion or reordering to discover that two different-looking terms are equal.

Use it when a formula subtracts a term from its own copy, as rewriting often produces. Do not expect it to cancel (x + 1) − x. It drops x’s shape, so x − x is not a tensor of zeros in a document where it is in force; write min(x^0, 0) for that.

symbolic-simplificationcode-generation

minus_zero

law minus_zero = x − 0 = x

For all \(x \in \mathbb{R}\),

\[x - 0 = x .\]

Fires on any subtraction of the literal zero.

Intuition Taking away nothing changes nothing. It is the subtraction counterpart of zero, needed because a difference is its own operator and is not rewritten into a sum.

Use it when the subtracted side of a difference has been emptied, as when the difference rule differentiates x² − c and constant turns \(\partial c/\partial x\) into zero. It keeps x, so it is shape-safe. There is no 0 − x law: that is a negation, not a no-op.

symbolic-simplificationdifferentiationcode-generation

Laws and shapes

Every value in Hilbert may be a tensor, and a law cannot see shapes: to a rewrite rule, a vector and a real are the same expression. A law that keeps its variable — unit, unit_left, zero, zero_left, power_one, neg_neg, minus_zero — is safe on tensors of any shape, because the value it returns still carries that shape.

nil, nil_left and cancels drop their variable, and the zero they leave behind is a rank-0 value. That is exactly right when the zero is added to or multiplied into something that already has a shape, which is what happens inside derivatives: \(\partial(2x + y)/\partial x\) first becomes \(2 \cdot 1 + x \cdot 0\), and only nil lets it finish as \(2\). It is wrong when you meant the zero to have a shape. In a document where these laws are in force, x − x is not a way to write “a tensor of zeros shaped like x”; write min(x^0, 0) instead, which no law rewrites.

Why there is no x^0 = 1 law

\(x^0 = 1\) is true of a real, but for a tensor x^0 is a tensor of ones shaped like x, while 1 is a single rank-0 value. Several Prelude modules build their vector of ones as x^0 — for example ones in Statistics, on which ranks, sorting and the median depend — so a law rewriting it to 1 would silently remove that shape from every document that opened Arithmetic, and functions such as median would fail. For that reason the module deliberately has no power_zero law: x^0 is left exactly as written.

Examples

Tidy a formula before it is compiled

A formula that carries neutral elements is emitted without them.

open Prelude.Arithmetic

fn scaled(x, y) ↦ (x · 1 + 0) · y^1

using Examples;

var r = Tidy.Scaled(3.0, 4.0);

Output (verified):

The generated real-valued method is the reduced formula:

public static double Scaled(double x, double y) =>
    (x * y);

Compiled without open Prelude.Arithmetic (and with no other file of the document opening it), the same doorway is emitted as written: (((x * 1d) + 0d) * System.Math.Pow(y, 1d)).

Absorbing and cancelling terms

cancels, nil and nil_left together reduce a whole expression to zero.

open Prelude.Arithmetic

fn leftover(x, y) ↦ (y − y) + x · (0 · y)

using Examples;

var r = Tidy.Leftover(3.0, 4.0);

Output (verified):

The generated real-valued method is 0d: neither argument is read.

Double negation

open Prelude.Arithmetic

fn twiceNegated(x) ↦ −(−x) − 0

using Examples;

var r = Tidy.TwiceNegated(5.0);

Output (verified):

neg_neg and minus_zero reduce the body to x.