INRIA Paris-Rocquencourt
3pm Thursday, 3rd September, 2009
Room 4.31/33, Informatics Forum
Note nonstandard day and time
Models of the untyped lambda-calculus may be defined either as reflexive objects in cartesian closed categories (categorical models), or as combinatory algebras satisfying the 5 axioms of Curry and the Meyer-Scott axiom (lambda-models). Concerning categorical models, we show that _every_ categorical model can be presented as a lambda-model, also when the underlying category is not well-pointed, and we give sufficient conditions for categorical models living in arbitrary cpo-enriched cartesian closed category for having H* as equational theory. We build a categorical model D living in a ccc of sets and (multi)-relations (relational semantics) and satisfying these conditions (thus such that Th(D) = H*).
Finally, we show that this relational model satisfies interesting algebraic properties that make it suitable for dealing with non-deterministic and parallel extensions of lambda calculus. 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 MIX rule of Linear Logic.
We describe the interpretation of this parallel and non-deterministic 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.