Computable decision making on the reals and other spaces. Via partiality and nondeterminism

DOI10.1145/3209108.3209193MaRDI QIDQ5145365zbMATH OpenOpenAlexFDO

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

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.00468

zbMATH Keywords

constructive analysislocale theory

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Frames and locales, pointfree topology, Stone duality (18F70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 $mathbbR$. 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 $mathbbR$. We then introduce pattern matching on spaces, a language construct for creating programs on spaces, generalizing 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.

Recommendations

• Semantics of a sequential language for exact real-number computation
• A Denotational Semantics for Total Correctness of Sequential Exact Real Programs
• Lazy computation with exact real numbers
• Lazy computation with exact real numbers
• Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

Cited in

(3)

• scientific article; zbMATH DE number 66690 (Why is no real title available?)
• scientific article; zbMATH DE number 1157657 (Why is no real title available?)
• Towards constructive hybrid semantics

Describes a project that uses

Uses Software

• ROSCoq

This page was built for publication: Computable decision making on the reals and other spaces. Via partiality and nondeterminism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145365)