## February 9, 2007

### 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.

Posted at February 9, 2007 8:34 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1157

## 0 Comments & 2 Trackbacks

Read the post Classical vs Quantum Computation (Week 12)
Weblog: The n-Category Café
Excerpt: How to see computation as a process: rewrite rules.
Tracked: February 9, 2007 9:21 PM
Read the post Classical vs Quantum Computation (Week 14)
Weblog: The n-Category Café
Excerpt: From typed lambda-calculus to cartesian closed categories and back.
Tracked: February 16, 2007 10:47 PM

Post a New Comment