Adaptinginnocent g ame models for the B#ohm tree -theory
Andrew D. Ker, Hanno Nickau, H. Luke Ong · 2003
We present a game model of the untyped � -calculus, with equational theory equal to the B#ohm tree � -theory B, which is universal (i.e. every element of the model is de8nable by some term). This answers a question of Di Gianantonio, Franco and Honsell. We build on our earlier work, which uses the methods of innocent game semantics to develop a universal model inducing the maximal consistent sensible theory H ∗ . To our knowledge these are the 8rst syntax-independent