Abstract

We study models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, in the category of games G, introduced by Abramsky, Jagadeesan and Malacaria, all lambda-models can be partitioned in three disjoint classes, and each model in a class induces the same theory, i.e. the set of equations between terms, that is: the theory H*, the theory which identifies all the terms which have the same Boehm tree and the theory which identifies all the terms which have the same Levy-Longo tree.