Physics, Topology, Logic and Computation: a Rosetta Stone

March 11, 2008

Physics, Topology, Logic and Computation: a Rosetta Stone

Posted by John Baez

$MathML-enabled post (click for more details).$

It’s done!

John Baez and Mike Stay, Physics, topology, logic and computation: a Rosetta Stone.

Learn how category theory serves as a lingua franca that lets us translate between certain aspects of these four subjects… and perhaps, eventually, build a general science of systems and processes! In a nutshell, it goes like this:

$\begin{matrix} object & morphism \\ Physics & system & process \\ Topology & manifold & cobordism \\ Logic & proposition & proof \\ Computation & data type & program \end{matrix}$

It takes a while to explain the details.

$MathML-enabled post (click for more details).$

Actually, I’ve come to feel that in academia no project is ever really done. At least, not until you lose interest or die — which, come to think of it, is just an extreme case of losing interest. There’s always room for revising, improving, extending, and otherwise revisiting old projects. This is particularly evident with the rise of electronic media like the arXiv. When you catch the umpteenth typo, do you put up yet another version of your paper or not? It just depends how much you care.

There are certainly lots of typos still lurking in this paper, and probably much worse problems. But, we’ve tried to take all your comments into account — sometimes by judiciously not doing anything about them — and I feel they’ve vastly improved the paper. Thanks, all of you! We could never have done it without all you logicians and computer scientists.

Posted at March 11, 2008 5:47 AM UTC

TrackBack URL for this Entry: http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1629

90 Comments & 0 Trackbacks

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Hi John!

If I am very patient, may I be able to write Windows XP using manifolds and cobordisms? What would be the blue screen of death? How would I halt a program?

I am not joking.

Posted by: Daniel de França MTd2 on March 11, 2008 2:00 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Daniel wrote:

If I am very patient, may I be able to write Windows XP using manifolds and cobordisms?

If string theory is correct, Windows XP already runs using manifolds and cobordisms. If loop quantum gravity is correct, it’s using something a bit different, but very similar: spin networks and spin foams.

If Microsoft’s Project Q succeeds, and you’re very patient, you may someday use a version of Windows XP that runs using a modular tensor category implemented via the fractional quantum Hall effect. Read the conclusions of our paper!

But, you may have switched to Vista by then.

Posted by: John Baez on March 11, 2008 9:01 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Let’s pose a variant then on Daniel’s question.

I took it he was wondering, given the structural similarity between manifolds/cobordisms and data type/program, whether an actually used program could be seen ‘in principle’ as a highly complex manifold?

In view of the complex three-dimensional pictures as shown on page 31 of Yves Giraud’s The Three Dimensions of Proof for very simple operations, Windows XP, or some equivalent in a functional programming language, would be truly monumental.

But what could be said, in whatever stretched sense of ‘in principle’, about the relation between the cobordism which is the program operating on an input and the cobordism which might be the physics underlying a running of the program as seen by quantum gravity?

I take it that your reply points to an ultimate convergence between the physical and program cobordism.

Posted by: David Corfield on March 12, 2008 12:14 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

“In view of the complex three-dimensional pictures as shown on page 31 of Yves Giraud’s The Three Dimensions of Proof for very simple operations, Windows XP, or some equivalent in a functional programming language, would be truly monumental.”

Interesting article. At first, it resembled me Citanovic’Birdtrack notation. http://www.nbi.dk/GroupTheory/ It was one of John’s last years’s XMas gifts.

Guess what? Yves did use Birdtrack notation (you can also call it Penrose notation)! See page 29. And more, his point was to extend to 3 dimensions.

Now, let´s brainstorm here. Birdtrack notation is used to represent tensors ia much compact way. So, maybe we could have some intermadiate steps like:

tensors > birdtrack notation > (generalize) > Yves 3D notation > logic

according to roseta stone, topology can be translated into logic, so :
Yves 3D notation > Topology > generalized (?) tensors.

I hope it makes 0.1% of sense…

Posted by: Daniel de França MTd2 on March 12, 2008 2:22 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Although I doubt anyone will be confused, just to note that in the functional programming community the term Bird-track used to be used sometimes to refer to a particular style of literate programming (acquiring its name from Richard Bird of the Oxford comlab). It’s seldom used now, but if you’re reading old usenet threads, etc… don’t think you’ve stumbled upon some hidden application of graphical notation.

Posted by: bane on March 13, 2008 4:31 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Anyway it would be nice to see a couple examples of programs written using monoidal closed combinator calculus. :) Is it possible or I talk nonsence?

Posted by: osman on March 12, 2008 12:50 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Let me introduce my (maybe naive, I am not mathematician) idea of modifying $λ$ -calculus in order to directly forbid duplication or deletion data. In case of $λ$ -calculus the aplication ( $β$ -reduction) rule substitutes all occurences of $x$ in $F [x]$ for expression $λ x : F [x]$ . In case of non-deleting calculus (let’s call it $δ$ -calculus) we 1) are not able to apply reduction rule to $δ x : F [x]$ if F has $0$ occurences of $x$ (no deletion) and 2) may replace only the first occurence of $x$ by reduction rule applied to $δ x : F [x]$ in case there are 1 or more occurences of $x$ in $F$ (no duplication).

