Topological representation of the lambda-calculus
S. Awodey
Carnegie Mellon University
September 1998
The lambda-calculus can be represented
topologically by assigning certain spaces to the types and certain
continuous maps to the terms. Using a recent result from category
theory, the usual calculus of lambda conversion is shown to be
deductively complete with respect to such topological
semantics. It is also shown to be functionally complete, in
the sense that there is always a ``minimal'' topological model, in
which every continuous function is lambda-definable. These
results subsume earlier ones using cartesian closed categories, as
well as those employing so-called Henkin and Kripke lambda-models.