Computable decision making on the reals and other spaces via partiality and nondeterminism

• DOI: 10.48550/arxiv.1805.00468
• Publication Date: 2018-01-01
• Authors: Benjamin Sherman; Luke Sciarappa; Adam Chlipala; Michael Carbin
• Keywords: Constructive

Though many safety-critical software systems use floating point to represent real-world input and output, programmers usually have idealized versions in mind that compute with real numbers. Significant deviations from the ideal can cause errors jeopardize safety. Some programming implement exact arithmetic, which resolves this matter but complicates others, such as decision making. In these systems, it is impossible (total deterministic) discrete decisions based on connected spaces $\mathbb{R}$. We present programming-language semantics constructive topology variants allowing nondeterminism and/or partiality. Either or partiality suffices allow computable making then introduce pattern matching spaces, a language construct for creating programs generalizing functional programming, where patterns need not decidable predicates also may overlap be inexhaustive, giving rise partiality, respectively. Nondeterminism yield formal logics constructing approximate procedures. implemented constructs Marshall arithmetic.