It’s interesting if it’s possible to write monoidal closed combinators using such $δ$ -calculus.

I’m sorry if this is totally nonsence…

Posted by: osman on March 12, 2008 4:36 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

It’s not nonsense at all; it’s called linear lambda calculus, and we talk about it a little bit in the paper. We’ve also talked about it several times here on the cafe, especially in the classical vs quantum computation posts. Our original intent was to use it exclusively—John had never even heard of a combinator when we started—but the natural transformations required for a symmetric monoidal category correspond exactly to polymorphic combinators, so we went that route instead.

Posted by: Mike Stay on March 12, 2008 6:09 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

But… in Rosetta you describe SKI calculus and link between SKI and lambda-calculus. And you do not describe such link between monoidal closed combinators and linear lambda calculus - why? It would be very convenient for readers like me, for whom it’s too difficult to read special papers about linear lambda!

Posted by: osman on March 12, 2008 8:39 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Sure we do! They’re in definition 21 and 22.

Many of the combinators are irrelevant if you’re in a poset instead of a category. The important ones are B (which we call ‘compose’):

(1)

\begin{matrix} compose : (Y ⊸ Z) ⊸ (X ⊸ Y) ⊸ (X ⊸ Z) \\ compose = λ f . λ g . λ x . (f (g x)) \end{matrix}

C (which we call ‘braid’):

(2)

\begin{matrix} braid : (X ⊸ Y ⊸ Z) ⊸ (Y ⊸ X ⊸ Z) \\ braid = λ f . λ y . λ x . ((f x) y) \end{matrix}

and I (which we call ‘id’)

(3)

\begin{matrix} id : X ⊸ X \\ id = λ x . x \end{matrix}

B, C, and I are a universal basis for linear lambda calculus like S and K are for the usual lambda calculus.

Posted by: Mike Stay on March 12, 2008 11:40 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Sorry, I don’t understand. What about comonad “!”? How to write down factorial algorithm? :)

Posted by: osman on March 13, 2008 10:17 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Sorry, I don’t understand. What about comonad “!”? How to write down factorial algorithm? :)

As John explained, we don’t use the exponential comonad ‘!’. But that doesn’t mean you can’t calculate factorial (also denoted ‘!’, unfortunately). You just have to do it in a linear way. Say you introduce an object B together with morphisms and relations among them that make B behave like a bit. Then the Toffoli and Fredkin gates are morphisms

(1)

T : B \otimes B \otimes B \to B \otimes B \otimes B

(2)

F : B \otimes B \otimes B \to B \otimes B \otimes B

that are universal for classical computation.

Assuming you have enough memory (i.e. enough copies of B) to store the intermediate results, you can compute any computable function.

Posted by: Mike Stay on March 14, 2008 11:42 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Mike Stay wrote: also denoted ‘!’ unfortunately

I forget about that! No, of course I mean any other classical algorithm. As far as I understood comonad ‘!’ is needed for something like “duplication” or “deletion” in “monoidal” part. I did not mean it is directly linked to factorial algorithm. :)

Yes, I know about gates. But I thought it’s possible to make primitive recursion inside monoidal category in some way.

Posted by: osman on March 15, 2008 6:28 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

This is inside the monoidal category. The Toffoli and Fredkin gates are two morphisms in the category.

To embed classical computation into quantum computation, you first have to make the computation linear. Then the classical states form a basis for the quantum states. As long as you stick to basis vectors and don’t do any superpositions, you’ll be doing classical computation.

Then duplication and deletion are both control-NOT. Let U be the unitary operator implementing control-NOT. Then

(1)

U ∣ a, b 〉 = ∣ a, b \oplus a 〉

and in particular,

(2)

U ∣ 0,0 〉 = ∣ 0,0 〉

(3)

U ∣ 1,0 〉 = ∣ 1,1 〉 .

So if you have a qubit that you know is in the $∣ 0 〉$ state, then you can do a “classical copy” of the first bit onto the second. (Note that I said it makes a copy of the bit, not the qubit! This is equivalent to measuring the qubit and copying down the result.)

The same control-NOT can function as deletion. If you have two copies of the same bit, you can get rid of one and be left with a qubit bit you know is in the $∣ 0 〉$ state:

(4)

U ∣ 0,0 〉 = ∣ 0,0 〉

(5)

U ∣ 1,1 〉 = ∣ 1,0 〉 .

Posted by: Mike Stay on March 17, 2008 7:20 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Is it possible to express these things by modification of monoidal closed combinator calculus without making category cartesian (as described here)?

Posted by: osman on March 17, 2008 8:59 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Nothing I wrote above is cartesian. Control-NOT does not satisfy the coherence laws for duplication and deletion, because it doesn’t copy quantum state, only classical state.

Posted by: Mike Stay on March 17, 2008 10:50 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

OK, I modify my question: is it possible to express these things (control-NOT logic) by modification of monoidal closed combinator calculus? The answer is not obvious for me, unfortunately.

Posted by: osman on March 18, 2008 7:11 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

is it possible to express these things (control-NOT logic) by modification of monoidal closed combinator calculus?

I’m not sure what you mean by “modification”. If you mean, “Is the typical gate-based approach to quantum computation a symmetric monoidal closed category?”, then yes, it is. It’s a strict dagger closed category. (See section 2.7.)

There’s a qubit type, say $Q,$ and all the objects in the category are finite tensor products of these: $1,$ $Q,$ $Q \otimes Q,$ $Q \otimes Q \otimes Q, \dots$ There’s an internal hom type $X ⊸ Y = X^{*} \otimes Y ≅ X \otimes Y .$

When you’re interpreting this stuff in Hilb (i.e. as quantum computation) then the morphisms of the category are matrices with complex elements. For example, the control-NOT gate $U$ looks like

(1)

U = (\begin{matrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{matrix}) .

Say $X = Q^{\otimes n}$ and $Y = Q^{\otimes m} .$ The $n m$ elements of a matrix in $hom (X, Y)$ can be stored (up to normalization) in the $n m$ elements of a state in $X \otimes Y .$ For example, the matrix

(2)

V = (\begin{matrix} a & b \\ c & d \end{matrix})

gets represented as a state

(3)

∣ V 〉 = (\begin{matrix} a \\ b \\ c \\ d \end{matrix}) .

Gate teleportation is the protocol filling the role of “eval”. It takes the state

(4)

∣ V 〉 ∣ x 〉

to the state

(5)

∣ random 〉 ∣ V x 〉 .

(Actually, it’s a little more complicated than that: there are some corrections that have to be made related to the random bits, but I won’t go into that unless you really want the details.)

Posted by: Mike Stay on March 18, 2008 6:04 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

No, I mean combinator calculus. For example, extend your Definition 22 by following rules:

If $X$ is type then $meas (X)$ is type. If $X$ is type then following polymorphic combinators give terms:

dup : meas (X) ⊸ meas (X) \otimes meas (X)

$del : meas (X) \otimes meas (X) ⊸ meas (X)$ .

or something like that, in more details. Maybe directly add cartesian projections for $meas (X) \otimes meas (Y)$ , I don’t know.

Posted by: osman on March 18, 2008 8:32 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

No, I mean combinator calculus.

That is combinator calculus. Gates are combinators.

If $X$ is type then $meas (X)$ is type.

Sure, your “meas” is the same thing as the exponential “!”. Just follow the Curry-Howard isomorphism across from linear logic to computer science and you’ll get the combinator you want.

The thing is, you can leave out “!” because measuring the state of a system $X$ is the same as entangling $X$ with $Y$ and then tracing out (ignoring) $Y$ . That’s the whole point of the quantum eraser experiments.

Posted by: Mike Stay on March 18, 2008 9:43 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

My problem is following: I am not scientist. I am 35yo-C-coder-from-deep-Russia. I started very-slow-self-learning in Category Theory 3 years ago just because I want to know the-most-powerful-method-to-understand-the-world-where-I-live. So these things about quantum entaglement are a little bit difficult for me (but of course I’ll try to understand them, ignoring the fact that Hilbert space is quite non-intuitive thing for me).

I just think that if I would see the complete version of combinator calculus with meas, dup and del, it would be more easy for me to understand other things related to generalized computations. :) Thank you!

Posted by: osman on March 18, 2008 10:29 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

I just think that if I would see the complete version of combinator calculus with meas, dup and del, it would be more easy for me to understand other things related to generalized computations. :) Thank you!

Well, take the last four inference rules on page 4 here and add the corresponding polymorphic combinators and rewrite rules to definition 22. Those four rules allow duplication and deletion of measured systems.

Posted by: Mike Stay on March 18, 2008 10:52 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

I obtained following combinators:

${weak}_{X} : Y ⊸ (! X ⊸ Y)$ : weak_x y = (!x y)
$contr : (! A \otimes! A ⊸ B) ⊸ (! A ⊸ B)$ : contr ((!x ⊗ !x) y) = (!x y)
$derel : (A ⊸ B) ⊸ (! A ⊸ B)$ : derel (x y) = (!x y)
$prom : A ⊸! A$ : prom x = !x

And some preliminary questions:

Is it OK (especially ${weak}_{X}$ )?
Isn’t $derel$ just “ $prom ⊸ B$ ”?
How to duplicate?

Posted by: osman on March 19, 2008 9:24 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Maybe using evaluation we could convert ${weak}_{X}$ into form :

$weak :! X \otimes Y ⊸ Y$ : weak (!x y) = y

Posted by: osman on March 19, 2008 9:42 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

And it looks like $contr$ depends on $weak$ , because contr ((!x ⊗ !x) y) = (weak (!x ⊗ !x)) y. So if I am right we have only 2 independent combinators: $weak$ and $prom$ ?

Posted by: osman on March 19, 2008 10:02 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

I’m sorry, this everyting was wrong. OK, I’ll wait for some paper. Thank you everybody.

Posted by: osman on March 20, 2008 3:20 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Is closed *-autonomous category (and corresponding combinator calculus) exactly what am I looking for? If so I think I have enought information.

