Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

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:

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