Editing User:Michiexile/MATH198/Lecture 5 (section)

=====CCC to Lambda=====

To go in the other direction, starting out with a Cartesian Closed Category and finding a typed lambda calculus corresponding to it, we construct its ''internal language''.

Given a CCC <math>C</math>, we can assume that we have chosen, somehow, one actual product for each finite set of factors. Thus, both all products and all projections are well defined entities, with no remaining choice to determine them.

The ''types'' of the internal language <math>L(C)</math> are just the objects of <math>C</math>. The existence of products, exponentials and terminal object covers axioms 1-2. We can assume the existence of variables for each type, and the remaining axioms correspond to definition and behaviour of the terms available.

Using the properties of a CCC, it is at this point possible to prove a resulting equivalence of categories <math>C(L(C)) = C</math>, and similarly, with suitable definitions for what it means for formal languages to be equivalent, one can also prove for a typed lambda-calculus <math>L</math> that <math>L(C(L)) = L</math>. 

----
More on this subject can be found in:
* Lambek & Scott: ''Aspects of higher order categorical logic'' and ''Introduction to higher order categorical logic''

More importantly, by stating <math>\lambda</math>-calculus in terms of a CCC instead of in terms of ''terms'' and ''rewriting rules'' is that you can escape worrying about variable clashes, alpha reductions and composability - the categorical translation ignores, at least superficially, the variables, reduces terms with morphisms that have equality built in, and provides associative composition ''for free''.

At this point, I'd recommend reading more on Wikipedia [http://en.wikipedia.org/wiki/Lambda_calculus] and [http://en.wikipedia.org/wiki/Cartesian_closed_category], as well as in Lambek & Scott: Introduction to Higher Order Categorical Logic. The book by Lambek & Scott goes into great depth on these issues, but may be less than friendly to a novice.