Page 324 - 《软件学报》2021年第6期

1898 Journal of Software 软件学报 Vol.32, No.6, June 2021

函数,而非分块矩阵转置函数.具体如下.
Definition mmat_mul_mat {m2 n2 p2:nat} (left:Mat (Mat A m n) m2 n2) (right:Mat (Mat A n p) n2 p2):=
let l1:=mat (Mat A m n) m2 n2 left in
let right′:=trans (Mat A n p) (MO A Zero n p) right in
let l2:=mat (Mat A n p) p2 n2 right′ in
mdl_mul_dl l1 l2.
此处使用普通矩阵转置函数的原因在于:我们在每个内部分块做矩阵相乘时会进行对第 2 个矩阵进行转
置操作,而当我们使用分块矩阵的转置函数,则会使得其内部分块也进行转置,这两个操作在对内部分块的转置
操作重复.对于一个分块矩阵内部分块大小为 m×n,则要求其相乘分块矩阵内部分块为 n×p,若使用分块矩阵转
置函数,则会使得分块矩阵内部分块大小分别为 m×n 和 p×n,这不符合矩阵元素乘法函数的参数要求.
下面是利用定义好的函数进行计算验证的例子.
⎡ 31 ⎤⎡ ⎤
⎡ 10⎤ ⎡ 0 2 ⎤⎡ ⎤ ⎢ ⎣ 13 ⎥ ⎥⎢ ⎥ ⎡⎦ ⎢ 9 3⎤
验证 ⎢ ⎥ ⎢ ⎥ ⎥⎢ × ⎢ ⎥ = ⎢ ⎥ ,其证明过程如图 19 所示,其中,Mmake_simpl 与 MMmult_simpl
⎣ 01 ⎦ ⎣ ⎣ 2 0 ⎦ ⎢ ⎡ ⎦ 13⎤ ⎥ ⎣ 3 9 ⎦
⎢ ⎢ 31 ⎥ ⎣ ⎥ ⎦ ⎣ ⎦
为自定义的分别针对于矩阵构建以及矩阵乘法的化简策略,用于简化证明过程.

Fig.19 Verification example of block matrix multiplication function
图 19 分块矩阵乘法函数验证例子

3.4 分块矩阵函数与普通矩阵函数等价性证明
分块矩阵函数与普通矩阵函数的等价性证明成为分块矩阵形式化工作中的重要内容之一的原因有两个:
1) 保证分块矩阵运算函数的正确性;2) 将普通矩阵运算函数的性质利用该等价性移植于分块矩阵运算函数之
上,能够大大减少证明过程.分块矩阵能够使得矩阵运算并行化,但分块矩阵的函数相比于普通矩阵函数更加复
杂且容易出错.因此,为了保证利用分块矩阵技术对矩阵进行运算后得到的结果仍然等于其原结果,我们需要对
分块矩阵函数与普通矩阵函数进行等价性证明.
为了证明分块矩阵函数的等价性,我们构造了一个将分块矩阵转换为矩阵的函数 MM_to_M(如图 20 所示),
该函数的作用是将一个分块矩阵类型转换成普通矩阵.该函数的定义思路如下:分块矩阵中不同分块的合并涉
及到二维表的横向合并以及二维表的竖向合并,二维表的竖向合并可使用 app 函数实现,二维表的横向合并有
多种设计方法,对于方法的选择以及原因将在第 4.2 节中详细说明.