We present a game model of the untyped λ-calculus, with equational theory equal to the Böhm tree λ-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 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 first syntax-independent universal models of the untyped λ-calculus.
CITATION STYLE
Ker, A. D., Nickau, H., & Luke Ong, C. H. (1999). A universal innocent game model for the Böhm tree lambda theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1683, pp. 405–419). Springer Verlag. https://doi.org/10.1007/3-540-48168-0_29
Mendeley helps you to discover research relevant for your work.