FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Computable decision-making on the reals and other spaces via partiality and nondeterminism

Authors: Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam Chlipala

Paper Information

Title:Computable decision-making on the reals and other spaces via partiality and nondeterminism
Authors:Benjamin Sherman, Luke Sciarappa, Michael Carbin and Adam Chlipala
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:constructive mathematics, programming language semantics, formal topology, locale theory, pointfree topology
Abstract:

ABSTRACT. 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 and jeopardize safety. Some programming systems implement exact real arithmetic, which resolves this matter but complicates others, such as decision-making. In these systems, it is impossible to compute (total and deterministic) discrete decisions based on connected spaces such as R. We present programming language semantics based on constructive topology with variants allowing nondeterminism and/or partiality. Either nondeterminism or partiality suffices to allow computable decision-making on connected spaces such as R. We then introduce pattern matching on spaces, a language construct for creating programs on spaces that generalizes pattern matching in functional programming, where patterns need not represent decidable predicates and also may overlap or be inexhaustive, giving rise to nondeterminism or partiality, respectively. Nondeterminism and/or partiality also yield formal logics for constructing approximate decision procedures. We implemented these constructs in the Marshall language for exact real arithmetic.

Pages:10
Talk:Jul 12 14:00 (Session 76E)
Paper: