Verified exact computation over continuous higher types

验证了连续较高类型的精确计算

• 批准号: 22KF0198
• 负责人: 河村 彰星
• 金额: $ 1.47万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2023
• 资助国家: 日本
• 起止时间: 2023-03-08 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KF0198/
• 关键词: exact real computation; program verification; higher-order Hoare logic; constructive type theory; formalized mathematics

An imperative language for exact real number computation with pure higher-order function construction is proposed. The design is inspired by the standard functions in C++. The language is further equipped with primitive operators for countable nondeterministic choices and nondeterministic limits to make the language’s function construction useful. The language’s denotational semantics is formalized based on computable analysis and domain theory using an unbounded powerdomain for countable nondeterminism. Sound Hoare-style proof rules for the two additional primitive operations are devised. As an example, an imperative program nondeterministically computing a root of a continuous real function, a constructive variant of the Intermediate Value Theorem, is given and proved correct.Coq-AERN is an axiomatic formalization of exact real number computation in a constructive type theory and Coq. The formalization is extended with function spaces, open subsets, closed subsets, compact subsets, and overt subsets. Similarly to the programming language counterpart, this formalization is extended with countable choices. Examples of drawing various subsets, including some fractals, in Euclidean spaces are given.

提出了用于具有纯高阶功能构建的精确实际数量计算的命令式语言。该设计灵感来自C ++中的标准功能。该语言进一步配备了原始操作员，以实现可计数的非确定性选择和非确定性限制，以使该语言的功能构造有用。该语言的表示语义是基于可计算的无限量域的可计数性无限量基于可计算的无限量来形式化的。设计了另外两个原始操作的声音风格的证明规则。例如，给出并证明了一个连续实际函数（中间值定理的构造变体）的词根的命令式程序，并证明了正确的。格式化通过功能空间，开放子集，封闭子集，紧凑的子集和明显的子集扩展。与编程语言对应物类似，这种格式通过可计数的选择扩展。给出了在欧几里得空间中绘制各种子集（包括某些分形）的示例。

项目成果

A type-theoretical interpretation of intuitionistic fixed point logic

直觉定点逻辑的类型论解释

• 发表时间: 2022
• 作者: Ulrich Berger;Sewon Park;Holger Thies and Hideki Tsuiki
• 通讯作者: Holger Thies and Hideki Tsuiki

From Coq Proofs to Efficient Certified Exact Real Computation

从 Coq 证明到高效的认证精确真实计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Certified exact real computation on hyperspaces

超空间上经过认证的精确真实计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Univerza v Ljubljani(スロベニア)

Univerza v 卢布尔雅尼 (斯洛文尼亚)

Nondeterministic limits and certified exact real computation

不确定性限制和经过认证的精确实际计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies