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

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

目标需要的化简步骤以及子目标的泛化而产生的,这些引理专门为这一个性质而服务,以支持该性质的证明.
2) 辅助函数有多种构造方式的情况
在分块矩阵函数与矩阵函数等价性证明中,我们需要一个辅助函数——将分块矩阵转化为矩阵的函数
MM_to_M.然而,该函数的定义依赖于一个二维表的横向合并函数 mlink,该函数可以由多种实现方法,构造方式
的选择还需通过后续的证明决定.以下是两种不同的实现方法(如图 30、图 31 所示).
Fixpoint mlink ma mb n:=
match n with
|O⇒mb
|S n′⇒link A (headcolumn A Zero ma)
(mlink (tailcolumn A ma) mb n′)

Fig.30 Implementation principle of the first mlink definition
图 30 第 1 种 mlink 定义实现原理

Fixpoint mlink(ma mb:list (list A)):=
match ma with
|nil⇒mb
|x::x′⇒match mb with
|nil⇒ma
|y::y′⇒(x++y)::(mlink x′ y′)
end
end.

Fig.31 Implementation principle of the second mlink definition
图 31 第 2 种 mlink 定义实现原理

这两种定义所产生的操作结果经过测试都满足我们的要求,即横向合并两个二维表,根据这两种定义可以
构造出两种分块矩阵到矩阵的转换函数.虽然两种定义的函数产生的结果相同,但由于定义的不同,在证明过程
中,前一种定义方法会产生矛盾以及无法证明的问题.
第 1 种 mlink 的定义使用文献[3]中的 link 函数作为辅助函数,但在归纳变量化简后,中会出现过于复杂而导
致无法继续证明的情况,具体如图 32 所示.