quantifiers

std.sets.quantifiers · Level L2

Quantifiers over a finite domain U, for a predicate given by its truth values P(x): ∀x P(x) and ∃x P(x), each as 1 or 0; whether a counterexample to ∀x P(x) exists, and the first one (0 when there is none). One counterexample refutes the universal statement; failing to find one proves it only because the domain is finite and was checked completely. ¬∀x P(x) ⇔ ∃x ¬P(x).

∀x P(x), ∃x P(x), ¬∀x P(x) ⇔ ∃x ¬P(x)

Signature

quantifiers(p: f64[n]) → f64[], f64[], f64[], f64[]

Structure

The function as NOVA stores it: one box per input, operation and output, and arrows that carry values. A double border marks another library function this one runs — called once, or by Scan once per element; select it to open that function.

input
operation
constant
call
output

Verification

Signature proven by NOVA’s shape solver, for every size.
Equal to the reference all, any, and the first false in exact rational arithmetic, on all 40 test cases.
All 160 float64 results are exact: the error is zero.
Interpreter and NumPy backend return bit-identical results.
At float32 too: the 40 test cases rounded to float32, and 40 of them exact, with zero error.

Accuracy in detail

correctly rounded (the float64 nearest the exact value): 100%
bit-equal to the NumPy formula in float64: 100%
largest error, in units in the last place: 0

Identity

Calls

—

Called by

—

sha256:95d9d37ab0d6877fe110edc0f460fcc8ee1934b03d80fe349a1ee01d8c2c076d

The semantic hash of the graph. It changes when the program changes, and never when only its documentation does.

Control handle

Symbol: Ω:std.sets.quantifiers · Ω:quantifiers
Pins: sha256:ca99b42453a2728ec66a33363e36ad65afbda24e9143125dd27499f7130e3108this graph alone
Evidence: sha256:ee1d4bdba4c855cb6f5c906369da4f4d686a88498acc8c8a57496bde2d3c61ecthe hash of its verification record
Needs: no capability: a pure function

Through NOVA’s control layer, the symbol launches this function only while the program still matches what it pins: a change to this graph, or to any graph it reaches, needs a migration first.