Posted by: osman on March 19, 2008 2:18 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

And, to “follow from linear logic” is (maybe) not enough for me. I would like to know what kind of “closeness” or “adjointness” does it mean, how “natural” is linear logic from CT point of view, I would like to know the categorical meaning of any rule of this logic (which I did not know about just several days ago)

Posted by: osman on March 18, 2008 10:46 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Of course, Hilbert space is non-intuitive for me just because I have no time (and enought brain :) ) to learn categorical structuralization (or categorification, or groupoidification, or spanification) of it - this one already (or almost) exist, as I understood. May be in 5-10 years I’ll learn it. Categorical structuralization of physics is greatest progress of the human thought in this century I think.

Posted by: osman on March 19, 2008 1:38 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

I mean, is it possible to modify your closed monoidal calculus in order to add analogues of duplication and deletion, natural from quantum or cobordism point of view, and make some classical recursive algorithm?

I’m sorry that you should “decrypt” my questions. :)

Posted by: osman on March 15, 2008 8:56 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Osman wrote:

I mean, is it possible to modify your closed monoidal calculus in order to add analogues of duplication and deletion, natural from quantum or cobordism point of view, and make some classical recursive algorithm?

Sure! We’re describing a generalization of the ordinary untyped lambda calculus, so it’s easy to specialize back to that familiar case, where you can write all the programs you like.

Start with a combinator calculus of the sort we describe. For simplicity, suppose there’s one basic type $X$ (and all the types formed from this by $\otimes$ and $⊸$ ). This gives a closed symmetric monoidal category containing one object $X$ (and all the objects formed from this using the tensor product and internal hom).

Then, put in polymorphic combinators for duplication and deletion, and suitable rewrite rules. This ensures that your symmetric monoidal category is cartesian. So, now you’re back to the usual simply typed lambda calculus!

Then, put in terms

$α : X ⊸ (X ⊸ X)$ $α^{- 1} : (X ⊸ X) ⊸ X$

and rewrite rules saying these are inverses. Now you’re back to the usual ‘untyped’ lambda calculus, where you can apply any term to any other. So, now you write all the programs you want.

A bunch of this is explained here and elsewhere in the notes from our 2006-2007 seminar on this subject. I suppose it would be good to include a few sentences in the paper saying what I just said.

When one gets deeply involved in a subject, things start seeming ‘obvious’ that aren’t obvious to anyone else! This is a major reason it’s hard to explain things. I’m sure the stuff I just wrote would not have made sense to me a few years ago. When I write expository papers I always try to place myself back into the mental position I occupied before I learned what I’m explaining. But, sometimes I forget to do this.

Posted by: John Baez on March 15, 2008 10:25 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Thank you, but I’m afraid this is obvious what you said here. I supposed there is a “trick” that allows us to leave the category non-cartesian an anyway make some recursive computations. As I see it was my mistake.

I’m impressed with your patience to me, thanks a lot.

Posted by: osman on March 16, 2008 8:22 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Oh, my English again…

I mean I thought there is a trick allowing us to keep category non-cartesian but perform classical computations.

Posted by: osman on March 17, 2008 6:08 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Osman wrote:

I thought there is a trick allowing us to keep category non-cartesian but perform classical computations.

There are probably various tricks like this. The simplest one would be something like this: instead of making the whole category cartesian, make a specific object $X$ act cartesian by equipping it with its own personal duplication and deletion morphisms:

$Δ : X \to X \otimes X$ $! : X \to I$

You want these to make $X$ into a comonoid, at the very least. Then, if you also have an isomorphism

$α : X \to (X ⊸ X)$

you’re getting close enough to the untyped lambda calculus that you have a chance of building a universal computer using $X$ . But I’m sure some extra conditions must be required too, guaranteeing that the closed monoidal subcategory generated by $X$ , $Δ$ , $!$ and $α$ is sufficiently ‘free’.

There are probably other more interesting tricks, too…

Posted by: John Baez on April 7, 2008 9:48 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Osman wrote approximately:

Sorry, I don’t understand. What about the comonad “!”?

If you read the introduction to this paper, you’ll see we limit ourselves to explaining a very simple flavor of categories — symmetric monoidal closed categories — from four viewpoints: quantum physics, the topology of cobordisms and tangles, multiplicative intuitionistic linear logic, and a version of the combinator calculus.

If we tried to do more, the paper would become too long. It would become the book I someday want to write!

So, in the sections on logic and computation we avoid the comonad ‘ $!$ ’, even though it’s very important in linear logic. We’re only talking about the fragment of linear logic that applies to any symmetric monoidal closed category: ‘multiplicative intuitionistic linear logic’.

Posted by: John Baez on March 13, 2008 8:54 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Osman wrote:

And you do not describe such link between monoidal closed combinators and linear lambda calculus - why?

I explained why in the beginning of the section on computation:

Various flavors of ‘linear’ or ‘quantum’ lambda calculus have already been studied, for example by Benton, Bierman de Paiva and Hyland [ref], Dorca and van Tonder [ref], and Selinger [ref]. In the sections that follow we shall take a slightly different tack and consider a linear version, not of the lambda calculus, but of ‘combinatory logic’.

