The n-Category Café

So $\beta$-reduction and ‘The day ends’ share a common structure.

Returning to precise disciplines, there remains the small problem of relating this to fundamental $n$-categories of statified spaces, the kind of thing we talked about back here. Can one see $\beta$-reduction in terms of a stratified space?

David wrote:

Can one see β-reduction in terms of a stratified space?

That’s a fun question!

I hope stratified spaces give $n$-categories with duals, and there’s some evidence for this. An example is a symmetric monoidal category with duals, as defined below. These are relevant to quantum logic and the ‘quantum λ-calculus’.

Lately I’ve been catching up on the ‘classical λ-calculus’, and today’s class only discussed this. This is all about cartesian closed categories.

So: if we want to relate β-reduction to stratified spaces, it’ll work more smoothly if we consider β-reduction in the quantum λ-calculus!

If we did that, I would not have to draw ‘bubbles’ in my string diagrams and surface diagrams, as I did in today’s notes. For more on the role of these bubbles, read about popping bubbles to reveal the quantum world.

So, anyway, the answer to your question is yes: in the ‘quantum’ case, where we have a symmetric monoidal category with duals $C$, we should be able to build a stratified space whose fundamental category is $C$. And then, β-reduction in the corresponding quantum λ-calculus should really be related to fold singularities in a very direct way!

This would be fun to explore. It would really bring out the full content of the word topological.

Some reminders may be helpful, at least for people who are insufficiently fanatical about attending this Café:

Suppose $C$ is a symmetric monoidal category. Then we say:

• $C$ is closed if the functor of tensoring with any object $x\in C$: $$a\to x\otimes a$$ has a right adjoint, the internal hom $$b\to \mathrm{hom}(x,b).$$ In other words, we have a natural isomorphism $$\mathrm{HOM}(x\otimes a,b)\cong \mathrm{HOM}(a,\mathrm{hom}(x,b)).$$ Here HOM denotes the usual set of morphisms from one object to another, while hom is the “internal hom”, which is an object in our category. If the tensor product in $C$ is cartesian, and $C$ is also closed, we call it cartesian closed.
• $C$ has duals for objects if it is closed and for any object $x\in C$ there is an object $x^{*}\in C$, the dual of $x$, such that $$\mathrm{hom}(x,b)\cong x^{*}\otimes b$$ for all $b\in C$. If $C$ has duals for objects, it’s common for category theorists to say $C$ is compact or compact closed; algebraic geometers say it’s rigid.
• $C$ has duals for morphisms if for any morphism $f:a\to b$ there is a morphism $f^{†}:b\to a$ such that $$f^{††}=f$$ $$(fg{)}^{†}=(gf{)}^{†}$$ $$1^{†}=1$$ and all the structural isomorphisms (the associator, the left and right unit laws, and the braiding and balancing) are unitary, where a morphism $f$ is unitary when $f^{†}$ is the inverse of $f$.
• $C$ has duals if it has duals for objects and morphisms. If $C$ has duals, Abramsky and Coecke call it strongly compact closed, while Selinger calls it dagger compact closed.

The category of finite-dimensional Hilbert spaces is symmetric monoidal, and it has duals. The same is true for $n\mathrm{Cob}$, whose morphisms are $n$-dimensional cobordisms, like this (for $n$ = 2):

On 4/24/07, John Baez wrote:

Thanks! It’s an interesting paper, but I’ll need to learn about the “polymorphic” lambda-calculus and some other stuff before really appreciating it.

Encapsulation, inheritance and polymorphism are the three things that object-oriented programming brought to imperative languages like C or Fortran.

(Parametric) polymorphism is a second-order concept. It lets you give datatypes as inputs to other datatypes, not just as inputs to function symbols.

For instance, consider lists. A list datatype should have some function symbols that act on it. We’d like to be able to - append an element to the list - project onto the nth element of the list - get the list length - etc.

Notice that I never said what type an element is! In the first-order lambda calculus, I’d have to specify what the output datatype of the projection function symbol is. Here, it shouldn’t matter: the projections should work the same way no matter what the element type is.

The element datatype becomes a parameter in the definition of a list, and we can use the same function symbols on many differently-shaped objects. Thus “parametric polymorphism”.