## Quantum lambda calculus, symmetric monoidal closed categories, and TQFTs

The last post was all about stuff that’s already known. I’ll be working in my thesis on describing the syntax of what I’ll call simply-typed quantum lambda calculus. Symmetric monoidal closed categories (SMCCs) are a generalization of CCCs; they have tensor products instead of products. One of the immediate effects is the lack of built-in projection morphisms and for extracting the first and second element of a pair. And without these, there’s no duplication morphism $\Delta: A\to A\otimes A$; morphisms of this type can exist, but there’s no way to express the notion that it should make a copy of the input! The no-cloning theorem is built in.

The typical CCC in which models of a lambda theory are interpreted is Set. The typical SMCC in which models of a quantum lambda theory will be interpreted is Hilb, the category of Hilbert spaces and linear transformations between them. Models of lambda theories correspond to functors from the CCC arising from the theory into Set. Similarly, models of a quantum lambda theory should be functors from a SMCC to Hilb.

Two-dimensional topological quantum field theories (TQFTs) are close to being a model of a quantum lambda theory, but not quite.

There’s a simpler syntax than the simply-typed lambda calculus, called universal algebra, in which one writes algebraic theories. These give rise to categories with finite products (no exponentials) , and functors from these categories to Set pick out sets with the given structure. There’s an algebraic theory of groups, and the functors pick out sets with functions that behave like unit, inverse, and multiplication. So our “programs” consist solely of operations on our data type.

TQFTs are functors from 2Cob, the theory of a commutative Frobenius algebra, to Hilb. We can look at 2Cob as defining a data type and a TQFT as a quantum implementation of the type. When we take the free SMCC over 2Cob, we ought to get a full-fledged quantum programming language with a commutative Frobenius algebra data type. A TQFT would be part of the implementation of the language.

moietysaid, on 2006 August 24 at 5:18 pmRight.

The one thing that’s obvious is that these posts, perhaps this blog, is a tool that’s assisting in the evolution and construction of your thesis.

Beyond that I begin to despair that I’ll ever be able to understand it (that’s a challenging and discouraging thought, not out of hubris over my abilities, but out of interest in your work). The biggest discouraging factor is the scope of the total blanks I’m drawing; most of the time, I have at least a passing familiarity with the EXISTANCE of the concepts you mention, and perhaps a general sense of where they fit into the ecosystem of theory and also application. I’m lost here though.

:)

mikesaid, on 2006 August 24 at 6:27 pmYeah. I’m just saying stuff here to help me work it out in my head. It assumes a LOT of background.

Followups to this thread are going on at the n-category cafe if anyone’s interested.