计算机科学 ›› 2019, Vol. 46 ›› Issue (7): 139-145.doi: 10.11896/j.issn.1002-137X.2019.07.022

• 软件与数据库技术 • 上一篇    下一篇

基于Coq记录的矩阵形式化方法

马振威1,陈钢1,2   

  1. (南京航空航天大学计算机学院 南京210000)1
    (北京京航计算与通信研究所 北京100074)2
  • 收稿日期:2018-06-01 出版日期:2019-07-15 发布日期:2019-07-15
  • 作者简介:马振威(1992-),男,硕士生,CCF会员,主要研究方向为定理证明;陈 钢(1958-),男,博士,教授,CCF会员,主要研究方向为定理证明,E-mail:gangchensh@qq.com(通信作者)。
  • 基金资助:
    南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20171610),中央高校基本科研业务费专项资金资助

Matrix Formalization Based on Coq Record

MA Zhen-wei1,CHEN Gang1,2   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210000,China)1
    (Beijing Jinghang Research Institute of Computing and Communication,Beijing 100074,China)2
  • Received:2018-06-01 Online:2019-07-15 Published:2019-07-15

摘要: 矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制。Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂。针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质。基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证。同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便。

关键词: Coq, 定理证明, 记录类型, 矩阵, 形式化验证

Abstract: Matrix has a wide range of applications in engineering systems,and the correctness of matrix operations has an important impact on the reliability of engineering systems.Coq is a powerful higher-order theorem prover based on the type λ calculus.Although the Coq type system can describe variable-sized dynamic data types well,there is a lack of satisfactory description mechanisms for data types such as fixed-size vectors and matrices.At present,there is no vector library or matrix library in the Coq library,so it is more difficult to use Coq to formally verify the theorem or algorithm involving the matrix.In order to solve these problems,this paper proposed a matrix implementation method based on Record type,defined a set of basic matrix functions and proved their basic properties.The verification of the flight control transformation matrix can be done easily by using the matrix types and related lemmas provided in this paper.Compared with other matrix implementation methods,this method is not only relatively simple to implement,but also simpler and more convenient to use.

Key words: Coq, Formal verification, Matrix, Record type, Theorem proving

中图分类号: 

  • TP311
[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
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!