Dually nondeterministic functions

Abstract

Nondeterminacy is a fundamental notion in computing. We show that it can be described by a general theory that accounts for it in the form in which it occurs in many programming contexts, among them specifications, competing agents, data refinement, abstract interpretation, imperative programming, process algebras, and recursion theory. Underpinning these applications is a theory of nondeterministic functions; we construct such a theory. The theory consists of an algebra with which practitioners can reason about nondeterministic functions, and a denotational model to establish the soundness of the theory. The model is based on the idea of free completely distributive lattices over partially ordered sets. We deduce the important properties of nondeterministic functions. © 2008 ACM.