Verified exact computation over continuous higher types

提出了一种构造纯高阶函数的精确实数计算的命令式语言。设计灵感来自于C++中的标准函数。该语言进一步配备了用于可数非确定选择和非确定限制的本原运算符，以使语言的函数构造有用。该语言的指称语义是基于可计算分析和定义域理论而被形式化的，使用了可数不确定论的无界功率定义域。为这两个附加的基元运算设计了合理的Hoare风格的证明规则。作为一个例子，给出了一个非确定性计算连续实函数的根的命令性程序，证明了该程序的正确性。通过函数空间、开子集、闭子集、紧子集和显子集对形式化进行了扩展。与编程语言类似，这种形式化使用可数选项进行扩展。文中给出了在欧氏空间中绘制各种子集的例子，包括一些分形图。

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.