[…explanation of combinatory logic…]

It is a bit irksome to avoid duplication or deletion of data in the lambda calculus, since we need to count how many times each variable gets used. It is easier in combinatory logic: we just need to avoid combinators that duplicate or delete data.

We could have talked about a linear version of the lambda calculus, and that’s what I originally wanted to do. But Mike pointed out that it’s easier to avoid duplication and deletion of data using a combinator calculus. Combinators are like basic ‘building blocks’ that you stick together to form bigger programs; if these building blocks don’t delete or duplicate data, neither will the bigger programs. In the lambda calculus we need to count how many times each variable gets used, and make sure it gets used just once. Stating this precisely requires an annoying (but typical) detour into free versus bound variables. Furthermore, the constraint that each variable gets used once is slightly ‘nonlocal’. So, Mike convinced me that the combinator approach is better.

If we’d had time, I would have explained how to translate any expression in our ‘closed symmetric monoidal combinator calculus’ into a lambda-term. The resulting lambda-terms will then automatically satisfy the constraint that each variable gets used exactly once.

Posted by: John Baez on March 13, 2008 7:11 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

This is an exhaustive answer, thank you. Being a programmer (not CS-scientist) I just wanted to start writing programs with cobordisms, so I was a bit disappointed :)

Posted by: osman on March 14, 2008 3:34 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

How would I halt a program?

I have to admit that this is one part I’m not entirely clear on. There seem to be two approaches to halting, and I’d appreciate the help of the computer science people here in understanding.

The first is the normal form of a term under rewrite rules, which is entirely syntactic. A term has a normal form if the rules are confluent and terminating. This is the case for all terms in the simply-typed lambda calculus, but not in the untyped lambda calculus, since we can write

(1)

(λ x . (x x)) (λ x . (x x))

which rewrites to itself.

The second is interpreting the lambda calculus using (PointedSet, $\land$ ), the symmetric monoidal closed category of pointed sets, pointed maps, and the smash product. The special point of each pointed set is ‘bottom’ ( $⊥$ ), which is used to represent the non-halting state. Pointed maps with the smash product means that if part of the computation takes forever, the whole computation takes forever.

But this means the smash product isn’t cartesian! If you interpret a cartesian closed category $C$ in (PointedSet, $\land$ ), then you have to treat the cartesian product in $C$ as merely a tensor product: you can’t talk about real parallel execution any more. The best you can do is simulate it by threading.

Then there’s some weirdness going on with extensionality, because if you’ve got a language like simply-typed lambda calculus, you may not be able to write an infinite loop, but if you interpret it in PointedSet, you still have to worry about its behavior on bottom.

There’s a thread here where Robin talks about how two programs have the same behavior on all inputs that you can define syntactically, but differ when you feed them ‘parallel or’ (por). Por is not a pointed map with the smash product, but it’s apparently a map in a Scott domain, something I’m not very familiar with. It looks like Scott domains use the cartesian product on pointed sets.

If you use the cartesian product and pick the special point to be $(⊥, ⊥),$ then a pointed map out of $X \times Y$ contains more information than a pair of pointed maps, one out of $X$ and one out of $Y$ . This is because whereas a pointed map out of $X$ has to send $⊥$ to $⊥,$ a pointed map out of $X \times Y$ can send $(⊥, y)$ (where $y$ is not $⊥$ ) to something else. (PointedSet, $\times$ ) is a symmetric monoidal category in which por is a morphism. But (PointedSet, $\times$ ) is not a closed category, so we can’t interpret lambda calculus there without throwing away closedness. Is a Scott domain closed? How?

We put extensionality into our equivalence rules for the combinator calculus. Is it necessary in order to get a symmetric monoidal closed category?

In a purely functional context like combinator calculus, what are the reduction strategies available to us? How does extensionality play into each of these?

Posted by: Mike Stay on March 12, 2008 5:03 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Just a thought, but isn’t halting intimately related to fixed points? The lambda expression above is a fixed point of the evaluation function and so can be considered to have “halted” , just like a lambda expression that evaluates to 3, which is also then at a fixed point.

Posted by: Mark Biggar on March 14, 2008 7:35 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

On the contrary, fixed points of the rewrite rules are a class of programs that do not halt. 3 isn’t a fixed point of the rewrite rules; it’s a point at which no rewrite rule applies.

Posted by: Mike Stay on March 18, 2008 12:19 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

David wrote:

Let’s pose a variant then on Daniel’s question.

I took it he was wondering, given the structural similarity between manifolds/cobordisms and data type/program, whether an actually used program could be seen ‘in principle’ as a highly complex manifold?

Well, the point of our paper is that very similar ‘string diagram’ machinery can be used to describe quantum processes, cobordisms, proofs and programs.

But, the first two examples involved compact closed categories, while the second two often involved cartesian closed categories.

What does that mean?

Very crudely, ‘compactness’ is why quantum physics allows ‘creation and annihilation of particle-antiparticle pairs’, but doesn’t allow the arbitrary duplication and deletion of lone particles.

