Pietro Di Gianantonio, Ginaluca Franco, Furio Honsell

Game semantics for untyped lambda calculus.


We study extensional models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, somewhat unexpectedly and contrary to what happens in ordinary categories of domains, all reflexive objects in the category of games $\mathcal{G}$, introduced by Abramsky, Jagadeesan and Malacaria, induce the same $\lambda$-theory. This is $\mathcal{H}^{*}$, the maximal theory induced already by the classical CPO model $D_{\infty}$, introduced by Scott in 1969. This results indicates that the current notion of game carries a very specific bias towards {\em head reduction}.