Computational complexity and practice of verified and efficient algorithms for dynamical systems

动力系统的计算复杂性和经过验证的高效算法的实践

基本信息

批准号：
20K19744
负责人：
THIES HOLGER
金额：
$ 2.75万
依托单位：
Kyoto University (2021-2022)Kyushu University (2020)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Early-Career Scientists
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

Large progress has been made on the formalization of exact real computation in type theory and its implementation in the Coq proof assistant. Previous work on formalizing nondeterministic computation on real and complex numbers has been extended and unified. In particular, progress has been made on formalizing nondeterminism occuring in exact real computation and a sound notion of a multivalued limit operator was devised. The theory was implemented in the Coq proof assistant and using Coq's program extraction mechanism efficient Haskell programs for exact real computation can be extracted. As a non-trivial application we extract a nondeterministic program computing the complex square root.As Covid-19 related border restrictions loosened during this year, international joint research could be resumed. During a visit by Michal Konecny (Aston University, UK), we extended the aforementioned formalization to spaces of subsets and functions, which has important applications to differential equations, in particular regarding reachability questions.Several representations for dealing with subsets have been compared in terms of efficiency and certfied programs for generating drawings of subsets have been extracted and shown to behave well in terms of running time. Examples include fractals in two dimensional Euclidean space.Progress has also been made on integrating the logic based proof system IFP into our type theoretical work. A system for IFP style proofs in Coq and a new program extraction to untyped lambda calculus similar to IFP was developed based on the meta-coq framework.

关于类型理论中精确的实际计算的形式化及其在COQ证明助手中的实施方面取得了很大进展。以前关于对真实数字和副本的非确定计算进行正式化的工作已被扩展和统一。特别是，在确切的实际计算中形式化非确定性的正式化方面已经取得了进展，并设计了多价极限运算符的合理概念。该理论是在COQ证明助手中实施的，并使用COQ的程序提取机制有效的Haskell程序来进行精确计算。作为一种非平凡的应用，我们提取了计算复杂平方根的非确定程序。与19年相关的边界限制相关的边界限制，可以恢复国际联合研究。在Michal Konecny（英国阿斯顿大学）的一次访问中，我们将上述形式化扩展到子集和功能的空间，该空间对差分方程式具有重要的应用，特别是在可及性问题上。与之处理子集打交道的几个效率和确定性计划相比，与子集进行了比较，以使生成的绘图符合时间，并且已经提取了时间。示例包括二维欧几里得空间中的分形。还为将基于逻辑的证明系统IFP集成到我们的类型理论工作时也被提出。 COQ中的IFP样式证明的系统，以及基于Meta-COQ框架开发了类似于IFP的新程序提取到未型Lambda微积分的系统。