Pietro Di Gianantonio, Ginaluca Franco, Furio Honsell
Game semantics for untyped lambda calculus.
Abstract
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}.