1

Cartesian_Euclidean_Space在（HOL/Multivariate_Analysis 目录中）有一个矩阵乘法定义：

definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m ⇒ 'a ^'p^'n ⇒ 'a ^ 'p ^'m"
    (infixl "**" 70)
  where "m ** m' == (χ i j. setsum (λk. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"

现在平方矩阵将是A ** A和 A^3 将是A ** A ** A。

我找不到要定义的幂函数A^n （即A ** A ** ... ** An 次）。

库中是否有幂函数？需要手动定义吗？

4

1 回答 1

0

我在中找到了以下定义HOL/Power.thy：

primrec power :: "'a ⇒ nat ⇒ 'a" (infixr "^" 80) where
    power_0: "a ^ 0 = 1"
  | power_Suc: "a ^ Suc n = a * a ^ n"

（Control + Click 让你得到相应的定义！所以我点击了“^”，我只是先写了“1 ^ 1 = 1”作为引理。

这是矩阵幂的定义。（因为我只使用方阵这很好，但更一般的类型^'n^'m会很好。）

primrec powerM :: "(('a::semiring_1) ^'n^'n) ⇒ nat ⇒ (('a::semiring_1) ^'n^'n)" 
(infixr "^^^" 80) where
  powerM_0: "A ^^^(0::nat) = mat 1"
| powerM_Suc: "A ^^^(Suc n) = A ** (powerM A n)"
于 2013-11-27T11:33:38.687 回答