Classical vs Quantum Computation (Week 13)
Posted by John Baez
In this week’s class on Classical vs. Quantum Computation, we begin tackling our main example of how ‘processes of computation’ show up as 2morphisms in a 2category. We start by recalling the concept of a ‘typed λcalculus’. Next time we’ll show how a typed λcalculus can serve as a presentation of a cartesian closed category. Then we’ll try to get a cartesian closed 2category instead, where the relations give 2morphisms instead of equations between morphisms.

Week 13 (Feb. 8)  Categorifying the lambdacalculus. Lambek and Scott’s definition of a "typed lambdacalculus": types, terms, and relations (including ηreduction and βreduction).
Supplementary reading:
 David C. Keenan, To dissect a mockingbird.
 Joachim Lambek and Phil Scott, Introduction to HigherOrder Categorical Logic, Cambridge U. Press, 1988. Part 1 Sections 911: natural numbers objects in cartesian closed categories, typed λcalculi, and the cartesian closed category generated by a typed λcalculus. Note that I’m including the material on natural number objects (Section 9) mainly so you can see how to ignore it in Sections 10 and 11: in class, we are keeping things simple by considering typed λcalculi and cartesian closed categories without a natural numbers object.
Last week’s notes are here; next week’s notes are here.
Posted at February 9, 2007 8:34 PM UTC