The n-Category Café

Classical vs Quantum Computation (Week 17)

Posted by John Baez

Yay! In this week’s course on Classical vs Quantum Computation, we finally reached the promised land: surface diagrams — closely resembling string worldsheets! — illustrating ‘processes of computation’:

• Week 17 (Mar. 8) - 2-categories from typed λ-calculi. For each type, a category of terms of that type, freely generated by rewrite rules. Example: high-school calculus. Confluence and termination. Surface diagrams showing the process of computation.

  Supplementary reading:

  • Joachim Lambek and Phil Scott, Introduction to Higher-Order Categorical Logic, Cambridge U. Press, 1988. Part 1, Sections 12-14: the decision problem for equality; the Church-Rosser property for bounded terms; all terms are bounded.

Last week’s notes are here; next week’s notes are here.