‘Cartesianness’ is why traditional programs don’t allow ‘creation and annihilation of datum-antidatum pairs’, but do allow duplication and deletion of data.

So, there are similarities but also differences.

But, as we explain in the Conclusions, the similarities become more pronounced in quantum computation — especially topological quantum computation, like they’re trying to do in Project Q.

Posted by: John Baez on March 13, 2008 9:09 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Something about what I just wrote made me even more excited than usual about how ‘cartesianness’ lets us duplicate and delete:

$x \to x \otimes x$ $x \to 1$

while ‘compactness’ lets us create and annihilate particle-antiparticle pairs:

$x^{*} \otimes x \to 1$ $1 \to x \otimes x^{*}$

This made me ask Jim if he knew of any compact cartesian categories — that is, compact symmetric monoidal categories where the tensor product is the cartesian product and the unit object is terminal.

We soon saw the only example is the terminal category (fun little exercise).

Then Jim said this reminded him of Hawking radiation! Quantum theory lets you create and annihilate particle-antiparticle pairs. A black hole lets you ‘delete’ particles or antiparticles by throwing them down the black hole. The simple idea behind Hawking radiation is that this lets you create particles: create a particle-antiparticle pair, and then delete the antiparticle!

Here we are not using duplication, just deletion. So, I asked Jim a trickier question: are there any compact symmetric monoidal categories where the unit object is terminal?

I’ll leave this as a puzzle. If the only examples are trivial in some sense, it suggests there’s something funny about the simple story of Hawking radiation told above!

Posted by: John Baez on March 14, 2008 2:26 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

it suggests there’s something funny about the simple story of Hawking radiation told above!

But we know that, indeed, there is something funny about this way of telling the story: we know that it can’t be true literally that one member of the pair of particles is literally “deleted”. In some way or other it got to show up in the “internal state” of the black hole.

It’s that unitarity puzzle: there ought to be a way to descibe black hole formation and decay which is entirely “unitary”, meaning essentially that, globally, no deletion or creation takes place.

There are plenty of articles out there arguing that the entropy of a black hole can entirely be understood as “entanglement entropy” resulting from “tracing out” the stuff that “drops behind the horizon” (scare quotes for good reasons…).

Not sure what the canonical reference is, but this one looks reasonable:

Roberto Emparan, Black hole entropy as entanglement entropy: a holographic derivation .

By the way, I always thought of Frobenius modules as a nice analog for black hole radiation:

suppose $A$ is a Frobenius algebra and $V$ a right $A$ -module. In string diagrams this means that $A$ -lines can “be absorbed” into $V$ lines.

But that then automatically implies that $V$ -lines may “emit” $A$ -lines, namely that we also have a co-module structure on $V$ :

We start with $V$ and with the unit for $A$ to produce an $A$ “out of nothing”, then proceed with the coproduct to produce two copies of $A$ , then use the right $A$ action on $V$ to delete one of the copies. From far away this looks as if $V$ emitted an $A$ -line.

Of course this example doesn’t capture the particle/antiparticle notion.

Posted by: Urs Schreiber on March 14, 2008 9:49 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

are there any compact symmetric monoidal categories where the unit object is terminal?

Well, the functor $A \otimes -$ is right adjoint to $A^{*} \otimes -$ , hence it must preserve limits. In particular it preserves terminality: if $T$ is terminal then $A \otimes T$ is terminal too, for all objects $A$ . So, if the unit object is terminal then clearly every object is terminal, and the category is trivial.

More generally, in a (left or right) closed monoidal category, if the unit object is initial then the category must be trivial.

Also: in a compact symmetric monoidal category, if there is a terminal object $1$ then there is also an initial object $0 = 1^{*}$ . Now consider the object $0 \otimes 1$ . Since $0 \otimes -$ preserves limits, $0 \otimes 1$ must be terminal; and since $- \otimes 1$ preserves colimits, it must be initial. So it’s a zero object, which means that $0$ and $1$ are zero objects as well. The upshot is that every initial object is also terminal, and vice versa.

Posted by: Robin on March 14, 2008 11:58 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

John wrote:

…are there any compact symmetric monoidal categories where the unit object is terminal? I’ll leave this as a puzzle.

The Prince of Compact Categories replied:

Well, the functor $A \otimes -$ is right adjoint to $A^{*} \otimes$ , hence it must preserve limits. In particular it preserves terminality: if $T$ is terminal then $A \otimes T$ is terminal too, for all objects $A$ . So, if the unit object is terminal then clearly every object is terminal, and the category is trivial.

Right, that’s about how Jim did it. Being a bit of lowbrow myself, I enjoyed translating his answer into baby-talk. Others may enjoy this too:

Suppose the unit object of our compact symmetric monoidal category is terminal; let’s call it $T$ .

Since $A \otimes T ≅ A$ for any object $A$ , morphisms

$B \to A$

are in 1-1 correspondence with morphisms

$B \to A \otimes T$

By compactness, these are in 1-1 correspondence with morphisms

$A^{*} \otimes B \to T$

But, there’s only one of these, since $T$ is terminal. So, there’s only one morphism $B \to A$ so $A$ is terminal!

So, any such category is trivial (equivalent to the terminal category).

The assumption ‘symmetric’ was not necessary; I put it in just to avoid an annoying fuss about left versus right duals.

Posted by: John Baez on March 15, 2008 2:57 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Urs wrote:

we know that it can’t be true literally that one member of the pair of particles is literally “deleted”.

Maybe we know it — but it’s interesting to ask exactly why we ‘know’ it. There’s no experimental evidence on this topic, so what assumptions are we using to draw this conclusion?

It’s that unitarity puzzle: there ought to be a way to descibe black hole formation and decay which is entirely “unitary”, meaning essentially that, globally, no deletion or creation takes place.

Unitarity is a bit different than ‘no deletion’. If you’re a unitarian, you believe that the universe is described by a dagger-category, but that the only ‘physically possible’ morphisms are the unitary ones: that is, those with:

$f^{†} f = 1$ $f f^{†} = 1$

I don’t know a good a priori argument for unitarianism. It seems to work very well in ordinary life. But, in plenty of more far-out theories, like topological quantum field theories, we have a dagger-category but also treat nonunitary processes as physically possible. (These typically involve topology change.)

The argument I sketched proceeds along different lines: it says that any universe described by a compact monoidal category with a terminal object must be completely, utterly dull!

It’s not a very fleshed-out argument, just an idea for one. I don’t actually think a black hole should be modeled as a ‘terminal object’. But, you can imagine trying to describe the idea of a ‘perfect garbage dump’, where you can throw anything in and have all its information lost (or all but mass, angular momentum and charge)… and then trying to derive some paradox or problem from this assumption, and other assumptions.

Trying to formalize the idea of a ‘black hole as perfect garbage dump’ reminds me of a very interesting section in Sommerfeld’s Optics where he tries to define what it means for an object to be ‘black’. In other words: what boundary conditions for Maxwell’s equations correspond to a perfectly black surface? It turns out to be a hard problem. I’m not sure why: perhaps because a purely passive entity would violate reciprocity.

Posted by: John Baez on March 15, 2008 3:10 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Related question: how many category theorists visualize terminal objects as black and initial objects as white? I think I do.

Posted by: John Baez on March 15, 2008 3:22 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

A tiny request and a question:

- could we get page numbers? Would help in taking notes

- could we imagine adding inference to the Rosetta stone? I mean I’m sure there could be many other additions to such a general programme, but this is one I’d love to see. Of the many possible choices for the objects/morphisms I’d pick Bayesian style names (beliefs/updates?; propositions/inferences?). I’m very biased, but I’d put inference in the middle of the stone. Maybe someone could attribute this quote I once heard:

“First God invented Bayes rule, then he drew his pistol!”

Posted by: Allan E on March 16, 2008 7:32 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Allan wrote:

could we get page numbers?

Yes! You’ve got ‘em now! I apologize to everyone for not including them sooner; I didn’t want to mess with the publisher’s format until the paper had reached a reasonably stable state.

could we imagine adding inference to the Rosetta stone?

I can imagine it… but does it really work? I’d say it ‘works’ if we can describe closed symmetric monoidal categories where ‘beliefs’ are objects and ‘updates’ are morphisms — or something like that. I don’t see precisely how it should go. Has anyone tried something like this?

As for a closed symmetric monoidal category of ‘propositions’ and ‘inferences’, that’s sort of what the logic section is all about. But, sadly, I don’t really understand how Bayesian inference connects to proof theory. Maybe this has something to do with David’s ‘progic’ project?

Posted by: John Baez on March 16, 2008 9:48 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

A good place to start on relating inference to physical processes is belief propagation, which has as special cases

the forward-backward algorithm, the Viterbi algorithm, iterative decoding algorithms for Gallagher codes and turbocodes, Pearl’s belief propagation algorithm for Bayesian networks, the Kalman filter, and the transfer-matrix approach in physics.

In an ideal world I’d get down to understanding belief propagation in terms of information geometry.

Posted by: David Corfield on March 19, 2008 10:01 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Dear John Baez,

It seems an interesting paper, I’ll read it opportunely.

I wonder whether concurrent processes would have a place in your Table 4. I see that you have an analogy scheme for parallel processes. That is, processes that do not compete with themselves and proceed independently (uncoupled) . In the case of concurrent processes, they compete for common resources in order to achieve some computational objective (they are coupled in some sense). Directed topology (“ditopology”) has been introduced recently as a technique to help verifying concurrent computation, the presence of deadlocks, etc. It would be reasonable to think about concurrent processes as parallel processes with more structure, right? What would be the correspondence of such systems with other concepts in category theory, physics, etc?

I wonder about the relevancy of concurrent processes in physics, in particular.

Thanks
Christine

Posted by: Christine Dantas on March 17, 2008 7:55 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Last week I had lunch with Carl Hewitt and discussed with him the relationship between the actor model and physics. Hewitt had in mind creation and annihilation operators when conceiving of message passing: one actor “emits” a message, while another “aborbs” the message, and these particles can move around each other. Upon receipt or emission of a message, an actor’s ‘behavior’ changes, but is still considered to be the same actor.

