@@ -5,17 +5,15 @@ import Data.ZZ
6%default total
6%default total
9−infixr 2 <.> -- Vector inner product
8+infixr 2 <.> -- vector inner product
10−infixr 2 >< -- Vector outer product
9+infixr 2 >< -- vector outer product
11−infixr 2 <<>> -- Matrix commutator
10+infixr 2 <<>> -- matrix commutator
12−infixr 2 >><< -- Matrix anticommutator
11+infixr 2 >><< -- matrix anticommutator
13−infixl 3 <\> -- row times a Matrix
12+infixl 3 <\> -- row times a matrix
14−infixr 4 </> -- Matrix times a column
13+infixr 4 </> -- matrix times a column
15−infixr 5 <> -- Matrix multiplication
14+infixr 5 <> -- matrix multiplication
16infixr 7 \&\ -- vector tensor product
15infixr 7 \&\ -- vector tensor product
17−infixr 7 <&> -- Matrix tensor product
16+infixr 7 <&> -- matrix tensor product
20-----------------------------------------------------------------------
18-----------------------------------------------------------------------
21-- Vectors as members of algebraic classes
19-- Vectors as members of algebraic classes
@@ -41,24 +39,17 @@ instance RingWithUnity a => RingWithUnity (Vect n a) where
41instance Field a => Field (Vect n a) where
39instance Field a => Field (Vect n a) where
42 inverseM = map inverseM
40 inverseM = map inverseM
44−instance (Field a, AbelianGroup a) => VectorSpace a (Vect n a) where
42+instance RingWithUnity a => Module a (Vect n a) where
45− (<#>) s v = map (s <*>) v
43+ (<#>) r v = map (r <*>) v
47−instance (Field a, AbelianGroup a) => VectorSpace a (Vect n (Vect n a)) where
48− (<#>) s m = map (s <#>) m
50-----------------------------------------------------------------------
45-----------------------------------------------------------------------
51−-- (Ring) Vector functions
46+-- (Ring) Vector functions
52-----------------------------------------------------------------------
47-----------------------------------------------------------------------
54||| Inner product of ring vectors
49||| Inner product of ring vectors
55(<.>) : Ring a => Vect n a -> Vect n a -> a
50(<.>) : Ring a => Vect n a -> Vect n a -> a
56(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
51(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
58−||| Scale a ring vector by the appropriate scalar
59−scale : Ring a => a -> Vect n a -> Vect n a
60−scale s v = map (<*> s) v
62||| Tensor multiply (⊗) ring vectors
53||| Tensor multiply (⊗) ring vectors
63(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
54(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
64(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
55(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
@@ -73,18 +64,18 @@ basis i = replaceAt i unity $ neutral
75-----------------------------------------------------------------------
66-----------------------------------------------------------------------
76−-- Matrixrix functions
67+-- Matrix functions
77-----------------------------------------------------------------------
68-----------------------------------------------------------------------
79||| Matrix with n rows and m columns
70||| Matrix with n rows and m columns
80Matrix : Nat -> Nat -> Type -> Type
71Matrix : Nat -> Nat -> Type -> Type
81Matrix n m a = Vect n (Vect m a)
72Matrix n m a = Vect n (Vect m a)
83−||| Gets the specified column of a Matrix. For rows use the vector function 'index'
74+||| Gets the specified column of a matrix. For rows use the vector function 'index'
84getCol : Fin m -> Matrix n m a -> Vect n a
75getCol : Fin m -> Matrix n m a -> Vect n a
85getCol fm q = map (index fm) q
76getCol fm q = map (index fm) q
87−||| Deletes the specified column of a Matrix. For rows use the vector function 'deleteAt'
78+||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
88deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
79deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
89deleteCol f m = map (deleteAt f) m
80deleteCol f m = map (deleteAt f) m
@@ -92,14 +83,6 @@ deleteCol f m = map (deleteAt f) m
92indices : Fin n -> Fin m -> Matrix n m a -> a
83indices : Fin n -> Fin m -> Matrix n m a -> a
93indices f1 f2 m = index f2 (index f1 m)
84indices f1 f2 m = index f2 (index f1 m)
95−||| Ring scalar times a Matrix
96−RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
97−RescaleBy.(*) s m = map (map (s <*>)) m
99−||| Rescale Matrix by a ring scalar
100−RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
101−RescaleMatrix.(*) m s = map (map (<*> s)) m
103||| Matrix times a column vector
86||| Matrix times a column vector
104(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
87(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
105(</>) m v = map (v <.>) m
88(</>) m v = map (v <.>) m
@@ -108,13 +91,13 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
108(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
91(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
109(<\>) r m = map (r <.>) $ transpose m
92(<\>) r m = map (r <.>) $ transpose m
111−||| Matrix Multiplication
94+||| Matrix multiplication
112(<>) : Ring a => Matrix n k a ->
95(<>) : Ring a => Matrix n k a ->
113 Matrix k m a ->
96 Matrix k m a ->
114 Matrix n m a
97 Matrix n m a
115(<>) m1 m2 = map (<\> m2) m1
98(<>) m1 m2 = map (<\> m2) m1
117−||| Tensor multiply (⊗) for ring Matrixrices
100+||| Tensor multiply (⊗) for ring matrices
118(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
101(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
119(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
102(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
120 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
103 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
@@ -122,11 +105,11 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
122 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
105 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
123 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
106 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
125−||| Cast a vector from a standard Vect to a proper n x 1 Matrix
108+||| Cast a vector from a standard Vect to a proper n x 1 matrix
126col : Vect n a -> Matrix n 1 a
109col : Vect n a -> Matrix n 1 a
127col v = map (\x => [x]) v
110col v = map (\x => [x]) v
129−||| Cast a row from a standard Vect to a proper 1 x n Matrix
112+||| Cast a row from a standard Vect to a proper 1 x n matrix
130row : Vect n a -> Matrix 1 n a
113row : Vect n a -> Matrix 1 n a
131row r = [r]
114row r = [r]
@@ -139,15 +122,15 @@ allN : (n : Nat) -> Vect n (Fin n)
139allN Z = Nil
122allN Z = Nil
140allN (S n) = FZ :: (map FS $ allN n)
123allN (S n) = FZ :: (map FS $ allN n)
142−||| Identity Matrix
125+||| Identity matrix
143Id : RingWithUnity a => {d : Nat} -> Matrix d d a
126Id : RingWithUnity a => {d : Nat} -> Matrix d d a
144Id {d} = map (\n => basis n) $ allN d
127Id {d} = map (\n => basis n) $ allN d
146−||| Matrix Commutator
129+||| Matrix commutator
147(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
130(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
148(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
131(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
150−||| Matrix Anti-Commutator
133+||| Matrix anti-commutator
151(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
134(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
152(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
135(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
@@ -157,7 +140,7 @@ Id {d} = map (\n => basis n) $ allN d
157-----------------------------------------------------------------------
140-----------------------------------------------------------------------
160−-- TODO: Prove properties of Matrix algebra for 'Verified' algebraic classes
143+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
162-----------------------------------------------------------------------
145-----------------------------------------------------------------------
163-- Numberic data types as rings
146-- Numberic data types as rings