A Relational Model of a Parallel and Non-deterministic λ-Calculus

We recently introduced an extensional model of the pure

λ

-calculus living in a canonical cartesian closed category of sets and relations [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.