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

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

本次工作在已有引理基础上对未完成的引理进行补充以及证明,其内容见表 2、表 3.
Table 2 Existing matrix lemma
表 2 现有矩阵引理

函数 引理 引理名字 引理内容
加法交换律 matrix_add_comm A+B=B+A
加法结合律 matrix_add_assoc (A+B)+C=A+(B+C)
matrix_each add
左加零矩阵性质 matrix_add_zero_l O+A=A
右加零矩阵性质 matrix_add_zero_r A+O=A
减法交换律 matrix_sub_opp A−B=−(B−A)
matrix_each sub
减法结合律 matrix_sub_assoc A−B−C=A−(B+C)
matrix_mul 乘法左分配律 matrix_mul_distr_l (A±B)×C=A×C±B×C
T T
trans 转置性质 tteq (A ) =A
Table 3 Supplemental matrix lemma
表 3 补充矩阵引理
函数 引理 引理名字 引理内容
左减零矩阵性质 matrix_sub_zero_l O−A=−A
matrix_each sub 右减零矩阵性质 matrix_sub_zero_r A−O=A
自身相减性质 matrix_sub_self A−A=O
数乘交换律 const_mul_comm c1*A=A*c1
数乘左分配律 const_mul_l_distr_l (c1+c2)*A=c1*A+c2*A
const_mul_l
const_mul _r 数乘右分配律 const_mul_l_distr_r c*(A±B)=c*A±c*B
数左乘 0 性质 const_mul_l_0 0*A=O
数右乘 0 性质 const_mul_r_0 A*0=O
矩阵乘法左分配律 matrix_mul_distr_l (A±B)×C=A×C±B×C
矩阵乘法右分配律 matrix_mul_distr_r C×(A±B)=C×A±C×B
矩阵左乘零矩阵性质 matrix_mul_zero_l O×A=O
matrix_mul 矩阵右乘零矩阵性质 matrix_mul_zero_r A×O=O
矩阵左乘单位矩阵性质 matrix_mul_unit_l I×A=A
矩阵右乘单位矩阵性质 matrix_mul_unit_r A×I=A
矩阵乘法结合律 matrix_mul_assoc A×B×C=A×(B×C)
T
矩阵转置相等性质 meq_teq A=B↔A =B T
T
T
T
矩阵转置与加法性质 teq_add (A±B) =A ±B
trans T T
矩阵转置与数乘性质 cteq (k*A) =k*A
T
T
T
矩阵转置与乘法性质 teq_mul (A×B) =B ×A
对于一些相似的性质,我们无需一一证明,可以通过已有的矩阵函数性质推导得到,这样可以大幅度减少工
作量,如单位矩阵右乘性质:
×=
_
A I A (apply meq teq )
×
_
(A I ) = T A T (apply teq mul )
I × T A = T A T (apply trans MI )
_
I × A = T A T (apply matrix mul unit _ )l
_
_
本文定义的矩阵以及矩阵函数是多态类型,其能够使得矩阵向各个域扩展,因此在所有性质证明完成后,使
用 Module 对其进行封装,当输入实数模块参数时,获得实数矩阵模块,其中包括所有的矩阵类型、函数定义以及
相关性质.本次矩阵形式化工作中提出了整数矩阵、实数矩阵、复数矩阵以及函数矩阵的基础库.
坐标系转换矩阵构成了飞行控制系统的基本组成部分,其可靠性对飞行安全有重要影响.飞行控制系统设
计中使用了 5 种坐标系,它们之间存在 20 种转换矩阵,其中,许多转换矩阵相当复杂,利用人工计算难免会产生
错误.在本次研究工作中,我们利用矩阵形式化基础库对飞行控制系统中坐标系之间的转换矩阵做了验证,下面
我们利用实数矩阵库来验证其中一个简单的例子,即飞行控制系统中气流坐标系与稳定坐标系的旋转矩阵.
验证内容: