relation_properties

std.sets.relation_properties · Level L2

Four properties of a relation R on a finite set (an n × n 0/1 matrix), each checked over every element, pair or triple, as 1 or 0: reflexive (x R x for all x), symmetric (x R y ⇒ y R x), transitive (x R y and y R z ⇒ x R z, checked as R∘R ⊆ R), and antisymmetric (x R y and y R x ⇒ x = y). One counterexample disproves the property it violates.

xRx; xRy ⇒ yRx; xRy ∧ yRz ⇒ xRz; xRy ∧ yRx ⇒ x = y

Signature

relation_properties(R: f64[n, 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 every element, pair and triple in Python 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

equivalence_classes

sha256:a44ed428ff480862dc725729b1aa8996444d245ca82207880ec9eca82cc53768

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

Control handle

Symbol: Ω:std.sets.relation_properties · Ω:relation_properties
Pins: sha256:b2b734c02e6ade1f146ad76909e635b83aac163aece499da3b966db400fc4b0cthis graph alone
Evidence: sha256:a3e48a47fc66fe31b88dee9586073d75009657c7ac8efd473bf3e1d5f1c9041athe 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.