Languages that lack contraction, weakening or exchange

Question

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange?

Under Curry-Howard isomorphism, these rules, used frequently in logic, map into programming concepts. If we denote $A, B, C \vdash D$ a program (corresponding to a natural deduction proof) that computes a value of type $D$ from inputs of types $A$, $B$ and $C$, we get:

1. Contraction: $\Gamma, A, A\vdash B$ can be transformed into $\Gamma, A\vdash B$.

   That is, a single input can be used twice.

2. Weakening: $\Gamma\vdash B$ can be transformed into $\Gamma, A\vdash B$.

   That is, it's possible to add arbitrary, unused inputs.

3. Exchange: $\Gamma_1, A, B, \Gamma_2 \vdash C$ can be transformed into $\Gamma_1, B, A, \Gamma_2 \vdash C$.

   That is, the order of inputs doesn't matter.

An example for language lacking contraction would be quantum computing. There the allowed operations can be described with unitary matrices, and duplicating a value can't be expressed as such.

It also seems to me that weakening isn't an admissible rule for quantum computing, at least in the above form, as we can't forget a value with a unitary matrix. But we could have a weaker rule such as $\Gamma\vdash B$ can be transformed into $\Gamma, A\vdash A\otimes B$, and the $A$ in the output can be dropped when extracting the results of such a computation.

The exchange rule is clearly permissible in quantum computing.

Are there any other examples, in particular a language that doesn't allow exchange, or where weakening isn't allowed even in such a weaker form?

Answer 1

As other commenters have mentioned what you are actually asking for is a language for planar string diagrams, aka monoidal categories.

But let me address your question purely from the point of view of quantum computation. Clearly in any reasonable system you would want to have an introduction rule for the tensor product -- your proposed weakening rule is just a special case of this. Note that if you have any interesting (i.e. entanglement creating) constants in your language it's not really true to say that your can just forget $A$ in the output, unless the $A$ and $B$ parts never interact.

It also not quite right to say that contraction can't be admitted. There are (many, inequivalent) maps of type $A \to A\otimes A$ which are quantum-realisable. However none of them are natural transformations, which probably you want.

There were many attempts in the early 2000s to shoe-horn quantum computing into linear logic, which were largely unsuccessful: too much of the LL structure becomes degenerate, and too little of what makes quantum work is present in bare LL.

However you asked for an example of a system which lacks these rules; an early example is Selinger's QPL http://dx.doi.org/10.1017/S0960129504004256. More or less every other proposed quantum programming language that actually has a type system will disallow contraction and weakening for quantum data.

If you want to get rid of the exchange rule you might be interested in the field of topological quantum computing. In this setting the unitary operations are constructed from braidings; so the exchange rule is replaced by the braiding.

Answer 2

If you remove all those rules and add something like

• If $A \vdash B$ and $A' \vdash B'$ then $A, A' \vdash B, B'$

you get a logic essentially for monoidal categories (it's basically string diagrams in a sequent form). As a concrete example, you can imagine that the propositions are endo-functors and $,$ is composition.