A relational semantics for parallelism and non-determinism in a functional setting

We recently introduced an extensional model of the pure λ-calculus living in a canonical cartesian closed category of sets and relations (Bucciarelli et al. (2007) [6]). In the present paper, we study the non-deterministic features of this model. Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction. We show that our model provides a straightforward semantics of non-determinism (may convergence) by means of unions of interpretations, as well as of parallelism (must convergence) by means of a binary, non-idempotent operation available on the model, which is related to the mix rule of linear logic. More precisely, we introduce a λ-calculus extended with non-deterministic choice and parallel composition, and we define its operational semantics (based on the may and must intuitions underlying our two additional operations). We describe the interpretation of this calculus in our model and show that this interpretation is ‘sensible’ with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.