How is Fredkin and Toffoli's Conservative Logic related to Linear Logic?

Question

In the answers to this question, Timothy Gowers asks:

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning?

One answer to this question is given by Fredkin and Toffoli's conservative logic, which is an attempt to give a system of digital logic consistent with various abstract physical principles such as conservation laws, reversibility, and one-to-one composition (ie, no unbounded fanout, since signal strength degrades when signals are split). However, to a proof theorist, the constraints they describe sound hauntingly similar to the language used to motivate linear logic. Furthemore, the circuit diagrams they draw look like string diagrams in monoidal categories, which are models of linear logic.

So my own question is, how is conservative logic related to linear logic?

Answer 1

The question seems to be groping for a fancy, specific answer when, in my view, the most important connection is relatively basic and general.

In mathematics, as you say, you have symmetric monoidal categories. A word in a symmetric monoidal category has a set of inputs and a set of outputs and a certain type of labelled graph in between them. Symmetric monoidal categories are used in many situations. They were inspired by multilinear algebra with tensors; I gather that they are also important in linear logic.

In theoretical computer science, there is the notion of a circuit, and the closely related notion of a straight-line program. A circuit is also a labelled acyclic graph with inputs and outputs. Computer scientists began with boolean circuits, but these days there are a lot of study of arithmetic circuits over any ring, as well as quantum circuits composed of unitary gates. A precursor to quantum circuits is the clever definition of reversible and conservative circuits of Toffoli and Fredkin. In the paper cited, they have in mind a dynamical interpretation of graphs that don't have to be acyclic. However, the case of what they did that has had the most influence is finite, acyclic graphs. In this case, their essential insight is that you can have a perfectly good model of boolean circuits based on permutations of $\{0,1\}^n$ rather than functions from $\{0,1\}^a$ to $\{0,1\}^b$.

So the point is that the math concept of monoidal categories, which are broadly important, is basically the same as the CS concept of circuits, which are also broadly important. Every monoidal category, maybe together with some distinguished generators, gives you a new type of circuit, so that you can then ask circuit complexity questions. A particular monoidal category may or may not yield interesting circuit questions, and two different monoidal categories might yield equivalent circuit questions. Nonetheless, there are many interesting different cases.

Actually, not-necessarily-acyclic graphs can also be interpreted as words in symmetric monoidal categories that are also "closed" or "pivotal". There are several ways to interpret tensor words of this type as circuits; one of these ways (for some types of words) is as dynamical circuits.

Linear logic and conservative logic are both called "logic", and they both use monoidal categories. (Also, as Peter Shor mentioned, linear logic is partly inspired by quantum probability, while conservative logic is used in quantum computation.) Other than that, they don't look particularly related to me.