Classical vs Quantum Computation (Week 14)
Posted by John Baez
This time in our course on Classical vs. Quantum Computation, we sketched how a typed λcalculus serves as a presentation of a cartesian closed category, and how every cartesian closed category arises this way. Since the students seemed to be struggling with the levels of abstraction involved, we slowed down to tackle an example:

Week 14 (Feb. 15)  The cartesian closed category generated by a typed λcalculus, and how this construction gives a functor $C: λCalc \to Cart$. The ‘internal language’ of a cartesian closed category, and how this gives a functor $L: Cart \to λCalc$. $C$ and $L$ are adjoint,
and in fact give an equivalence between typed λcalculi and
and cartesian closed categories. Example 1: the λtheory of
commutative rings.
Supplementary reading:
 Joachim Lambek and Phil Scott, Introduction to HigherOrder Categorical Logic, Cambridge U. Press, 1988. Part 1, Section 11: the cartesian closed category generated by a typed λcalculus.
Last week’s notes are here; next week’s notes are here.
At the end of class we raised a puzzle: what is a cartesian closed functor
$F: C_{\lambda Th(CommRing)} \to Set$
where $\lambda Th(CommRing)$ is the typed $\lambda$calculus for commutative rings, and $C_{\lambda Th(CommRing)}$ is the cartesian closed category generated by this $\lambda$calculus?
Only one student claimed to know the answer — so I urged him not to say what it was, and I began leading everyone else to the solution through a process of Socratic dialogue. There are, in fact, some nasty subtleties lurking in here.
Next time we’ll finish solving this puzzle and tackle a better example: the typed $\lambda$calculus for high school calculus.
Re: Classical vs Quantum Computation (Week 14)
What do you mean by ‘high school calculus’? Do you mean a Tarski highschool algebra (like the natural numbers under addition, multiplication, and exponentiation), accidentally typing ‘calculus’ twice? Or do you mean some rulebased version of differential calculus with no reference to εs and δs (something like a differential algebra)?