基于偏性与非确定性的实数及其他空间上的可计算决策

尽管许多安全关键型软件系统使用浮点来表示真实世界的输入输出，程序员通常心中所想的是计算实数时的理想化版本。与理想情况的显著偏差会导致错误并危及安全。一些编程系统实现了精确实数算术，这解决了该问题却使其他问题复杂化，例如决策。在这些系统中，不可能基于如 $\mathbb{R}$ 这样的连通空间计算（全且与确定性的）离散决策。我们提出了基于构造拓扑的编程语言语义，其变体允许非确定性和/或偏性。非确定性或偏性任一即可允许在如 $\mathbb{R}$ 这样的连通空间上进行可计算决策。随后我们引入空间上的模式匹配，一种用于在空间上创建程序的语言构造，推广了函数式编程中的模式匹配，其中模式不必表示可判定谓词，且可能重叠或不穷尽，分别产生非确定性或偏性。非确定性和/或偏性还产生了用于构造近似决策过程的的形式逻辑。我们在用于精确实数算术的 Marshall 语言中实现了这些构造。