matching_step

std.linalg.matching_step · Level L3

One move of a backtracking search for a matching of ν edges: vertex p takes its next choice, a later free neighbour as its partner or, last, no partner of its own. A vertex an earlier one took has only that last choice. Leaving p unmatched is allowed only while at most n − 2ν vertices stay unmatched. Past the last choice, clear p and step back; on a choice not allowed, try the next; otherwise go on to p + 1. The body of max_matching's second loop.

choice(p) ← next; none left: back; not allowed: stay; else: p + 1

Signature

matching_step(p: f64[], ch: f64[n], A: f64[n, n], nu: f64[]) → f64[], f64[n]

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 the same move on Python lists in exact rational arithmetic, on all 40 test cases.
All 189 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

max_matching

sha256:20875c09ce04f1274ba94600937614c610a003d07a35410273aad586868c2563

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

Control handle

Symbol: Ω:std.linalg.matching_step · Ω:matching_step
Pins: sha256:1db074e2ba636c865b38c696d447c473637bf503119c2e023c28e5c45a7bd745this graph alone
Evidence: sha256:59631b11ed8dc3012a17a5f4ebc3700572bb6b2322ed11be5cb0edb257c803fbthe 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.