The claim grammar¶
Every example on this page is taken from mathema.lexicon.LEXICON, a
curated set of claims that is checked by the test suite, so nothing
here can drift away from what the parser actually accepts.
A claim is one string. At its simplest it is a relation between the
function under test, written f, and something else:
f(x) == x
Everything after that is optional detail: where the claim applies, what the symbols mean, and what you are allowed to assume.
Terse in, explicit out¶
The grammar accepts the shortest reasonable spelling of anything, and several spellings of most things, because a claim you have to look up the syntax for is a claim you will not write. ASCII and Unicode are interchangeable, and equivalent spellings parse to exactly the same claim:
| These are the same claim |
|---|
f(x) <= 1 and f(x) ≤ 1 |
for x in [0, 1], f(x) >= 0 and for x ∈ [0, 1], f(x) ≥ 0 |
for n in [0, 100] subset Z, f(n) >= 0 and for n in [0, 100] ⊂ ℤ, f(n) >= 0 |
d(f(x), x) >= 0 and f'(x) >= 0 |
integrate(f(x), x, 0, 1) == 1 and ∫(f(x), x, 0, 1) == 1 |
for x in [0, 1], f(x) >= 0 and ∀ x ∈ [0, 1], f(x) ≥ 0 |
for n in [0, 100] subset Z, f(n) >= 0 and ∀ n ∈ [0, 100] ⊂ ℤ, f(n) ≥ 0 |
f(x)^2 >= 0 and f(x)² ≥ 0 |
for x in [0, 1], sqrt(f(x)) >= 0 and ∀ x ∈ [0, 1], √(f(x)) ≥ 0 |
for x in [0, 1], f(x) * 2 == 4*x and ∀ x ∈ [0, 1], f(x) · 2 == 4*x |
for x in [0, oo), f(x) >= 0 and ∀ x ∈ [0, ∞), f(x) ≥ 0 |
for x in [0, 1], f(x) >= 0 and \forall x \in [0, 1], f(x) \geq 0 |
What you get back is never terse. Whatever mathema resolved your input
to is rendered explicitly in the record, the error message and the
proof condition, so a shorthand never quietly becomes something you did
not mean. Setting MATHEMA_UNICODE=0 switches output to ASCII; see
symbology and rendering.
Mathematical notation, and how to read it¶
Every symbol below is accepted by the parser and means exactly what its ASCII spelling means, so a claim can be written the way the mathematics is written without becoming a different claim. Code points are given because several of these have visually identical neighbours that are not the same symbol, and a claim pasted out of a PDF is a common way to meet one.
| Symbol | Code point | Read it as | ASCII |
|---|---|---|---|
∀ |
U+2200 | for all | for |
∈ |
U+2208 | in, an element of | in |
⊂ |
U+2282 | a subset of | subset |
ℝ |
U+211D | the reals | R |
ℤ |
U+2124 | the integers | Z |
ℕ |
U+2115 | the naturals | N |
ℂ |
U+2102 | the complex numbers | C |
≤ |
U+2264 | less than or equal to | <= |
≥ |
U+2265 | greater than or equal to | >= |
≠ |
U+2260 | not equal to | != |
≈ |
U+2248 | approximately equal to, within a tolerance | ~= |
≡ |
U+2261 | equivalent to, as a whole function, in its mathematics and its computation | =:= |
⟹ |
U+27F9 | implies | => |
· |
U+00B7 | times | * |
× |
U+00D7 | times | * |
− |
U+2212 | minus | - |
√ |
U+221A | the square root of | sqrt |
∞ |
U+221E | infinity, also written oo or infinity |
inf |
∂ |
U+2202 | the partial derivative of | d( |
∫ |
U+222B | the integral of | integrate( |
→ |
U+2192 | tends to, inside a limit | -> |
⌊ ⌋ |
U+230A, U+230B | the floor of | floor( |
⌈ ⌉ |
U+2308, U+2309 | the ceiling of | ceil( |
| | |
U+007C | the absolute value of | abs( |
|| || |
U+007C | the norm of; _1, _2 or _inf after the closing bars is the order |
norm( |
‖ ‖ |
U+2016 | the norm of; ₁, ₂ or ∞ after the closing glyph is the order |
|| || |
² |
U+00B2 | squared, and likewise ³ and the rest |
^2 |
Greek letters are accepted as themselves (α, σ, Δ), and so are the
mathematical-italic Greek letters in U+1D6E2 to U+1D7FF, which is what many
PDF and LaTeX renders paste instead. Both spell the same parameter. Where a
symbol has a plain LaTeX command with no braces, that is accepted typed
literally too, so \forall x \in [0,1], f(x) \geq 0 is the same claim as
its Unicode and ASCII forms.
A few more spellings are accepted and read as their ascii forms:
| Spelling | Reads as |
|---|---|
∀ x ∈ [1, 4], f(x) ≥ √x |
√ without parentheses, the root of the atom after it |
∀ x ∈ [1, 2], f(x) ≥ x⁻¹ |
a superscript minus, a negative power |
let g = mathema.lexicon.double, f \equiv g |
\equiv, function equivalence |
\forall x \in [0, 1], f(x) \leqslant 2 |
\leqslant, the slanted <= |
\forall x \in [0, 1], f(x) \geqslant 0 |
\geqslant, the slanted >= |
for x in [0, 1], abs(f(x) - x) \leq \varepsilon |
\varepsilon, the claim's tolerance like ε |
for \varphi in [0, 1], f(\varphi) \leq 1 |
\varphi, the letter φ |
for x in [-1, 1], \left| f(x) \right| \leq 2 |
\left/\right sizing, dropped |
A radical whose reach would be unclear (√x^2) is refused; write
√(x^2) or (√x)^2.
The look-alikes worth knowing about¶
⊂ (U+2282) is the subset operator the grammar accepts. ⊆ (U+2286) is
deliberately rejected, with an error rather than a silent reinterpretation,
because a proper subset and a subset-or-equal are different mathematical
statements and treating them as spellings of one another would quietly change
what you claimed.
Two pairs go the other way and are merged, since they are typesetting
variants of one symbol rather than distinct ones: ⩽/⩾ (U+2A7D, U+2A7E) are
the ISO-style slanted forms of ≤/≥, and 𝜋 (U+1D70B, mathematical italic)
is the same constant as π (U+03C0).
And keep ≡ and ≈ apart, since they sit next to each other on this page and
mean very different things. ≡ claims two implementations are the same
function, adjudicated on its own ladder. ≈ claims equality within a
tolerance.
Symbols beyond this set¶
This table is the notation the core grammar knows. For domain-conventional symbols, the notation a particular field expects for its own quantities, see mathema-symbology, which supplies those names and renders claims in them.
Relations¶
| Spelling | Meaning |
|---|---|
f(x) == x |
equality |
f(x) ≤ 1 |
inequality, in either ASCII or Unicode |
f(x) ~= x |
approximate equality, within a tolerance |
f =:= g |
function equivalence: two implementations of the same mathematics, whose computations agree within the claim's tolerance |
f equiv g |
the word alias for the same relation |
for a in [0.1,10], b in [0.1,10], 2/(1/a+1/b) <= f(a,b) <= (a+b)/2 |
a chained comparison, both bounds in one claim |
for s in L[unicode], f(s) in L[unicode] |
membership: every output is a member of a language or a set, ∈ in Unicode |
for x in [0, 1], f(x) in [0, 1] |
membership in a numeric interval, read as the chain it means |
for s in L[unicode], "<" not in f(s) |
containment: the value on the left is never found in the value on the right, ∉ in Unicode |
How close counts as equal¶
a ~= b means abs(a - b) <= ε, with ε the claim's declared
tolerance or else 1e-9 (see below), and the record says so: "read as
abs(f(x) - x) <= ε, ε = 1e-9 (the default)". On the derive route every
relation is decided exactly: == asks whether the two sides are the same
over the whole domain, in exact real arithmetic, and ~= whether their
difference stays within ε, so x + 1e-12 is not x under == and is
under ~=. A definition row in a compendium is an exact equation, written
with ==.
On the probe route, which runs the real function in floating point, ~=
is the same abs(a - b) <= ε in float64, and == counts the computed
sides as equal when they agree within the computation's allowance, a
relative 1e-7 of the result plus an absolute part of at most 1e-9. A draw
that passes only within that allowance is decided again in exact
arithmetic wherever the body can be read exactly, so x * (1 + 1e-8)
written in the body is not x under ==, while the same factor read from
a module constant, which has no exact reading, leaves such a draw
inconclusive and uncounted. A claim sets its own absolute tolerance with the
tolerance field of a claims file, or tolerance= on mathema.claim(),
and that value replaces the whole allowance: the two sides must agree within
it, with no relative tolerance on top. On ==, <=, >= and !=, as
on a function equivalence f =:= g, the tolerance governs the
computation line alone, since the mathematics line is exact: x + 1e-6
== x with a tolerance of 1e-3 is falsified by its exact gap, as is x +
1e-10 <= x with a tolerance of 1e-9, and "close enough mathematically"
is ~=, as Multi-function claims describes
for =:=. A single a ~= b, and an f =:= g, may also name the
tolerance's kind (see Tolerance kinds below), while
every other relation takes a bare number.
Inside the claim text, ε (also eps, epsilon or \epsilon) names that
tolerance directly: the declared value when there is one, and the 1e-9
default otherwise, on both routes. It is never a free variable to sample, and
a function parameter that happens to be called eps or ε stays a
parameter. With two functions in gaps.py, one off by 1e-10 and one by
1e-7:
def nearly_identity(x: float) -> float:
return x + 1e-10
def small_gap(x: float) -> float:
return x + 1e-7
mathema check gaps.py --claim "for x in [0, 1], abs(f(x) - x) <= ε"
ok gaps.nearly_identity: source, no side effects; claims 3/3 checked (1 proven, 2 holds, 0 falsified)
FAIL gaps.small_gap: source, no side effects; claims 2/2 checked (0 proven, 1 holds, 1 falsified) <- 1 falsified claim(s)
The first gap is within the default tolerance and proves for every x in the
range (its second claim is the proof's [float] companion, which holds); the
second is a hundred times larger than it and is falsified.
The other relations use the same allowance where it makes sense: <= and
>= accept a difference within the absolute tolerance, < and > accept
none, since equality must not pass for strictly less, and != with no
declared tolerance fails only where the two sides are exactly equal.
On the probe route a draw whose computed values meet ==, <= or >=
only within the allowance (inside its absolute part as well as through
its relative part) is decided again in exact arithmetic wherever the
body can be read exactly, its literals as the decimals written: false
there falsifies, with that draw as the witness, so the allowance never
carries a claim that is false at a point the probe ran. Where the body
cannot be read exactly (a float it reads from outside, a library's
value), such a pass is no evidence either way: it is not counted, and a
claim with no other draw ends unknown with the note "N draws passed
only within the tolerance and could not be evaluated in exact
arithmetic, so they are not counted". A declared tolerance makes such a
pass count, since the claim asks for that allowance.
Every computation line that holds with a gap the tolerance absorbed says
so in its note, for == as for <= and >=, on every route (a probe
line, a ground claim's one call, the [float] line a proof spawns, the
computation row of an f =:= g claim): the largest gap, the point it
was measured at, and the tolerance it fell within (the declared one, or
the default allowance's value at that point). A pass with no gap carries
no such clause, so a bit-exact pass reads apart from an absorbed one.
The derive route has no allowance
to spend: when it disproves a <=, >= or == claim, the real code is
run at derive's witness and compared exactly, and a violation there,
however small, falsifies the claim with that point as the witness. So
f(x) == x is falsified for x + 1e-10, but not for x + 1e-20 on
[1, 2], where rounding makes the executed values exactly equal. For a
function that returns -1e-10:
import mathema
def just_below(x: float) -> float:
return -1e-10
for route in ["probe", "derive"]:
(p,) = mathema.claims.check(
just_below, [mathema.claim("for x in [0, 1], f(x) >= 0", route=route)])
print(f"{route:7} {p.verdict:9} {p.counterexample or ''}")
print(f" {p.note}")
probe falsified x = 0: -1e-10 vs 0, within the float tolerance but false here in exact arithmetic
derive falsified x = 0.06163325083761284
reproduced exactly at derive's witness: the executed code misses the relation there by 1e-10, within the allowance (1e-09) the probe route gives the computation, and compared exactly it fails
A declared tolerance binds the computation line only: the probe
compares the floats within it, and derive's disproof stands on the exact
gap however small. Where the executed code rounds the difference away, the body is
read exactly at derive's witness: a literal is the decimal written, so
x + 1e-20 is x + 1/10^20 and the claim is falsified on the
mathematics, the record noting that the float computation holds within
its allowance. A derive disproof that neither the executed code nor the
exact reading reproduces (the gap comes from a float the body reads
from outside, a module constant or a library's value) comes back
unknown with mathema.corroboration: "uncorroborated"; when the exact
comparison ran at the point where the exact difference is, the record
adds mathema.corroboration_reason: "exact arithmetic only" and the note
says the difference exists in exact arithmetic and floating point does not
reproduce it. Any other unreproduced disproof is flagged as a probable
engine bug.
Tolerance kinds¶
A bare number is an absolute allowance, which is the wrong shape for a
value that spans many orders of magnitude: an option deep out of the
money prices at 1e-7 and the same function prices at 190 in the money,
so 1e-9 is half a percent of the small price and a rounding error at
the large one. On a ~= b (and on f =:= g) the tolerance may instead
name its kind, in a claims file as tolerance: {rel: 1e-9, floor: 1e-14}
or on mathema.claim() as tolerance={"rel": 1e-9, "floor": 1e-14}:
| Kind | Allows |
|---|---|
{abs: x} |
abs(a - b) <= x |
{rel: x} |
abs(a - b) <= x * max(abs(a), abs(b)) |
{ulp: n} |
abs(a - b) within n units in the last place of the float64 nearest max(abs(a), abs(b)), n a whole number |
floor: x, beside any of them |
adds x to the kind's own allowance |
The floor adds, so {rel: 1e-9, floor: 1e-14} allows 1e-9 * max(abs(a),
abs(b)) + 1e-14, which is the relative-plus-absolute error of the
standard rounding-error model, and it applies in full. On the mathematics
line the inequality is decided exactly, each number of the kind read as
the decimal written; on the computation line it is computed in float64.
A kind is not one number, so a claim that reads ε in its own text, a
premise compared within the tolerance (==, != or ~= after
assuming) and a chain of relations refuse it.
The two call prices below are the same mathematics, one with its normal
CDF from erfc and the other from 1 + erf, which cancels for a far
out-of-the-money call:
import math
import mathema
def call_erfc(spot: float) -> float:
d1 = (math.log(spot / 100) + 0.03) / 0.2
d2 = d1 - 0.2
return (spot * math.erfc(-d1 / math.sqrt(2))
- 100 * math.exp(-0.01) * math.erfc(-d2 / math.sqrt(2))) / 2
def call_erf(spot: float) -> float:
d1 = (math.log(spot / 100) + 0.03) / 0.2
d2 = d1 - 0.2
return (spot * (1 + math.erf(d1 / math.sqrt(2)))
- 100 * math.exp(-0.01) * (1 + math.erf(d2 / math.sqrt(2)))) / 2
law = "for spot in [35, 290], f(spot) ~= g(spot)"
for tolerance in [1e-9, {"rel": 1e-9}, {"rel": 1e-9, "floor": 1e-14}]:
rows = mathema.check(call_erfc, claims=[mathema.claim(
law, funcs={"g": call_erf}, tolerance=tolerance)]).probes
for p in rows:
if p.name.startswith("f_spot"):
print(f"{p.name:28} {p.verdict:9} {p.counterexample or ''}")
print(rows[0].note)
f_spot_approx_g_spot proven
f_spot_approx_g_spot[float] holds
f_spot_approx_g_spot proven
f_spot_approx_g_spot[float] falsified spot = 35
f_spot_approx_g_spot proven
f_spot_approx_g_spot[float] holds
read as abs(f(spot) - g(spot)) <= 1e-9 * max(abs(f(spot)), abs(g(spot))) + 1e-14, the tolerance {rel: 1e-9, floor: 1e-14} (declared)
The mathematics is proven under all three. Under the bare 1e-9 the
computation holds, though that allowance would also pass a price of
2e-7 that is off by half a percent; under {rel: 1e-9} it is falsified
at spot = 35, where the erf form's cancellation leaves a gap of about
4e-15 on a price of 2e-7, a relative error of 2e-8; and the floor of
1e-14 covers that cancellation while the relative part still judges
the large prices.
{ulp: n} counts rounding steps, for an implementation that claims to
agree with another to the last bit or close to it. (x * 3) / 3 is
exactly x, so the mathematics is proven, and in float64 it is off by
at most one unit in the last place:
import mathema
def thirds(x: float) -> float:
return (x * 3) / 3
for tolerance in [{"ulp": 0}, {"ulp": 1}]:
rows = mathema.check(thirds, claims=[mathema.claim(
"for x in [-10, 10], f(x) ~= x", tolerance=tolerance)]).probes
for p in rows[:2]:
print(f"{p.name:20} {p.verdict:9} {p.counterexample or ''}")
print(rows[0].note)
f_x_approx_x proven
f_x_approx_x[float] falsified x = -5.858032318615711
f_x_approx_x proven
f_x_approx_x[float] holds
read as abs(f(x) - x) <= 1 unit in the last place of the float64 nearest max(abs(f(x)), abs(x)), the tolerance {ulp: 1} (declared)
A proof does not express the float64 nearest a value, so under {ulp:
n} the mathematics line is proven only where the two sides are equal,
and otherwise the probe decides it, exactly, at each point it draws.
A floor beside abs adds the two, which reads oddly on its own and is
shown here only to make the arithmetic plain: an offset of 1.5e-9
misses {abs: 1e-9} and is within {abs: 1e-9, floor: 1e-9}:
import mathema
def shifted(x: float) -> float:
return x + 1.5e-9
for tolerance in [{"abs": 1e-9}, {"abs": 1e-9, "floor": 1e-9}]:
(p, *_) = mathema.check(shifted, claims=[mathema.claim(
"for x in [1, 2], f(x) ~= x", tolerance=tolerance)]).probes
print(f"{p.verdict:9} {p.counterexample or ''}")
print(f" {p.note}")
falsified x = 1.061633250837613
read as abs(f(x) - x) <= 1e-9, the tolerance {abs: 1e-9} (declared)
proven
read as abs(f(x) - x) <= 1e-9 + 1e-9, the tolerance {abs: 1e-9, floor: 1e-9} (declared)
Expressions¶
| Spelling | Meaning |
|---|---|
f(x)^2 >= 0 |
powers with a caret |
|f(x)| <= 1 |
absolute value with bars |
for x in [0, 1], y in [0, 1], |x + y - f(x, y)| <= ε |
bars around any expression; on matrices, the determinant |
for x in R^n, f(x) ~= ||x||_1 |
a norm with double bars, the order a subscript; ^2 after the bars is the square |
for n in [1, 5] subset Z, f(n) <= n! |
postfix factorial |
f(x, 1.0) == x[-1] |
indexing into a sequence parameter |
f(\alpha) ≤ 1 |
a Greek name written as a LaTeX escape |
for x in [1, 5], f(x) == exp(1) |
the mathematical constants and functions |
Bare bars are the Euclidean norm of a vector and the Frobenius norm of a
matrix. _1, _2, _inf (also _oo, _∞) and a whole number _p
name the other orders; on a matrix _1 is the largest column sum, _2
the spectral norm and _inf the largest row sum, numpy's ord. The
order is never a superscript, so ||x||^2
is the square of the norm. A claim written with the bars and one
written with norm(...) are one claim: the claims file keeps the
spelling you wrote, and the record's statement is the call form.
What each of the grammar's words computes (sum, mean, std,
dot, norm, det, cumsum, quantile and the rest), where it has
a value, its keywords and what it does with a missing slot is listed on
the grammar's words.
Domains: where the claim applies¶
A claim with no domain is a claim about every input, which is usually
stronger than you mean. The for clause narrows it:
| Spelling | Meaning |
|---|---|
for x in [0, 1], f(x) >= 0 |
a closed interval |
for x in (0, 1), f(x) >= 0 |
an open interval, and (0, 1] for half-open |
for n in [0, 100] subset Z, f(n) >= 0 |
restricted to the integers |
for n in N, f(n) >= 0 |
the naturals, with Z, R and C likewise |
for z in C, f(z) == z |
the complex plane |
for x in [-1, 1] \ {1}, f(x) >= 0 |
an interval with a point excluded |
for scale in {"info", "linear"}, f(r, scale) >= 0 |
a finite set of strings |
for v in R^n, f(v) >= 0 |
a real vector of length n, never empty |
for A in R^(m,n), f(A) == f(A) |
an m-by-n real matrix, rows then columns |
for c in [0, 1]^3, f(c) in [0, 1] |
a vector of exactly 3 elements, each in [0, 1]; a number written as a dimension is fixed |
for A in R^(n,3), f(A) in R^(3,3) |
a matrix with 3 columns and any number of rows; the output's space, judged by the output's shape |
for s in L[unicode], f(f(s)) == f(s) |
every string, the empty string included: a language |
for s in L[unicode] \ {""}, len(f(s)) >= 1 |
a language with the empty string excluded |
A matrix space is written R^(m,n), the order of a numpy shape. The
spellings R^{m,n}, R^(m×n), R^{m×n}, R^(m*n) and the superscript
ℝᵐˣⁿ are the same space, as are ℝ³ˣ³ and ℝ^{3×3} for a fixed size,
and all of them are written back as R^(m,n). The unicode display uses
superscripts wherever they read back as the same space; a dimension
named with an x (the superscript ˣ is the separator) or with a
letter that has no superscript form is shown as ℝ^(x,n) instead.
Over C equality and closeness are adjudicated like any other value
claim: == compares exactly and ~= compares abs(a - b) against the
same tolerance as over the reals, while an ordering (<, <=, >,
>=) of a side that reads a complex value is skipped as misspecified,
since complex numbers have no order: compare a real quantity instead,
abs(...), re(...) or im(...) (z.real, z.imag on a parameter).
This holds whether the claim writes for z in C or the parameter's
complex annotation puts it over C. The computation
companion of a claim over C runs in complex128 and is named
<claim>[complex], with corners on both axes at float64's largest
magnitude; a NaN or an infinity in either component is no value.
The excluded-point form is how you state a claim around a pole. The finite-set form is how a string-valued parameter that selects a branch becomes something the derive route can reason about, since it can then check every case rather than guessing.
L[<name>] is a language: the set of strings, or of structured
values, a name stands for, the way R is the set of reals. An
alphabet language contains the empty string, as a Kleene star does;
\ {""} removes it. The names themselves (unicode, ascii,
latin-1, json, a schema of your own) come from the
mathema-language package, installed as mathema[language]; a name
mathema cannot resolve is refused with the vocabulary, never read as a
wider set. Language domains says what a language
samples, what the record states about it, and which claims a parser
or a renderer earns over one.
Calculus¶
| Spelling | Meaning |
|---|---|
d(f(x), x) >= 0 |
first derivative |
f'(x) >= 0 |
the same thing, prime notation |
∂(f(x, y), x) == y |
partial derivative |
d(f(x, y), x, y) == 0 |
a second, mixed derivative |
d(f(x), x) @ {x = 1} == 2 |
evaluated at a point |
d(f(x), x) at {x = 1} == 2 |
the word form of the same |
lim(f(x), x, oo) == 0 |
a limit |
lim(f(x), x -> 0) == 0 |
the arrow form |
integrate(f(x), x, 0, 1) == 1 |
a definite integral |
∫(f(x), x, 0, 1) == 1 |
the symbol form |
integrate(f(x), x)|_{0}^{1} == 1 |
with an evaluation bar |
let n be [1, 20] subset Z, Sum(f(i))_{i=1}^n == n*(n+1) |
a sum, subscript form, its bound declared |
let n be [1, 20] subset Z, Prod(f(i), i, 1, n) >= 0 |
a product |
P.V.(integrate(1/(x - c), x, -1, 1)) == f(c) |
a Cauchy principal value |
Safety predicates¶
Some questions come up so often that they have names. These are facts about the computation, one implementation executed in float64, established by running the code rather than by algebra, and each answers one of three questions you have about a function.
Which question each one answers¶
Does it run on my domain? Every input the claim admits gets a value: no raise, no NaN, and no infinity from a finite input. When one of these fails, the witness names the input, the note names the call that failed, and the fix is usually one of the ones below.
| Spelling | What you learn | Usual fix |
|---|---|---|
is_number_set_safe(x) |
every restricted builtin the code calls (sqrt, log, asin, factorial, ...) gets an argument it accepts: no math.sqrt of a negative, no math.log of zero |
narrow the domain to the builtin's range, or guard the call |
is_pole_safe(x) |
the code never meets a pole, a point where the formula divides by zero or otherwise blows up (1 / (x - 1) at x = 1), anywhere in the domain |
exclude the point from the domain, or guard it with an explicit raise |
is_library_safe(numpy) |
every library call a compendium covers returns a value on the domain | keep the call's argument inside the region the compendium states |
is_overflow_safe(x) |
no result overflows to infinity and nothing raises OverflowError from a finite input, out to float64's maximum along an unbounded direction (bound it with let |inf| be ...); the restriction form (name: is_overflow_safe, statement: "x <= 709.78") states the region where the computation stays in float range |
narrow the domain below the overflow point, or rescale (work in logarithms) |
is_missing_safe(f) |
every hole a parameter admits (nan, null, NA) has a policy the code follows: it raises, drops it or gives a hole back, on purpose (missing values) |
state the policy, or guard the hole at entry |
is_absent_safe(f) |
every parameter, field or key that may be None has a policy the code follows, and a None result is declared by the return type (missing values) | state the policy, or annotate the parameter |
is_empty_safe(xs) |
an empty sequence gets an answer or a deliberate error, not an IndexError or a division by a zero length |
handle the empty case first |
is_representation_safe(x) |
one number written differently (1, 1.0, True) gets one answer |
normalize the input type at entry |
is_language_defined(s) |
over a language: every member gets an answer (a return or an exit status) and every non-member is refused; over a plain string: no input makes the function crash by accident, its exits and deliberate raises being its refusals, which the note lists | answer every member of the language; validate the rest and refuse it |
is_recursion_safe(f) |
the recursion never runs out of stack (RecursionError) over the domain; suggested when the body calls itself |
rewrite the recursion as a loop, or narrow the domain |
is_dimension_safe(f) |
every operand and the result have shapes that fit (no matmul of mismatched matrices, no result breaking its Vec/Mat marker) |
fix the shapes, or guard them with @enforce_dimensions |
is_concurrency_safe(f) |
reserved for a later release: the function runs correctly under concurrent calls |
Is the answer right in float64? The function returns, and the number it returns is the one the mathematics says.
| Spelling | What you learn | Usual fix |
|---|---|---|
is_numerically_stable |
the float64 result agrees with the exact value of the mathematics, within the claim tolerance (1e-9 plus 1e-7 times the magnitude by default), at every point tried in the working domain; stated with mathema.f.accurate, and the witness shows the exact and the float value |
reorder or rescale the arithmetic that loses the value |
<name>[float] |
the companion every proof spawns: the proven relation run in float64 at the domain's corners and inside it, falsified with a witness where the computation loses what the mathematics proves (see the evidence ladder) | fix the code, narrow the domain, or state the claim with route="derive:math_only"; where it fails along an unbounded direction, let |inf| be B is offered once a run under it holds, bounding the computation alone and never the proof |
is_precision_safe(f) |
reserved for a later release: the answer stays right in a narrower number representation (float32, say) | |
is_representation_consistent(f) |
reserved for a later release: the same answer across the computations the bracketed descriptor names |
Is it repeatable? The same call gives the same answer and leaves nothing behind.
| Spelling | What you learn | Usual fix |
|---|---|---|
is_deterministic |
the result depends on the arguments alone. mathema reads the source (and the source of every project function it reaches) and never runs it: a read of the environment, the clock, a file, a module-level value the call changes, or a draw from a shared random generator falsifies, with that read as the witness. A threaded reduction (numpy dot, matmul, @, linalg) whose rounding can depend on how its work is split, or anything mathema cannot read, leaves it unknown with the reason |
remove the hidden input (a clock, a global counter, an unseeded random draw) |
is_reproducible |
for a function that takes a seed or a generator (a parameter named seed, rng, random_state or key, or one annotated as a numpy Generator or RandomState or a random.Random), every draw comes through that parameter and nothing else the arguments do not carry is read, so the same seed gives the same answer. It is read from the source, as is_deterministic is |
draw from a generator the caller can seed |
is_state_safe |
the call changes nothing outside itself: no argument mutated, no global written, and no process state changed (the environment, the working directory, sys.path, the global random generators, logging's configuration). mathema reads the source, following aliases (ys = xs, e = os.environ) and the project functions it calls, and never runs it: a write falsifies with its site as the witness, even one in a branch the domain never reaches (the witness then says so too), and anything it cannot read (getattr, exec, a library function it has no entry for) leaves it unknown with the reason. Emitting a log record through the standard library's own logging, and drawing from a generator passed in, are not changes |
copy before modifying, and return the result instead of storing it |
is_order_invariant(f) |
reserved for a later release: the same answer whatever order a reduction runs in |
A reserved family is a known claim that is skipped in this release,
with a note saying so, and it is never suggested. A platform (a GPU, a
JIT compiler, a distributed runtime) is never part of a family name: it
is named in the bracketed computation descriptor after a claim name
([float] today), which says which computation was attempted.
The families form a tree, and a roll-up summarises its children; the
children stay individual claims. is_defined(f) (a value or a
deliberate error) has two children, is_language_defined and
is_numerically_defined; the second rolls up is_pole_safe,
is_number_set_safe and is_dimension_safe.
is_computation_safe(f) rolls up is_overflow_safe,
is_representation_safe and is_recursion_safe, and is_input_safe(f)
rolls up is_missing_safe, is_absent_safe and is_empty_safe.
is_finite_over_floats(f) is a view rather than a node: poles and
overflow together. An overflow is never a point where is_defined
finds no value, and an infinity nothing tells from an overflow (no
overflow error, no numpy flag, a body the exact reading cannot follow)
leaves is_defined unknown at that point. Each roll-up runs every child that applies to the
function and is declared by the author, never suggested; its note
names each child's verdict. A falsified child falsifies the roll-up with
that child's name and witness; the roll-up is proven when every child
is, and otherwise takes its weakest child's verdict.
is_repeatable(f) answers the repeatability question, and the seed
decides how: a function that takes a seed or a generator is held to
is_reproducible (same seed, same answer), any other to
is_deterministic (same input, same answer), and is_state_safe
always joins; it is proven when every child is, since its children are
read from the source and never sampled.
A function's own guards cut its working domain: a conditional raise,
@enforce_domain (an assert at the top of the body feeds it) and an
entry check of @enforce_dimensions reject a call on purpose, so
is_defined(f) and the families judge only the calls the guards let
through, and the record names each guard by its condition. A domain the
claim binds itself is the domain: for x in [-1, 1], is_defined(f)
states that f has a value at every point of [-1, 1], so a guard
refusing a call inside it falsifies the claim there, while
is_defined(f) with no binding reads the working domain. A bare
assert is not a guard: a failed assert counts against is_defined, and
so does a RangeError from @enforce_range (a result outside its
declared range). Nor is a nan or an infinity the body returns
(return math.nan, x if x > 0 else float("inf")): it is no value,
so it counts against is_defined as a failing call does.
The old family names is_builtin_safe, is_extremity_safe,
is_arbitrary_input_safe and is_compendium_safe are still read, as
is_number_set_safe, is_overflow_safe, is_language_defined and
is_library_safe, and the record says the spelling was accepted.
Whether a function is defined at a point (a square root of a negative, a logarithm of zero) is a question about the mathematics, the same in every language, and the derive route reasons about it directly; see conditional claims.
Partiality: claims about raising¶
Raising is behaviour, so it is claimable:
raises(f(x), ValueError)
raises(f(50, 0), ValueError)
The second form infers the domain from the literal arguments, so you do
not restate what you already wrote. The exception is a built-in name
(ValueError), a dotted path (numpy.linalg.LinAlgError), or a bare
name defined on the function's own module or a parent package
(LinAlgError for numpy.linalg.inv); a name none of these resolve
makes the claim skipped:misspecified, and the note names it. A function that raises inside a
region a claim quantifies over falsifies that claim, on either evidence
route, because a claim about a value is not satisfied by an exception.
A complex result counts as a raise. A real claim reads the function as
real-valued, and x ** 0.5 of a negative float is a complex number in
Python, not a real one:
import mathema
def half_power(x: float) -> float:
return x ** 0.5
(p,) = mathema.claims.check(half_power, [mathema.claim("f(x)^2 >= 0", route="probe")])
print(p.verdict, p.counterexample)
falsified x = -1: f returned the complex value 6.12323e-17+1j, which a real claim reads as a raise; narrow the claim's domain to where every call is real, or annotate the function complex
The derive route falsifies it too, with an executed witness. A function
annotated complex (its return or a parameter), or a claim over C,
reads a complex result as an ordinary value.
let: naming things¶
let binds a name before the claim uses it, which keeps long claims
readable and lets you talk about things that are not parameters:
| Spelling | Binds |
|---|---|
let g = math.sqrt, for x in (0,100], g(x) >= 0 |
a real function, by dotted path |
let g = budget_line, let I be [10, 1000], let px be [0.5, 20], let py be [0.5, 20], d(g(x, I, px, py), x) == -px/py |
another function in the same module, by bare name |
let c be [-1e6,1e6], for x in [0,10], f(x) + c >= 0 |
a free variable over a range |
let c be [1,100] subset integer, for x in [0,10], f(x) + c >= 0 |
a typed free variable |
let compute_square_root = numpy.sqrt, for x in [0, 100], compute_square_root(x) >= 0 |
a long name, kept readable |
for returns in [-0.1, 0.1]^n, let s = mathema.f.scale_seq, let c be [0.1, 10], assuming std(returns, ddof=1) > 0, f(s(returns, c)) ~= f(returns) |
a transform of a sequence, by dotted path: s(returns, c) scales every entry by c |
for a in [-100, 100]^n, let s = mathema.f.shift_seq, let c be [-5, 5], f(s(a, c)) == f(a) |
the shift of a sequence: s(a, c) adds c to every entry |
A function the claim names takes keyword arguments the way its own
callers pass them, each a literal or a name, and the record keeps them
as written: let g = numpy.round, for x in [0, 1], g(x, decimals=1) <= 1.
The grammar's own functions keep their fixed keywords (axis= and
ddof=). The probe route also reads str, a value's text, for a round
trip through a parser that returns an object; the derive route declines
a claim that uses it.
A free variable is the difference between "this holds for the inputs" and "this holds for the inputs and any constant you care to add", which is often the claim you actually meant.
Every name a claim uses must be declared: a parameter of the function,
a name bound by for or let, a dimension of a declared space
(n in R^n), a variable a derivative, sum, integral or limit binds,
or a known constant or function. Any other name is refused with its
name and the let ... be [...] that declares it, rather than being
sampled as a value nobody chose. A binding may continue a let run
without repeating let, so a bare name = expr straight after the run
reads as one more binding; a claim written that way is refused with a
message saying to write the relation as ==.
Pinning a parameter: let p be v¶
let followed by a parameter's own name and a literal value (a number,
None, True or False) pins that parameter: every call the claim
makes passes it at that value, whether or not the claim's text writes
it into the call. It is how a claim about a library function states a
value other than the default, since a library function's other
parameters are otherwise passed at their defaults (see
Claims transfer):
numpy.mean:
claims:
- name: one_mean_per_column
statement: "let axis be 0, for a in R^(n,n), dim(f(a)) == dim(a)"
The pin is part of the claim's canonical text, so it survives every
round trip, and the record lists it among the values held at their
defaults, axis: 0 (pinned) under numpy.mean. A pin naming something the function
does not take is a misspecified claim, never a silent free variable.
Operational infinity: let |inf| be ...¶
One more binding uses bars around the name. It sets an operational
infinity, the finite magnitude that stands in for oo wherever the
computation of a claim is exercised along an unbounded direction, and it
exists because code running on doubles does not reach infinity while the
mathematics it implements does. The binding bounds only the computation,
never the proof, which stays over the full domain: a proof is about the
mathematics, so it is over ℝ whatever the binding says, with infinity as
infinity, and the binding sets how far a proof's [float] companion and
the probe route execute. Past about 1.34e154, x ** 2
raises OverflowError, and with no operational infinity declared the
companion runs an unbounded direction out to float64's maximum
(about 1.8e308), where that
overflow shows.
The standard normal density shows both halves of the rule:
import math
import mathema
def gauss(x: float) -> float:
"""The standard normal density."""
return math.exp(-x ** 2 / 2) / math.sqrt(2 * math.pi)
for law in ["∫(f(x), x, -oo, oo) == 1",
"f(x) >= 0",
"let |inf| be 1e100, f(x) >= 0"]:
for p in mathema.check(gauss, claims=[law]).probes:
if "mathema.policy" in (p.meta or {}):
continue # what f does with a missing x, a row of its own
label = " [float]" if p.name.endswith("[float]") else law
print(f"{label:31} {p.verdict:9} {p.counterexample or p.condition or ''}")
∫(f(x), x, -oo, oo) == 1 proven
f(x) >= 0 proven ∀ x ∈ ℝ
[float] falsified x = -1.7976931348623157e+308
let |inf| be 1e100, f(x) >= 0 proven ∀ x ∈ ℝ
[float] holds
The integral over the whole line is proven, since an integral, like a
limit, is a statement about the mathematics, and so is the pointwise
claim, because the density is positive at every real x and the proof
says so over ℝ. The computation is a separate question, and the [float]
row under each proof answers it: at x = -1.79769e308 the code squares x
before it returns anything, the square overflows, and the companion is
falsified with that witness while the proof stands. Declaring let |inf|
be 1e100 says that for this claim the computation is exercised out to
1e100 in magnitude, where x ** 2 is still a finite double, so the
companion holds; the proof is the same proof over ℝ it was without the
binding, and the binding stays in the claim's statement, so a reader
sees what bounded the computation (see the evidence ladder).
mathema verify offers such a binding under a computation line that
fails along an unbounded direction, once a run of the claim under it
holds: here that is let |inf| be 1e+154, the largest power of ten
whose square is still a finite double.
A claim can also state a half-line explicitly, let |inf| be 1e12, for
x in [0, oo], f(x) >= 0, where the probe route and the companion stop
the oo endpoint at 1e12 and the proof keeps oo, so the proof's
own row quantifies over [0, oo] and the bound appears only beside the
executed evidence. Nothing in the claim refers to |inf| by name, so it
is not an ordinary binding, and in Python the same setting is
claim(..., pseudo_infinity=1e100). A binding that can bound nothing,
because every name the claim reads already has a bounded domain, is
dropped from the claim's text and so from its identity.
The claim is the first of three levels. A function's entry in a claims
file can carry a pseudo_infinity: field beside claims:, which
mathema.check(fn, pseudo_infinity=...) also sets, and a project sets
one for every function with the MATHEMA_PSEUDO_INFINITY environment
variable. The claim's own binding wins over the function level, the
function level over the project, and with none of them set the
computation runs to float64's own maximum. Only the claim's own binding
is part of the claim: the value that applied is output. Where it bounds
an unbounded direction of the claim's domain, the computation rows show
it as a plain binding in front of their condition (let |inf| be
1e+100, for x in R), whichever level it came from, and the level is
recorded in meta["mathema.pseudo_infinity"]; mathema verify treats a change in it as a stale record, not a
different claim. A claim whose every direction is bounded says nothing
about infinity at any level:
import math
import sys
import mathema
def gauss(x: float) -> float:
"""The standard normal density."""
return math.exp(-x ** 2 / 2) / math.sqrt(2 * math.pi)
level = float(sys.argv[1]) if len(sys.argv) > 1 else None
for law in ["f(x) >= 0", "for x in [-3, 3], f(x) >= 0"]:
rows = mathema.check(gauss, claims=[law], pseudo_infinity=level).probes
companion = rows[-1]
reach = [part for part in companion.note.split("; ")
if part.startswith("unbounded")]
print(f"{law:27} [float] {companion.verdict:9} "
f"{companion.meta.get('mathema.pseudo_infinity')}")
print(f" {reach[0] if reach else '(every direction bounded)'}")
MATHEMA_PSEUDO_INFINITY=1e100 python levels.py
MATHEMA_PSEUDO_INFINITY=1e100 python levels.py 1e50
f(x) >= 0 [float] holds None
(every direction bounded)
for x in [-3, 3], f(x) >= 0 [float] holds None
(every direction bounded)
f(x) >= 0 [float] holds None
(every direction bounded)
for x in [-3, 3], f(x) >= 0 [float] holds None
(every direction bounded)
The value a project sets hides every overflow beyond it, so mathema
verify and mathema check warn once on stderr when
MATHEMA_PSEUDO_INFINITY is below 1e100: values beyond it are not
checked for computation, and an explicit domain for the variables
(for x in [lo, hi], ...) is usually the better way to say the same
thing, since it is part of the claim a reader sees. The probe route reads the same value: an unbounded
direction, declared (for x in [0, oo), for x in R) or a parameter
with no domain at all, is exercised with finite values only. Nine draws
in ten stay at everyday magnitudes (the special values near zero first,
then modest ranges), and one in ten goes toward the reach: the value
that applied, or else float64's maximum (sys.float_info.max), spread
over the decades so the far end is reached. A real domain contains no
infinity, so the probe never calls the code at inf itself.
assuming: stating a premise¶
assuming says what the claim takes for granted, which is how a claim
that is only true in part of the input space stays honest without being
watered down:
| Spelling | Assumes |
|---|---|
assuming k != 0, f(x, k) == x/k |
a simple side condition |
assuming b^2 - 4*a*c >= 0.01, for a in [1,10], b in [-10,10], c in [-10,10], d(f(a,b,c), c) <= 0 |
an inequality over the parameters |
assuming real_roots, for a in [1,10], b in [-10,10], c in [-10,10], d(f(a,b,c), c) <= 0 |
another claim, by name |
assuming grows holds, for x in [0,10], f(x) == 2*x |
that claim reached at least holds |
assuming base_case is proven, for n in [2, 30] subset Z, f(n) == f(n-1) + f(n-2) |
that claim reached proven specifically |
assuming is_defined(f), for w in [-50, 50], f(F0,k,m,-w,c) == f(F0,k,m,w,c) |
that the function is defined there at all |
assuming f is defined, for w in [-50, 50], f(F0,k,m,-w,c) == f(F0,k,m,w,c) |
the postfix spelling of the same |
assuming n >= 5, for xs in R^n, f(xs) == xs[4] |
a vector at least five long |
assuming n >= 3, for a in R^(n,n), f(a) == a[2][2] |
a square matrix at least 3 by 3 |
assuming min(m, n) >= 3, for a in R^(m,n), f(a) == a[2][2] |
a rectangular matrix with at least three rows and three columns |
assuming dim(returns) >= 2, for returns in [-0.1, 0.1]^n, f(returns) >= 0 |
a vector at least two long, by the parameter's dim |
for returns in [-0.1, 0.1]^n, assuming std(returns, ddof=1) > 0, is_defined(f) |
a statistic of the vector; the premise's std is computed exactly, so a constant vector is outside |
A vector or matrix space is never empty, since R^n already means at
least one element, so a dimension premise is needed only for a bound
beyond that. Two assuming clauses in one claim are one premise, their
conjunction: assuming m >= 3, assuming n >= 3, ... is stored as
assuming m >= 3 and n >= 3, .... Only relations are joined this way;
a definedness, lemma or matrix structure premise is written as one
clause of its own.
The f is defined premise is how compositional claims are built:
prove that a function is defined on a region, then assume it in the
claims that depend on it, and the record keeps the dependency.
Several functions in one claim¶
f is the function under test, but it is not the only one you can
mention:
f(x) == g(x)
let I be [10, 1000], let px be [0.5, 20], let py be [0.5, 20], d(budget_line(x, I, px, py), x) == -px/py
let g = budget_line, let I be [10, 1000], let px be [0.5, 20], let py be [0.5, 20], d(g(x, I, px, py), x) == -px/py
Inputs of the second function that are not parameters of f (here the
income and the two prices) are declared with let, like any other name.
A second function named this way is a full participant, lifted and
reasoned about like f rather than treated as an opaque call.
Outcome references¶
f(x) > 0 => self.stays_positive
This names a sibling claim that should follow when this one holds, so
a claim can point at the vocabulary your codebase already uses. The
clause is parsed and kept verbatim in the record, but it is not
adjudicated: nothing derives the named outcome from it yet. When one
claim must actually rest on another, use an assuming premise, as
Conditional claims and lemmas describes.
Recurrences¶
for n in [2, 30] subset Z, f(n) == f(n-1) + f(n-2)
A self-recursive linear recurrence over one scalar parameter is solved
to its closed form rather than unrolled, so a Fibonacci-shaped function
can reach proven over a stated integer range. See the derive
route for the exact shapes this covers.
Routes¶
A claim's route says which evidence it accepts, and it is set beside
the claim text (route= in Python, route: in a claims file), never
inside it. The default, best, attempts a proof and falls through to
running the code when the proof cannot settle the claim, so a sampled
holds can stand in for a proof that did not close. probe runs the
code only. derive asks for derive's verdict: when the proof cannot
settle the claim the probe still samples it, but only a counterexample
it executes counts, and the claim is then falsified on the probe's
route with derive's reason in the note. A float miss or an overflow at
a point where the claim read exactly holds is no counterexample: the
note records it as a finding about the computation. An infinity at a
point with no exact reading is no counterexample either, since an
overflow and a pole cannot be told apart there. A NaN, a hole, or a
plain miss at a point with no exact reading still falsifies. Draws that
find no counterexample leave the claim unknown, never holds. Over a
finite domain, a sweep that runs every point and finds the claim exact
at each is proven on derive:brute_force; a sweep that passes only
inexactly, or runs part of the domain, leaves the claim unknown on
this route. The one holds on this route is a sweep that runs every
point and finds the claim exact at each over a function the examination
cannot show pure: it is holds on derive:brute_force, and the note
names what stops the proof and what would make the sweep one. A proof's
[float] companion and a disproof's executed witness are the same on
every route. On every route, a miss found by sampling derive's own
reconstruction of the function (probe:lifted_numeric, for a claim the
code cannot evaluate, such as a derivative or an integral) falsifies the
claim only where the code, run at that point, fails the relation
exactly; otherwise the claim is unknown, the note naming the point and
why it is no witness. See Verdicts and exit codes.
When a claim will not parse¶
mathema check reports an unparseable claim as a clean error naming
the part it could not read, and exits 2 rather than 1, because nothing
was adjudicated.
If you are working through an agent, the MCP surface exposes the same
check as a parse_claim tool so a claim can be validated before paying
for a full adjudication. See the MCP interface.