Nondeterministic Functional Programming with Sets

Abstract

Nondeterminism can be introduced into a functional language, along with a set of laws for reasoning about the behaviour of programs, without disturbing referential transparency. We show how to do this by adding a new type constructor for sets and a carefully selected family of operations on sets. Instead of specifying a nondeterministic choice explicitly with choose or amb, a programmer specifies the set of values which the program might compute. Operations on sets are restricted in order to maintain laws for reasoning about programs; in particular, no function can choose an element from a set. The implementation is specified via rewrite rules that transform a program in the nondeterministic language into an ordinary functional program augmented with amb (which is not directly accessible to the programmer). The denotational semantics for this language is based on the Hoare powerdomain, so it includes bottom as a possible result even when the implementation will definitely not produce bottom. Since the denotational semantics fails to capture all the properties of the implementation, we present an additional method for reasoning about the productivity of a program. Productivity can be used to place additional constraints on the implementation which are not expressible in the powerdomain semantics. All of these techniques are illustrated by defining a “processor farm” program and proving several of its properties.