3.1. Object implementation using Array-backed vectors
This implementation implement's Bird's algorithm using matrices represented by Array-backed vectors.
namespace BirdDet
open Matrix
variable
{R : Type*} [CommRing R]
/-- A Matrix instantiated using Array-backed Vectors -/
abbrev VecMatrix (R : Type*) (n : ℕ) := Vector (Vector R n) n
namespace VecMatrix
def ofMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : VecMatrix R n :=
Vector.ofFn fun i => Vector.ofFn fun j => A i j
def mul {n : ℕ} (A B : VecMatrix R n) : VecMatrix R n :=
Vector.ofFn fun i =>
Vector.ofFn fun j =>
∑ k : Fin n, A[i][k] * B[k][j]
/-- The `μ` function from Bird's paper -/
def μ {n : ℕ} (A : VecMatrix R n) : VecMatrix R n :=
Vector.ofFn fun i =>
let diag := - ∑ k, if i < k then A[k][k] else 0
Vector.ofFn fun j =>
if j < i then 0
else if i = j then diag
else A[i][j]
/-- `F^{n - 1} A` from Bird's paper -/
def iterF {n : ℕ} (A : VecMatrix R n) : ℕ → VecMatrix R n → VecMatrix R n
| 0, X => X
| k + 1, X => mul (μ (iterF A k X)) A
end VecMatrix
/-- Extraction of `det A` using Theorem 1 of Bird's paper -/
def birdDet {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : R :=
let absDet :=
match n with
| 0 => 1
| k + 1 =>
let va := VecMatrix.ofMatrix A
(VecMatrix.iterF va k va)[0][0]
(-1 : R) ^ (n - 1) * absDet
end BirdDet
3.1.1. Examples
Some examples of using the birdDet function
def m2 : Matrix (Fin 2) (Fin 2) ℤ :=
!![ 1, 2;
3, 4]
def m3 : Matrix (Fin 3) (Fin 3) ℤ :=
!![ 1, 2, 3;
4, 5, 6;
7, 8, 9]
def m8 : Matrix (Fin 8) (Fin 8) ℤ :=
!![ 2, 0, -1, 0, 0, 0, 0, 0;
0, 2, 0, -1, 0, 0, 0, 0;
-1, 0, 2, -1, 0, 0, 0, 0;
0, -1, -1, 2, -1, 0, 0, 0;
0, 0, 0, -1, 2, -1, 0, 0;
0, 0, 0, 0, -1, 2, -1, 0;
0, 0, 0, 0, 0, -1, 2, -1;
0, 0, 0, 0, 0, 0, -1, 2]
def m10 : Matrix (Fin 10) (Fin 10) ℤ :=
!![ 2, 0, 2, 0, 2, 2, -2, 0, 1, 0;
2, -2, 0, -2, 1, -2, 0, -1, -1, 1;
0, 0, -2, -2, -2, 0, -1, 2, -1, 1;
-2, -1, 0, 2, 0, 2, -2, -2, -2, 0;
2, -2, -1, 1, 2, 1, 1, 1, -1, 0;
-2, 2, -2, -1, -1, -2, -2, 2, 2, 0;
0, 1, 2, 1, 0, 0, 1, 0, -1, -1;
1, 0, 0, 1, 2, -2, 0, -1, 0, 2;
-1, 1, -1, 0, 2, 2, -1, 1, -1, 2;
-2, 1, 1, 1, 0, 2, 1, -2, 1, 0]
#eval birdDet m2
#eval birdDet m3
#eval birdDet m8
#eval birdDet m10