Game semantics for the untyped λβη-calculus

Abstract. We study extensional models of the untyped lambda calculus in the setting of the game semantics introduced by Abramsky, Hyland et alii. In particular we show that, somewhat unexpectedly and contrary to what happens in ordinary categories of domains, all reflexive objects in a standard category of games, induce the same λ-theory. This is H∗, the maximal theory induced already by the classical C.P.O. model D∞, introduced by Scott in 1969. This results indicates that the current notion of game carries a very specific bias towards head reduction