3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I'm not sure I understand the question, but the Wikipedia article you link to mentions substructural logics, which are also discussed in SEP: 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. $\endgroup$ – Radu GRIGore Aug 5 '17 at 20:18
  • 1
    $\begingroup$ 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) 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)? $\endgroup$ – Damiano Mazza Aug 6 '17 at 5:03
  • $\begingroup$ @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. $\endgroup$ – Petr Pudlák Aug 6 '17 at 13:57
  • $\begingroup$ @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. $\endgroup$ – Petr Pudlák Aug 6 '17 at 14:00
  • 1
    $\begingroup$ So you prefer programming languages to logics. Haskell with linear types, then? ghc.haskell.org/trac/ghc/wiki/LinearTypes $\endgroup$ – Radu GRIGore Aug 6 '17 at 18:32
4
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Max New Aug 7 '17 at 15:07
  • $\begingroup$ Yeah, you're right. Should be monoidal categories. $\endgroup$ – Izaak Meckler Aug 7 '17 at 15:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.