We can get a monoidal category from this by having an object X be “an actor with behavior X” and morphisms be either sending a message

(1)

a^{*} : X \to X^{'} \otimes M

or receiving a message

(2)

a : X \otimes M \to X^{'} .

So roughly, a lambda calculus term is a description of one possible ordering of messages being sent and received. Denotational semantics talks about all possible orderings.

Feynman diagrams were invented to keep track of this kind of thing: each diagram keeps track of one way two systems can interact. The rules of the game tell you how to get all possible interactions.

In physics, more complicated interactions are less probable. This is somewhat related to algorithmic information theory, in that the number of interactions gives a notion of the length of the program, and the probability of each drops off exponentially with the number of interactions or instructions.

Now, since this is the n-Category Café, we really have higher categories in mind. Typed lambda calculus gives a 2-category with objects from types, morphisms from terms, and 2-morphisms from rewrite rules. These rewrite rules happen to be confluent for lambda calculus, so it doesn’t matter in which order you apply them.

The actor model gives a 2-category with objects from types, morphisms from behaviors, and 2-morphisms from sending/receiving a message. These 2-morphisms are not confluent, so you can model two actors vying for the same resource.

Note that in the comparison above, I had to use 1-categories, and the way I got 1-categories from each of these 2-categories was different. With lambda calculus, we can get rid of the 2-morphisms by taking equivalence classes; this is possible because the rewrite rules are confluent.

With the actor model, they’re not confluent, so I had to get rid of the lowest level, the types, instead. I did it by declaring all data types to be isomorphic: every data type is just bits.

Posted by: Mike Stay on March 17, 2008 10:41 PM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

As to ditopology, I do not know what the current `best model’ for concurrency is from that direction.

In a paper on the Dagstuhl seminar/conference site, I did look at using simplicially enriched categories and then using bar/cobar type constructions to get a DG category rather as is used in work by Lazaroiu. (My paper is at
kathrin.dagstuhl.de/files/Materials/06/06341/06341.PorterTimothy.Paper!!.pdf)
There may be other papers on that site with relevance to Christine’s question.
The relevant details for that meeting were:

date 20.08.-25.08.06, Seminar Nº 06341

Computational Structures for Modelling Space, Time and Causality

organised by R. Kopperman (City University of New York, US), P. Panangaden (McGill University - Montreal, CA), M. B. Smyth (Imperial College London, GB), D. Spreen (Univ. Siegen, DE)

There are mostly just the abstracts there but there are also links to the proceedings (DROPS submission) for some of the participants.

Posted by: Tim Porter on March 19, 2008 8:57 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

Here’s a quick note, disagreeing with one of your constructions. In 1.4.2, you translate a programming language into a closed monoidal category, and I was nodding and agreeing that your translation did what I would expect a dictionary to do until I got to the last generator for the equivalence relation on morphisms:

“ if terms are “extensionally equivalent”, they are equivalent. Here we say f:(X \to Y) and f’:(X \to Y) are extensionally equivalent if (f x):Y and (f’ x):Y are equivalent for all terms x:X. ”

Certainly you get a closed monoidal category using your scheme. But you get (I argue) the wrong one: in particular, you still get a closed monoidal category without the extensionality condition.

Let me give an example:

In the category SVect, the objects are super-vector spaces (Z/2-graded vector spaces) and the morphisms are grading-preserving linear maps (“even” maps). The internal hom between two svector spaces? That’s the svector space of all linear maps. (In particular, External Hom is not Forget applied to Internal Hom.)

The monoidal structure is tensor, where the product of two (-1)-graded parts is (+1)-graded. (The braiding, which I don’t need for this discussion, is the usual flip map, with a sign when I braid an odd thing past an odd thing.) The unit object is still just \R, but, for example, there is only the zero morphism from this unit object to a purely-odd vector space like \R^{(0|1)} = 0 \oplus \R, where the \R has odd grading.

In particular, given a space X, then (external hom) maps from the unit object into X pick up just the even (i.e., (+1)-graded) elements; they’re not enough to get all elements. Your “extensionally equivalent” condition loses information, when applied to this category: it says that two functions agree if they agree on all even elements.

So if I translate SVect into a programming language using the method you outline, and then translate back into a category, I get back Vect of (ungraded) vector spaces, not SVect; moreover, this is not the forgetful function SVect \to Vect that forgets the grading, but rather the “reduce” functor (I can’t call it “Forget”, because it is not fully faithful) that forgets the odd part of the space.

Posted by: Theo on March 23, 2008 1:30 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

SVect is also a good example where the re-write rule should not be “(((braid f) x) y) = ((f y) x)”, even though the braiding is symmetric.

Posted by: Theo on March 23, 2008 1:33 AM | Permalink | Reply to this

Re: Physics, Topology, Logic and Computation: a Rosetta Stone

$MathML-enabled post (click for more details).$

Theo’s got a point. The general idea is that if one wants to argue “elementwise” in category theory, one should be

The n-Category Café

Skip to the Main Content

March 11, 2008