Executable matrix evaluation and finite tests

Every inverse node requires a nonsingular operand. The finite tests inspect exact rational matrix values; their correctness does not assert a bit-time bound.

def Complexity.RationalHitting.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.

Equations

• (Complexity.RationalHitting.Formula.var i).evalMatrix? X = some (X i)
• (Complexity.RationalHitting.Formula.const a).evalMatrix? X = some ((algebraMap ℚ (Complexity.RationalHitting.Mat d)) a)
• (f_2.add g).evalMatrix? X = do let a ← f_2.evalMatrix? X let b ← g.evalMatrix? X pure (a + b)
• (f_2.mul g).evalMatrix? X = do let a ← f_2.evalMatrix? X let b ← g.evalMatrix? X pure (a * b)
• f_2.inv.evalMatrix? X = do let a ← f_2.evalMatrix? X if Matrix.det a = 0 then none else some ((Matrix.det a)⁻¹ • Matrix.adjugate a)

def Complexity.RationalHitting.Output.admissibilityTest {n : ℕ} (H : Output n) (f : Formula n) : Bool

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

Equations

• H.admissibilityTest f = H.tuples.any fun (X : Complexity.RationalHitting.Tuple n H.dimension) => (f.evalMatrix? X).isSome

def Complexity.RationalHitting.Output.nonzeroTest {n : ℕ} (H : Output n) (f : Formula n) : Bool

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

Equations

• One or more equations did not get rendered due to their size.