The n-Category Café

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 2-morphisms in a 2-category. 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 2-category instead, where the relations give 2-morphisms instead of equations between morphisms.

• Week 13 (Feb. 8) - Categorifying the lambda-calculus. Lambek and Scott’s definition of a "typed lambda-calculus": types, terms, and relations (including η-reduction and β-reduction).
  
  Supplementary reading:
  
  
  • David C. Keenan, To dissect a mockingbird.
  • Joachim Lambek and Phil Scott, Introduction to Higher-Order Categorical Logic, Cambridge U. Press, 1988. Part 1 Sections 9-11: 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.