Andrew D Ker, Hanno Nickau and C-H Luke Ong:
A universal innocent game model for the Böhm tree
lambda theory.
In Computer Science Logic 1999, Springer-Verlag, Lecture Notes in
Computer Science, volume 1683, pages 405 - 419, 1999.
BibTeX Entry
Compressed Postscript File
Abstract
We present a game model of the untyped
lambda-calculus, with equational theory equal to the Böhm tree
lambda-theory B, 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 lambda-calculus.
|