权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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程序。作为一个非平凡的应用程序，我们提取了一个计算复数平方根的非确定性程序。随着今年新冠肺炎相关边境限制的放松，国际联合研究可能会恢复。在访问期间由Michal Konecny（阿斯顿大学，英国），我们扩展了上述形式化的空间的子集和功能，它有重要的应用微分方程，特别是关于可达性questions.Several表示处理子集进行了比较的效率和certified程序生成图纸的子集已被提取，并表现良好的运行时间。例子包括二维欧几里德空间中的分形。在将基于逻辑的证明系统IFP整合到我们的类型理论工作中方面也取得了进展。基于Meta-Coq框架，开发了一个Coq语言的IFP风格证明系统和一个新的类似于IFP的无类型lambda演算的程序抽取方法.