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

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

Fig.13 Type definition of block matrix
图 13 分块矩阵类型定义
3.2 分块矩阵类型等价性质
在第 2.2 节中,我们提出了一个新的函数 M_eq 来判别矩阵相等,但该函数不适用于分块矩阵,当使用 M_eq
来判别分块矩阵相等时,会出现图 14 的情况:

Fig.14 Problems caused by M_eq discriminating the equality of block matrices
图 14 由 M_eq 判别分块矩阵相等引起的问题
M_eq 函数的作用是:提取出矩阵类型中的二维表后,用 eq 函数判别是否相等.由图 14 可以看出:使用 M_eq
判别分块矩阵时,需要用 eq 函数判别两个二维表相等.这要求二维表中所有元素相等(使用 eq 函数作为判别函
数),但该分块矩阵中的二维表内元素为用 Record 表示的矩阵类型,在第 2.2 节中我们说明了矩阵类型不能使用
eq 函数来判别矩阵类型相等的问题,因此我们提出了针对分块矩阵的等价判别函数 MM_eq.该函数是一个递归
函数,其依赖于两个递归函数 list_Meq 和 dlist_Meq.为了代码的简洁性,在分块矩阵形式化的代码部分我们也采
用了 Section 机制,在下文的代码中,A,m,n,m2 和 n2 都为局部变量,其类型为(A:Set)(m n m2 n2:nat).
list_Meq 主要对由矩阵构成的表进行相等判断,该函数对表中的每个相应的矩阵利用 M_eq 函数进行相等
判断,最后返回的是所有矩阵相等的与命题,其实质是利用 M_eq 来判别两个表内所有相应矩阵相等.下面是
list_Meq 函数的定义以及图示(如图 15 所示).
Fixpoint list_Meq(l1 l2:list(Mat A m n)):=