Executable matrix evaluation and finite tests

Rational formulas are evaluated on square rational matrices by the native formula evaluation Cslib.Circuits.Formula.eval under an interpretation in Option (Mat d), which rejects a singular operand at every inverse node and otherwise inverts it exactly through the adjugate. Partiality here is the computable stand-in for the relational semantics Formula.Eval, to which it is proved equal in Cslib.Circuits.Rational.Formula.evalMatrix?_eq_some_iff. The finite tests inspect the exact rational matrix values on a list; their correctness does not assert a bit-time bound.

Main definitions

• Cslib.Circuits.Rational.matrixInterpretation: the partial interpretation on rational matrices.
• Cslib.Circuits.Rational.Formula.evalMatrix?: executable evaluation on a matrix tuple.
• Cslib.Circuits.Rational.Output.admissibilityTest, Cslib.Circuits.Rational.Output.nonzeroTest: search a list for a defined, respectively an invertible, value.

Main results

• Cslib.Circuits.Rational.Formula.evalMatrix?_add and its siblings: the executable evaluation unfolds along the constructors.

References

• From the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787 (file Complexitylib/RationalHitting/Evaluation/Defs.lean), built on OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.

def Cslib.Circuits.Rational.matrixInterpretation (d : ℕ) : Interpretation ratSignature (Option (Mat d))

The partial interpretation of the rational operations on d × d rational matrices: an inverse node is undefined at a singular operand, and otherwise takes the exact inverse det⁻¹ • adjugate.

def Cslib.Circuits.Rational.Formula.evalMatrix? {n d : ℕ} (f : Formula n) (X : Tuple n d) : Option (Mat d)

Compute a matrix value, rejecting a singular operand at every inverse node.

@[simp]

theorem Cslib.Circuits.Rational.Formula.evalMatrix?_var {n d : ℕ} (i : Fin n) (X : Tuple n d) : (var i).evalMatrix? X = some (X i)

@[simp]

theorem Cslib.Circuits.Rational.Formula.evalMatrix?_const {n d : ℕ} (q : ℚ) (X : Tuple n d) : (const q).evalMatrix? X = some ((algebraMap ℚ (Mat d)) q)

@[simp]

theorem Cslib.Circuits.Rational.Formula.evalMatrix?_add {n d : ℕ} (f g : Formula n) (X : Tuple n d) : (f.add g).evalMatrix? X = do let a ← f.evalMatrix? X let b ← g.evalMatrix? X pure (a + b)

@[simp]

theorem Cslib.Circuits.Rational.Formula.evalMatrix?_mul {n d : ℕ} (f g : Formula n) (X : Tuple n d) : (f.mul g).evalMatrix? X = do let a ← f.evalMatrix? X let b ← g.evalMatrix? X pure (a * b)

@[simp]

theorem Cslib.Circuits.Rational.Formula.evalMatrix?_inv {n d : ℕ} (f : Formula n) (X : Tuple n d) : f.inv.evalMatrix? X = do let v ← f.evalMatrix? X if Matrix.det v = 0 then none else some ((Matrix.det v)⁻¹ • Matrix.adjugate v)

def Cslib.Circuits.Rational.Output.admissibilityTest {n : ℕ} (H : Output n) (f : Formula n) : Bool

Test whether at least one tuple belongs to the formula's domain.

def Cslib.Circuits.Rational.Output.nonzeroTest {n : ℕ} (H : Output n) (f : Formula n) : Bool

Test whether at least one tuple yields an invertible matrix value.