Classical vs Quantum Computation (Week 18)
Posted by John Baez
Today we had our last class on Classical vs Quantum Computation for this quarter:

Week 18 (Mar. 15) 
2categories from typed λcalculi, continued.
The ChurchRosser theorem. Surface diagrams showing
the process of computation. βreduction as a fold
catastrophe. Thom’s ideas on catastrophe theory.
Challenge: draw the surface diagram for ηreduction.
Which catastrophe does it correspond to?
Blog entry.
Supplementary reading:
 Lucien Dujardin, Catastrophe teacher: an introduction for experimentalists.
 Barnaby P. Hilken, Towards a proof theory of rewriting: the simplytyped 2λcalculus, Theor. Comp. Sci. 170 (1996), 407–444.
 R. A. G. Seely, Weak adjointness in proof theory in Proc. Durham Conf. on Applications of Sheaves, Springer Lecture Notes in Mathematics 753, Springer, Berlin, 1979, pp. 697–701.
 R. A. G. Seely, Modeling computations: a 2categorical framework, in Proc. Symposium on Logic in Computer Science 1987, Computer Society of the IEEE, pp. 65–71.
 C. Barry Jay and Neil Ghani, The virtues of etaexpansion, J. Functional Programming 1 (1993), 1–19.
Last week’s notes are here; next week’s notes are here.
We came pretty close to our goal of explaining how processes of computation are 2morphisms in a 2category. Namely, we came close to seeing how for any typed λcalculus there’s a 2category with
 types as objects,
 terms as morphisms,
 rewrite rules (ways of simplifying terms) as 2morphisms.
We saw how to draw these 2morphisms as surfaces, and we noticed an intriguing relation to René Thom’s ideas on catastrophe theory: it turned out that the process of ‘applying a function to its argument’ gives a surface with the simplest sort of catastrophe — a fold catastrophe:
We did not reach our goal of proving that the 2category we got is a ‘cartesian closed 2category’. In fact, we didn’t even define that concept! Nor did we get around to generalizing all this to the noncartesian — or roughly speaking, ‘quantum’ — context.
Today’s session was a bit sad, because it’s the last one my student Mike Stay will attend. He’s the one who turned my interest in categories and computation from a hobby to something a bit more than a hobby, by coming to U.C. Riverside with a master’s in computer science and wanting to work on categories and quantum computation. Unfortunately, he couldn’t earn enough money here to support his family, so he took a job at Google, and he’s leaving town this weekend. Luckily, his skills in cryptography will now let him earn more than I do! I’m hoping he becomes a bigshot at Google and sets up a little ncategory research group.
Right now we’re writing an expository paper on logic, computation, categories and Feynman diagrams, for a book Bob Coecke is editing. Google has a nice policy of letting their employees spend one day a week on projects of their own choosing. So, we’ll keep working away — but it won’t be the same. I may or may not keep the Classical vs Quantum Computation seminar going in the Spring quarter: my other students are working on other stuff!
Re: Classical vs Quantum Computation (Week 18)
I was under the impression that Whitney, not Thom, discovered the fold map, and more generally classified singularities of 2dimensional maps (i.e. maps R^{2} → R^{2}).
(I was also under the impression that since the 1980s there’s a rule against calling these things “catastrophes,” but maybe the backlash has died down enough by now.)