Hans Aberg <[EMAIL PROTECTED]> writes:
> Exactly how is this connection between the lambda calculus and
> category theory described? -- That is, one would expect to know that
> if one has a category of some sort, it is equivalent to the lambda
> calculus, or something like that.
There is a very beautiful connection here, which is explained at
length e.g. in [1]. In short, every simply typed lambda-calculus gives
rise to a a cartesian closed category (ccc) (by taking its term
model). On the other hand, every ccc gives us a simply typed
lambda-calculus, by considering its so-called internal language, which
has its objects as types, and its morphisms as terms: a morphism
f:A--> B is a a term of B in the context of a variable (or a tuple of
variables) of type A. These two mappings are adjoint (the internal
language construction is the right adjoint).
To get the untyped lambda-calculus, you move from ccc's to so-called
c-monoids, but I've forgotten the exact definition of that; it's like
a ccc, but without a terminal object I think to eliminate trivial
(one-point) models.
--Christoph.
[1]
@Book{LambekScott,
author = "J.~Lambek and P.~J.~Scott",
title = "Introduction to Higher Order Categorical Logic",
publisher = "Cambridge University Press",
year = 1986,
volume = 7,
series = "Cambridge studies in advanced mathematics"
}
