Skip to main content

How to Calculate with Nondeterministic Functions

Richard S. Bird and Florian Rabe

Abstract

While simple equational reasoning is adequate for the calculation of many algorithms from their functional specifications, it is not up to the task of dealing with others, particularly those specified as optimisation problems. One approach is to replace functions by relations, and equational reasoning by reasoning about relational inclusion. But such a wholesale approach means one has to adopt a new and sometimes subtle language to argue about the properties of relational expressions. A more modest proposal is to generalise our powers of specification by allowing certain nondeterministic, or multi-valued functions, and to reason about refinement instead. Such functions will not appear in any final code. Refinement calculi have been studied extensively over the years and our aim in this article is just to explore the issues in a simple setting and to justify the axioms of refinement using the semantics suggested by Morris and Bunkenburg.

Book Title
Mathematics of Program Construction
Editor
Graham Hutton
Pages
138−154
Publisher
Springer
Volume
11825
Year
2019