A. Ker, H. Nickau and C.-H.L. Ong
November 2000, 40 pp.
We present a game model of the untyped lambda-calculus, with equational theory equal to the Böhm tree lambda-theory, which is universal (i.e. every element of the model is definable by some term). This answers a question of Di Gianantonio, Franco and Housell. We build on our earlier work, which uses the methods of innocent game semantics to develop a universal model inducing the maximal consistent theory H*. To our knowledge these are the first syntax-independent universal models of the untyped lambda-calculus.