John Baez
August 13, 2009
Computation and the Periodic Table
In physics, Feynman diagrams are used to reason about quantum processes. Similar diagrams can also be used to reason about logic, where they represent proofs, and computation, where they represent programs. With the rise of topological quantum field theory and quantum computation, it became clear that diagrammatic reasoning takes advantage of an extensive network of interlocking analogies between physics, topology, logic and computation. These analogies can be made precise using the formalism of symmetric monoidal closed categories. But symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized "periodic table" of ktuply monoidal ncategories. This raises the question of how these analogies extend. An important clue comes from the way symmetric monoidal closed 2categories describe rewrite rules in the lambda calculus and multiplicative intuitionistic linear logic. This talk is based on work in progress with PaulAndré Melliès and Mike Stay.
Click on this to see the transparencies of the talk:
For more details try the following papers:

John Baez and Mike Stay,
Physics, topology, logic and computation: a Rosetta Stone,
to appear in New Structures in Physics, ed. Bob Coecke.

John Baez and Aaron Lauda, A prehistory
of ncategorical physics, in Deep Beauty: Mathematical
Innovation and the Search for an Underlying Intelligibility of
the Quantum World, ed. Hans Halvorson.

Albert Burroni,
Higherdimensional word problems with applications
to equational logic, Theor. Comp. Sci. 115 (1993),
4362.

Yves Guiraud, The three
dimensions of proofs, Ann. Pure Appl.
Logic 141 (2006), 266295.

Barnaby P. Hilken, Towards a
proof theory of rewriting: the simplytyped 2λcalculus,
Theor. Comp. Sci. 170 (1996), 407444.

C. Barry Jay and Neil Ghani, The virtues of etaexpansion,
J. Functional Programming 1 (1993), 119.

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

R. A. G. Seely, Modeling
computations: a 2categorical framework, in
Proc. Symposium on Logic in Computer Science 1987,
Computer Society of the IEEE, pp. 6571.
Also try my seminar notes from
Fall 2006 and
Winter 2007.
© 2009 John Baez
baez@math.removethis.ucr.andthis.edu