Laws and derivatives

Most computer algebra systems ship a simplifier: a large, invisible body of rules deciding what sin(x)² + cos(x)² becomes. Hilbert has none. When the compiler reduces a formula it folds numbers (2 · 3 is 6) and substitutes definitions — and applies only the laws of the modules that are opened.

Laws

A law is a named rewrite from a pattern to a simpler expression, declared inside a model:

model Arithmetic {
  law unit       = x · 1 = x
  law zero       = x + 0 = x
  law power_one  = x^1 = x
}

Every name in a law is a pattern variable unless it is a constant (π, e) or a definition. x · 1 = x matches (a + b) · 1 with x = a + b.
Matching is structural. No commutativity is assumed, so an identity that holds both ways is stated both ways — the Prelude has unit (x · 1) and unit_left (1 · x).
A law is applied bottom-up to a fixed point, and a rewrite is kept only if it makes the expression smaller (except a rewrite that removes a derivative, which is always kept).
Laws are document-wide: once any file of a project opens Prelude.Arithmetic, its laws act on every formula compiled together with it.

A generated method records which laws reduced it, for example <remarks>Reduced by power, self, unit, power_one.</remarks> on the derivative of x².

A law may have a guard

Some identities hold only under a side condition. where x ∉ u (ASCII notin) says the variable x must not occur in the expression u:

law constant = ∂ u / ∂ x = 0 where x ∉ u
law power    = ∂ (u^n) / ∂ x = n · u^(n − 1) · ∂ u / ∂ x where x ∉ n

Laws that are true only on part of the domain — exp(ln(x)) = x holds only for positive x — are deliberately absent from the Prelude: a rewrite rule cannot check the sign of a run-time value, and it would silently “repair” a formula that ought to fail.

Derivatives are rewriting

∂ u / ∂ x is an ordinary term. Prelude.Calculus states the rules of differentiation as laws — self, constant, sum, difference, negation, product, quotient, power, sine, cosine, exponential, logarithm and root — each oriented so that it removes a ∂. A doorway that still contains a derivative after reduction is not emitted, and no error is printed — this happens when Prelude.Calculus is not opened, and for functions it has no rule for (∂ tan(x) / ∂ x, ∂ x^x / ∂ x). If a method you expect is missing from the generated class, look for a derivative that could not be taken.

open Prelude.Calculus
open Prelude.Trigonometry

fn slope(x)  ↦ ∂ x² / ∂ x                -- 2x
fn rate(x)   ↦ ∂ (sin(x) · x) / ∂ x      -- cos(x) · x + sin(x)
fn chain(x)  ↦ ∂ sin(x²) / ∂ x           -- cos(x²) · 2x
fn energy(x) ↦ sin(x)² + cos(x)²         -- 1, by the pythagorean law

Slopes.Slope(3);      // 6
Slopes.Rate(0);       // 0
Slopes.Chain(1);      // 1.0806046117362795   (= 2 cos 1)
Slopes.Energy(0.7);   // 1 — the formula was reduced to a constant before it was compiled

∂ x² / ∂ x meets power, then self, then Arithmetic’s power_one and unit: 2 · x^1 · 1 becomes 2x, and every step is a law you can open and read.

Writing a derivative. The body of ∂ … / ∂ x is one factor: ∂ x² / ∂ x, or parenthesise a sum, ∂ (u + v) / ∂ x. There is no ASCII spelling for ∂.

Theorems

A theorem states an equation and names the laws that prove it. The compiler checks it while building: both sides are rewritten with the listed laws, and the build fails — printing both normal forms — if they do not meet.

open Prelude.Arithmetic

theorem settled : (x · 1) + 0 = x by rewrite [unit, zero]

A theorem that does not check is a build error, so a library’s identities are verified every time it is compiled.

To use these laws from a running program, see Compute.

The Prelude’s law modules

Module	What it states
Arithmetic	ring identities: units, zeros, `x^1`, double negation, `x − x`, `x − 0`
Trigonometry	Pythagoras, double angles, odd/even symmetry
Calculus	the rules of differentiation, with guards

Because the laws are ordinary Hilbert, you can write your own model of laws for your domain and open it the same way.