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

<p>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.</p>

<p>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.</p>

<p>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.</p>

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

<p>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 <em>braidings</em>; so the exchange rule is replaced by the braiding.</p>

CC BY-SA 3.0
2017-08-09T16:53:45.427Z
2017-08-09T16:53:45.427Z
Ross Duncan
<p>If you remove all those rules and add something like </p>

<ul>
<li>If $A \vdash B$ and $A' \vdash B'$ then $A, A' \vdash B, B'$</li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2017-08-07T15:07:30.047Z
This looks wrong to me. If you can , any two types then you are talking about monoidal categories, which can be seen as a very special case of 2 categories.
Max New
CC BY-SA 3.0
2017-08-07T15:24:51.070Z
Yeah, you're right. Should be monoidal categories.
Izaak Meckler
CC BY-SA 3.0
2017-08-05T22:56:57.830Z
2017-08-07T15:25:04.127Z
2017-08-07T15:25:04.127Z
Izaak Meckler
<p>When learning about <a href="http://www.megacz.com/berkeley/garrows/" rel="nofollow noreferrer">generalized arrows</a>, a question arised to me: Are there any languages (or potential languages) that lack one or more of the <a href="https://en.wikipedia.org/wiki/Structural_rule" rel="nofollow noreferrer">structural rules</a>: contraction, weakeing and exchange?</p>
<p>Under <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow noreferrer">Curry-Howard isomorphism</a>, these rules, used frequently in logic, map into programming concepts. If we denote <span class="math-container">$A, B, C \vdash D$</span> a program (corresponding to a natural deduction proof) that computes a value of type <span class="math-container">$D$</span> from inputs of types <span class="math-container">$A$</span>, <span class="math-container">$B$</span> and <span class="math-container">$C$</span>, we get:</p>
<ol>
<li><p><strong>Contraction</strong>: <span class="math-container">$\Gamma, A, A\vdash B$</span> can be transformed into <span class="math-container">$\Gamma, A\vdash B$</span>.</p>
<p>That is, a single input can be used twice.</p>
</li>
<li><p><strong>Weakening</strong>: <span class="math-container">$\Gamma\vdash B$</span> can be transformed into <span class="math-container">$\Gamma, A\vdash B$</span>.</p>
<p>That is, it's possible to add arbitrary, unused inputs.</p>
</li>
<li><p><strong>Exchange</strong>: <span class="math-container">$\Gamma_1, A, B, \Gamma_2 \vdash C$</span> can be transformed into <span class="math-container">$\Gamma_1, B, A, \Gamma_2 \vdash C$</span>.</p>
<p>That is, the order of inputs doesn't matter.</p>
</li>
</ol>
<p>An example for language lacking contraction would be <a href="https://en.wikipedia.org/wiki/Quantum_computing" rel="nofollow noreferrer">quantum computing</a>. There the allowed operations can be described with <a href="https://en.wikipedia.org/wiki/Unitary_matrix" rel="nofollow noreferrer">unitary matrices</a>, and duplicating a value can't be expressed as such.</p>
<p>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 <span class="math-container">$\Gamma\vdash B$</span> can be transformed into <span class="math-container">$\Gamma, A\vdash A\otimes B$</span>, and the <span class="math-container">$A$</span> in the output can be dropped when extracting the results of such a computation.</p>
<p>The exchange rule is clearly permissible in quantum computing.</p>
<p>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?</p>

CC BY-SA 3.0
2017-08-05T20:18:16.080Z
I'm not sure I understand the question, but the Wikipedia article you link to mentions substructural logics, which are also discussed in SEP: https://plato.stanford.edu/entries/logic-substructural/ In addition, separation logic lacks Contraction, and may or may not have Weakening depending on which variant you're using.
Radu GRIGore
CC BY-SA 3.0
2017-08-06T05:03:34.340Z
I don't understand the question.  You ask for a "language", by which I assume you mean a programming language, but as an example of answer you give a computational paradigm (quantum computing).  There obviously are programming languages in which there is any combination of structural rules (including none, like the linear planar $\lambda$-calculus of [this question](https://cstheory.stackexchange.com/q/38494/20716)) and in some cases these are well known and studied (cf. linear logic), but maybe you see them as artificial and wonder whether they have any application (like quantum computing)?
Damiano Mazza
CC BY-SA 3.0
2017-08-06T13:57:21.847Z
@DamianoMazza You're right that the distinction between languages and paradigms is a bit unclear in my question. For me both suffices, in a sense. I'm more interested in actual languages. But since I don't know any particular languages for quantum computing, and any such language would be bound to its principles and lack contraction/weakening, this is enough for me as an example.
Petr
CC BY-SA 3.0
2017-08-06T14:00:58.860Z
@RaduGRIGore I'd be interested in languages that have some use or value on their own, rather than just being artificially constructed for the sake of an example. We can always take a particular logic and make it into a language using Curry-Howard isomorphism, but I'd like to know, if there are more interesting examples.
Petr
CC BY-SA 3.0
2017-08-06T18:32:53.480Z
So you prefer programming languages to logics. Haskell with linear types, then? https://ghc.haskell.org/trac/ghc/wiki/LinearTypes
Radu GRIGore
CC BY-SA 3.0
2017-08-07T12:41:09.667Z
@RaduGRIGore That looks very interesting, thanks. I'll be happy to upvote, if you make it into an answer.
Petr
<lo.logic><pl.programming-languages><curry-howard>
Languages that lack contraction, weakening or exchange
Petr
# Languages that lack contraction, weakening or exchange

(Asked by: username_0 on 2017-08-05)

When learning about [generalized arrows](http://www.megacz.com/berkeley/garrows/), a question arised to me: Are there any languages (or potential languages) that lack one or more of the [structural rules](https://en.wikipedia.org/wiki/Structural_rule): contraction, weakeing and exchange?

Under [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), 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](https://en.wikipedia.org/wiki/Quantum_computing). There the allowed operations can be described with [unitary matrices](https://en.wikipedia.org/wiki/Unitary_matrix), 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?

**Tags:** lo.logic, pl.programming-languages, curry-howard
> **Comments:**
> **username_1**: I'm not sure I understand the question, but the Wikipedia article you link to mentions substructural logics, which are also discussed in SEP: https://plato.stanford.edu/entries/logic-substructural/ In addition, separation logic lacks Contraction, and may or may not have Weakening depending on which variant you're using.  
> **username_2**: I don't understand the question.  You ask for a "language", by which I assume you mean a programming language, but as an example of answer you give a computational paradigm (quantum computing).  There obviously are programming languages in which there is any combination of structural rules (including none, like the linear planar $\lambda$-calculus of [this question](https://cstheory.stackexchange.com/q/38494/20716)) and in some cases these are well known and studied (cf. linear logic), but maybe you see them as artificial and wonder whether they have any application (like quantum computing)?  
> **username_0**: @DamianoMazza You're right that the distinction between languages and paradigms is a bit unclear in my question. For me both suffices, in a sense. I'm more interested in actual languages. But since I don't know any particular languages for quantum computing, and any such language would be bound to its principles and lack contraction/weakening, this is enough for me as an example.  
> **username_0**: @RaduGRIGore I'd be interested in languages that have some use or value on their own, rather than just being artificially constructed for the sake of an example. We can always take a particular logic and make it into a language using Curry-Howard isomorphism, but I'd like to know, if there are more interesting examples.  
> **username_1**: So you prefer programming languages to logics. Haskell with linear types, then? https://ghc.haskell.org/trac/ghc/wiki/LinearTypes  
> **username_0**: @RaduGRIGore That looks very interesting, thanks. I'll be happy to upvote, if you make it into an answer.  

---

## 2 answers

### Answer by username_3 on 2017-08-09. Score: 4 | Accepted answer

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 by username_4 on 2017-08-05. Score: 3

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.

> **Comments:**
> **username_5**: This looks wrong to me. If you can , any two types then you are talking about monoidal categories, which can be seen as a very special case of 2 categories.  
> **username_4**: Yeah, you're right. Should be monoidal categories.  

---

