Game semantics for untyped λβη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 G, introduced by Abramsky, Jagadeesan and Malacaria, induce the same λ-theory. This is H*, the maximal theory induced already by the classical CPO model D∞, introduced by Scott in 1969. This results indicates that the current notion of game carries a very specic bias towards head reduction.