A relational model of a parallel and non-deterministic lambda calculus

Abstract. We recently introduced an extensional model of the pure -calculus living in a canonical cartesian closed category of sets and re-lations [6]. In the present paper, we study the non-deterministic features of this model. Unlike most traditional approaches, our way of interpret-ing non-determinism does not require any additional powerdomain con-struction: we show that our model provides a straightforward semantics of non-determinism (may convergence) by means of unions of interpreta-tions 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 de ne its operational semantics (based on the may and must intuitions underlying our two additional operations). We describe the interpreta-tion 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