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
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K19744/
• 关键词: Computable Analysis; Exact Real Computation; Formal Proofs; Type Theory; Program Extraction; Spaces of subsets; ODEs; Proof Assistants; 計算可能解析学; 計算量; 計算機援用証明; 実数計算; Computable analysis; Differential equations; Verification; Formal proofs

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

项目成果

Determining approximate solution of partial differential equations using radial basis function model trained with parallel symbiotic organisms search algorithm

使用并行共生生物搜索算法训练的径向基函数模型确定偏微分方程的近似解

• DOI: 10.1002/cpe.7558
• 发表时间: 2022-12-07
• 期刊: Concurrency and Computation: Practice and Experience
• 作者: Arnapurna P;a;a
• 通讯作者: a

Axiomatic Reals and Certified Efficient Exact Real Computation

公理实数和经过认证的高效精确实数计算

• DOI: 10.1007/978-3-030-88853-4_16
• 发表时间: 2024-09-13
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: M. Konečný;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Formalizing Hyperspaces for Extracting Efficient Exact Real Computation

形式化超空间以提取高效精确的实数计算

• DOI: 10.4230/lipics.mfcs.2023.59
• 发表时间: 2024-09-13
• 期刊: Journal of Physics: Conference Series
• 作者: M. Konečný;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Uniform Complexity of Solving Partial Differential Equations and Exact Real Computation

求解偏微分方程的一致复杂度与精确实数计算

• 发表时间: 2021
• 作者: Holger Thies

Computable analysis and notions of continuity in Coq

Coq 中的可计算分析和连续性概念

• DOI: 10.23638/lmcs-17(2:16)2021
• 发表时间: 2019-04-30
• 期刊: Log. Methods Comput. Sci.
• 作者: Florian Steinberg;L. Théry;Holger Thies
• 通讯作者: Holger Thies