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

麻莹莹 等:基于 Coq 的分块矩阵运算的形式化 1887

Lemma M_eq_ref: forall {A:Set} {m n:nat} (m0:Mat A m n), m0===m0.
Lemma M_eq_sym: forall {A:Set} {m n:nat} (m0 m1:Mat A m n),
m0===m1→m1===m0.
Lemma M_eq_trans: forall {A:Set} {m n:nat} (m0 m1 m2:Mat A m n),
m0===m1→m1===m2→m0===m2.
2.3 矩阵函数构造
关于矩阵类型的运算操作函数主要分为矩阵取负运算函数、加减运算函数、矩阵数乘运算函数、矩阵乘
法运算函数以及矩阵转置函数.矩阵处理函数的构造主要分为 3 个步骤:一是构建对二维表处理操作函数,二是
完成该函数输出二维表的高度和宽度等价证明,三是利用前两者构建处理矩阵并且生成矩阵的函数(封装).采
用该方法构造的矩阵处理函数使得矩阵的高度与宽度证明贯穿于函数处理过程中,能够真正地保证输入与输
出矩阵高度与宽度固定,因此无法产生矩阵越界错误.以矩阵乘法函数为例,矩阵乘法的原理如下.
若 A 为 m×n 矩阵,B 为 n×p 矩阵,则其两者的乘积 AB 会是一个 m×p 矩阵:
n
(AB ) = ∑ a b .
ij
ir rj
r= 1
矩阵乘法函数的构造需依次构造多个递归函数,其分别为 product′,l_mul_dl,dl_mul_dl,mat_mul_mat.其中,
• product′函数为表的内积函数,其接受两个表作为输入参数并返回其内积结果;
• l_mul_dl 函数是表与二维表相乘函数,其利用递归将 l 与 m 中每个表分别进行内积,将其结果以表类型
输出.在完成该函数的构造后,还需对其输出结果(表)的长度进行证明,如图 2 所示;
• dl_mul_dl 为二维表与二维表的相乘函数,其基于 l_mul_dl 函数利用递归实现两个二维表中的表依次
内积,并以二维表类型输出.在完成该函数的构造后,还需对其输出结果(二维表)的高度与宽度进行证
明,如图 3 所示;
• mat_mul_mat 以两个矩阵类型作为输入参数,由于矩阵乘法原理要求乘号左边的矩阵的每一行乘上与
乘号右边的矩阵的每一列作内积,根据 dl_mul_dl 函数的实现原理,需要将第二个矩阵进行转置后再进
行运算.在完成该函数的构造后,还需对其输出结果(二维表)的高度与宽度进行证明,如图 4 所示.

Fig.2 Implementation principle of l_mul_dl function
图 2 l_mul_dl 函数实现原理

Fig.3 Implementation principle of dl_mul_dl function
图 3 dl_mul_dl 函数实现原理