2009 | OriginalPaper | Chapter
A Relational Model of a Parallel and Non-deterministic λ-Calculus
Authors : Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto
Published in: Logical Foundations of Computer Science
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.