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.

提出了一种具有纯高阶函数构造的精确实数计算的命令式语言，该语言进一步配备了用于可数非确定性选择和非确定性限制的原始运算符，以实现该语言的函数构造。该语言的指称语义是基于可计算分析和领域理论而形式化的，使用无界幂域来实现两个附加原语操作的可数非确定性证明规则。作为一个例子，给出了一个非确定性计算连续实函数根的命令式程序，它是中值定理的构造性变体，并且被证明是正确的。Coq-AERN 是构造类型中精确实数计算的公理形式化。形式化通过函数空间、开放子集、封闭子集、紧致子集和显性子集进行了扩展，与编程语言对应部分类似，这种形式化通过可数选择进行了扩展。给出了在欧几里得空间中绘制各种子集（包括一些分形）的方法。

项目成果

Nondeterministic limits and certified exact real computation

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

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

Certified exact real computation on hyperspaces

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

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

A type-theoretical interpretation of intuitionistic fixed point logic

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

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

Univerza v Ljubljani(スロベニア)

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

Some steps toward program extraction in a type-theoretical interpretation of IFP

IFP 类型理论解释中程序提取的一些步骤

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