Non-determinism in a functional setting

The pure untyped lambda calculus augmented with an (erratic) choice operator is considered as an idealised nondeterministic functional language. Both the `may´ and the `must´ modalities of convergence are of interest. Following Abramsky´s (1991) work on domain theory in logical form, we identify the denotational type that captures the computational situation δ=P[[δ→δ]⊥], where P[-] is the Plotkin power-domain functor. We then carry out a systematic programme that hinges on three distinct interpretations of δ, namely process-theoretic, denotational, and logical. The main theme of the programme is the complementarity of the various interpretations of δ. This work may be seen as a step towards a rapprochement between the algebraic theory of processes in concurrency on the one hand, and the lazy lambda calculus as a foundation for functional programming on the other