Innocent game models of untyped lambda calculus.

Abstract

We present a new denotational model for the untyped lambda-calculus, using the techniques of game semantics. The strategies used are `innocent' in the sense of Hyland and Ong (1994) and Nickau (1996), but the traditional distinction between `question' and `answer' moves is removed. We first construct models D and D_rec as global sections of a reflexive object in the categories /A and /A_rec of arenas and innocent and recursive innocent strategies respectively. We show that these are sensible lambda-eta-algebras but are neither extensional nor universal.

We then introduce a new representation of innocent strategies in an `economical form'. We show a strong connexion between the economical form of the denotation of a term in the game models and a `variable-free form' of the Nakajima tree of the term. Using this we show that the definable elements of D_rec are precisely what we call `effectively almost-everywhere copycat (EAC) strategies'. The category /A_eac with these strategies as morphisms gives rise to a lambda-eta-model D_eac which we show has the same expressive power as D_infinity, i.e. the equational theory of D_eac is the maximal consistent sensible theory H*. We show that the model D_eac is sensible, order-extensional and universal (i.e. every strategy is the denotation of some lambda-term). To our knowledge this is the first syntax-free model of the untyped lambda-calculus with the universality property.