计算机科学 ›› 2019, Vol. 46 ›› Issue (7): 139-145.doi: 10.11896/j.issn.1002-137X.2019.07.022
马振威1,陈钢1,2
MA Zhen-wei1,CHEN Gang1,2
摘要: 矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制。Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂。针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质。基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证。同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便。
中图分类号:
[1]吴森堂.飞行控制系统[M].北京:北京航空航天大学出版社,2013. [2]Cook M V.Flight Dynamic Principles[M].British:Butterworth-Heinemann,2007:20-33. [3]CHLIPALA A.Certified Programming with Dependent Types:A Pragmatic Introduction to the Coq Proof Assistant[M].The MIT Press,2011. [4]TEAM T C D.The Coq Proof Assistant Reference Manual -- Version V8.7.1[C]∥INRIA.2016. [5]NIPKOW T,WENZEL M,PAULSON L C.Isabelle/HOL:a proof assistant for higher-order logic[C]∥Springer-Verlag,2002:xiii-xiv. [6]SHI Z,SONG X,ZHANG J,et al.Formalization of Matrix Theo- ry in HOL4[J].Advances in Mechanical Engineering,2014,56(5):1-14. [7]HARRISON J.A HOL theory of euclidean space[C]∥International Conference on Theorem Proving in Higher Order Logics.Springer-Verlag,2005:114-129. [8]MCBRIDE C.Epigram:Practical Programming with Dependent Types[M]∥Advanced Functional Programming.Springer Berlin Heidelberg,2005:130-170. [9]MAGAUD N.Programming with Dependent Types in Coq:a Study of Square Matrices[C]∥Unpublished.2005. [10] WILSON S,FLEURIOT J,SMAILL A.Inductive Proof Automation for Coq[R].England:The University of Edinburgh,2010:3-9. [11] DENES M,BERTOT Y.Experiments with computable matrices in the Coq system[R].France:INRIA,2011:2-27. [12] MULLEN E,PERNSTEINER S,WILCOX J R,et al.Euf:minimizing the Coq extraction TCB[C]∥The ACM Sigplan International Conference.ACM,2018:172-185. [13] SOZEAU M,TABAREAU N.Universe Polymorphism in Coq[M]∥Interactive Theorem Proving.Cham:Springer,2014:499-514. [14] ZILIANI B,SOZEAU M.A unification algorithm for Coq featuring universe polymorphism and overloading[C]∥ACM Sigplan International Conference on Functional Programming.ACM,2015:179-191. [15] KREBBERS R,SPITTERS B.Type classes for efficient exact real arithmetic in Coq[J].Logical Methods in Computer Science,2013,9(1):51-59. [16] BOLDO S,LELAY C,MELQUIOND G.Coquelicot:A User- Friendly Library of Real Analysis for Coq[J].Mathematics in Computer Science,2015,9(1):41-62. |
[1] | 李斌, 万源. 基于相似度矩阵学习和矩阵校正的无监督多视角特征选择 Unsupervised Multi-view Feature Selection Based on Similarity Matrix Learning and Matrix Alignment 计算机科学, 2022, 49(8): 86-96. https://doi.org/10.11896/jsjkx.210700124 |
[2] | 蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098 |
[3] | 齐秀秀, 王佳昊, 李文雄, 周帆. 基于概率元学习的矩阵补全预测融合算法 Fusion Algorithm for Matrix Completion Prediction Based on Probabilistic Meta-learning 计算机科学, 2022, 49(7): 18-24. https://doi.org/10.11896/jsjkx.210600126 |
[4] | 刘云, 董守杰. 基于CUDA核函数的多路视频图像拼接加速算法 Acceleration Algorithm of Multi-channel Video Image Stitching Based on CUDA Kernel Function 计算机科学, 2022, 49(6A): 441-446. https://doi.org/10.11896/jsjkx.210600043 |
[5] | 何亦琛, 毛宜军, 谢贤芬, 古万荣. 基于点割集图分割的矩阵变换与分解的推荐算法 Matrix Transformation and Factorization Based on Graph Partitioning by Vertex Separator for Recommendation 计算机科学, 2022, 49(6A): 272-279. https://doi.org/10.11896/jsjkx.210600159 |
[6] | 黄华伟, 李春华. 一种基于热带半环的密钥建立协议的安全性分析 Security Analysis of A Key Exchange Protocol Based on Tropical Semi-ring 计算机科学, 2022, 49(6A): 571-574. https://doi.org/10.11896/jsjkx.210700046 |
[7] | 魏鹏, 马玉亮, 袁野, 吴安彪. 用户行为驱动的时序影响力最大化问题研究 Study on Temporal Influence Maximization Driven by User Behavior 计算机科学, 2022, 49(6): 119-126. https://doi.org/10.11896/jsjkx.210700145 |
[8] | 梁珍珍, 徐明. 基于海洋水声信道的密钥协商方案 Key Agreement Scheme Based on Ocean Acoustic Channel 计算机科学, 2022, 49(6): 356-362. https://doi.org/10.11896/jsjkx.210400097 |
[9] | 唐超尘, 仇洪冰, 刘鑫, 唐清华. 非均匀白噪声条件下的相干MIMO雷达角度估计 Angle Estimation of Coherent MIMO Radar Under the Condition of Non-uniform Noise 计算机科学, 2022, 49(5): 262-265. https://doi.org/10.11896/jsjkx.210300162 |
[10] | 高越, 傅湘玲, 欧阳天雄, 陈松龄, 闫晨巍. 基于时空自适应图卷积神经网络的脑电信号情绪识别 EEG Emotion Recognition Based on Spatiotemporal Self-Adaptive Graph ConvolutionalNeural Network 计算机科学, 2022, 49(4): 30-36. https://doi.org/10.11896/jsjkx.210900200 |
[11] | 王以涵, 郝世杰, 韩徐, 洪日昌. 基于低秩矩阵估计的暗光图像增强模型 Low-light Image Enhancement Model with Low Rank Approximation 计算机科学, 2022, 49(1): 187-193. https://doi.org/10.11896/jsjkx.210600090 |
[12] | 官铮, 邓扬琳, 聂仁灿. 光谱重建约束非负矩阵分解的高光谱与全色图像融合 Non-negative Matrix Factorization Based on Spectral Reconstruction Constraint for Hyperspectral and Panchromatic Image Fusion 计算机科学, 2021, 48(9): 153-159. https://doi.org/10.11896/jsjkx.200900054 |
[13] | 董晓梅, 王蕊, 邹欣开. 面向推荐应用的差分隐私方案综述 Survey on Privacy Protection Solutions for Recommended Applications 计算机科学, 2021, 48(9): 21-35. https://doi.org/10.11896/jsjkx.201100083 |
[14] | 张杰, 岳韶华, 王刚, 刘家义, 姚小强. 基于Stackelberg与边拉普拉斯矩阵的多智能体系统 Multi-agent System Based on Stackelberg and Edge Laplace Matrix 计算机科学, 2021, 48(8): 253-262. https://doi.org/10.11896/jsjkx.200700032 |
[15] | 杨宏鑫, 宋宝燕, 刘婷婷, 杜岳峰, 李晓光. 基于耦合随机投影的张量填充方法 Tensor Completion Method Based on Coupled Random Projection 计算机科学, 2021, 48(8): 66-71. https://doi.org/10.11896/jsjkx.200900055 |
|