Multi-function claims

Most claims speak about one function, spelled f. A claim may also bind further function symbols and state laws that relate them: a composition against a library function, a comparison against a sibling in the same module, or full behavioural equivalence between two implementations.

Binding a second function

Three spellings, from most to least explicit:

let g = math.sqrt, for x in (0, 100], g(x) >= 0

The let spelling binds g to an importable function by its dotted path and is the form the record keeps: it survives every store round trip, because the path is text.

mathema.check(mine, claims=[mathema.claims.claim("f(x) == g(x)", funcs={"g": other})])

funcs= on claim() binds a live callable and adjudicates identically. When the callable is a module-level function importable by its own dotted path, the record stores the binding in the let spelling (let g = mymodule.other, f(x) = g(x)), so the claim rebuilds from the record alone. A callable with no such path (a lambda, a nested function, a function defined in __main__) has no text spelling: the record keeps the law but not the binding, and a later run reconstructing the claim from the record cannot re-bind g.

A bare call name (g(x) with no let and no funcs=) binds automatically when a function of that name is defined in f's module or the calling scope. The record keeps the bare name, which binds the same way again from f's module; a function found only in the calling scope (a notebook cell, a script) is not there for a later run to find.

Laws over two functions

Once bound, the second symbol participates like any expression:

for x in [0, 4], f(x) == g(x) + 1
for x in [1, 8], f(g(x)) >= 0

Both routes handle these: derive substitutes each function's lifted body and decides the combined expression; probe executes both real functions on shared draws.

Behavioural equivalence

f =:= g
f equiv g

The equivalence relation asks whether two implementations are the same mathematics, which is the question behind every rewrite, refactor and port: an agent's new version against the one it replaces, or another runtime's implementation against the Python reference. Between two Python functions the claim records two lines, as a value claim does, and it is falsified when either line is.

The mathematics line is derive's, and it climbs a ladder, strongest rung first, where each rung may decline:

1. Identical canonical form. Both functions lift to the same alpha-renamed shape, and the claim is proven by the form hash alone: two spellings of one computation.
2. Symbolic difference. The two lifts, positionally aligned, subtract to zero under the declared domain. Where both sides raise, this rung proves the equivalence when they raise the same exception on exactly the same region and their lifts agree everywhere else (for a function of one parameter). A disproof stands once both functions, run at derive's witness and compared exactly, disagree there, however small the difference, so sqrt(x) against sqrt(x) + 1e-12 is falsified on this line although no float tolerance would notice the gap; a disproof that exact evaluation does not confirm is unknown, with the flag that marks a likely mathema bug.
3. Closed forms. Where both bodies provably never raise, their closed forms are compared directly.

The computation line, the row NAME[float] under the claim, runs both real functions on the same 96 seeded draws from the declared domain, and at least 24 of them must agree before it holds. Two results agree within the claim's own tolerance, so an equivalence between a float and a fixed-point implementation is stated, not guessed. A draw where both sides raise the same exception agrees, and so does a draw where both sides overflow to the same infinity. A NaN computed from non-missing inputs is no value and agrees with nothing, another NaN included, and an infinity disagrees with a value or with the opposite infinity: each is a counterexample. A draw with a missing input, or where either side returns something non-numeric, is not compared, and both kinds of uncompared draw are counted in the record rather than dropped. Sampling never proves, so the line's ceiling is holds.

The two lines answer different questions, and they can disagree: (x + 1e20) - 1e20 against x over [0, 1] is proven on the mathematics line and falsified on the computation, since in float64 the large sum swallows x. When derive cannot decide (a function with no source to read, a body it cannot lift, or a difference it cannot settle), there is no mathematics line, and the shared draws are the claim's only row, a computation line, exactly as the probe's row is for a value claim.

f =:= g claims f(x) == g(x) at every point of the domain, so a point where one side raises and the other returns a value is a counterexample, and the executed raise is its witness. x / x and 1.0 agree everywhere except x = 0, and both lines find it:

import mathema


def ratio(x: float) -> float:
    return x / x


def one(x: float) -> float:
    return 1.0

for p in mathema.claims.check(ratio, [mathema.claim("f =:= g", funcs={"g": one})]):
    print(p.name, p.verdict, p.counterexample)

f_equiv_g falsified x = 0: f raised ZeroDivisionError, g returned 1
f_equiv_g[float] falsified x = 0: f raised ZeroDivisionError, g returned 1

=:= compares behaviour, so a point where both sides raise the same exception type is a point where they agree: 1 / x and 2 / (2 * x) are proven equivalent over [-1, 1], both raising ZeroDivisionError at x = 0. Different exception types at the same point are a disagreement, and the executed pair is the witness: against a version that raises ValueError at zero, the claim is falsified with x = 0: f raised ZeroDivisionError, g raised ValueError. A complex result from one side counts as a raise, unless that side is annotated complex or the claim is over C.

A tolerance applies to the computation line alone, since the mathematics line is exact whatever the tolerance: x + 1e-3 =:= x with a tolerance of 1e-2 is falsified there while its computation holds. With no tolerance declared, each of the two computed values may miss the exact one by the allowance every computation line uses (1e-7 of its magnitude plus a small absolute part, at most 1e-9), and the two are added, so they may differ by about 2e-7 times the larger magnitude plus 2e-9; below magnitudes of 1e-2 the absolute part shrinks with the values, so two values near 1e-3 apart by 1e-9 disagree. To judge the computation by another rule, declare one: a bare number is an absolute allowance that replaces the default whole, and a kind ({abs: x}, {rel: x} or {ulp: n}, each with an optional floor: x that adds to it, as Tolerance kinds describes) is judged at each pair of values. The record shows the tolerance as written. A rate that runs 1e-8 high is falsified on the mathematics line under every tolerance, and its computation line follows the rule declared:

import mathema


def rate(x: float) -> float:
    return x * (1 + 1e-8)


def reference(x: float) -> float:
    return x

for tolerance in [None, 1e-9, {"rel": 1e-9}, {"rel": 1e-7}]:
    rows = mathema.claims.check(rate, [mathema.claim(
        "for x in [1, 2], f =:= g", funcs={"g": reference},
        tolerance=tolerance)])
    print(f"{str(tolerance):14}", [(p.name, p.verdict) for p in rows])

None           [('f_equiv_g', 'falsified'), ('f_equiv_g[float]', 'holds')]
1e-09          [('f_equiv_g', 'falsified'), ('f_equiv_g[float]', 'falsified')]
{'rel': 1e-09} [('f_equiv_g', 'falsified'), ('f_equiv_g[float]', 'falsified')]
{'rel': 1e-07} [('f_equiv_g', 'falsified'), ('f_equiv_g[float]', 'holds')]

Agreement within a tolerance is a different claim, f(x) ~= g(x), and accepting such a falsification as a discovery (mathema accept KEY NAME --as discovery) offers it at the tolerance the computation compared under: a declared number or kind as written, or, with none declared, {rel: 2e-7, floor: 2e-9}, which is the default exactly for values of magnitude 1e-2 and above and slightly wider below. It is written only when it holds or is proven. Either way the whole claim retires with both its lines: the computation row alone is never accepted, since the computation is what runs.

The record annotates both sides' structural complexity, so an equivalence between a one-liner and a loop reads as what it is.

Another language on the other side

What an equivalence licenses, and what it never does, is the subject of Claims transfer. How an implementation in another language is reached is a target resolver, an extension point that maps a key such as cpp: or ts: to a callable.

Because g may be any callable, the other implementation need not be Python. The ladder above compares two Python forms, so it runs only when the Python frontend read both sides. When either side's facts came from another frontend, as for a function a runtime adaptor serves, f =:= g is answered by the equivalence family: a claim family registered under the name equivalence, which can bring that runtime's own reading of a refusal, a tolerance and a region. With no such family, or one that declines, the claim is skipped with the reason equivalence across runtimes needs the equivalence family. Whatever the family finds, safety claims never transfer between implementations, because they are facts about an implementation and its language rather than about the mathematics.

Premises over bound functions

The assuming machinery composes with bindings: a premise may reference the bound function's own claims, and the definedness machinery reads registered partiality lemmas for functions the body calls (see Conditional claims and lemmas).