<p>If additive commutations are omited in MALL, it's easy to show that the size of a proof decreases with every cut-elimination step. If additive commutations are allowed, the proof is not as easy, but it was provided in the original “Linear Logic” paper. It's called Small Normalization Theorem (Corollary 4.22, p71), which says that as long as the contraction–promotion rule is not involved (which is the case in MALL) normalization holds. The argument does not rely on formulas themselves, they could be infinite (e.g. recursively defined).</p>

<p>It means that it's not possible to encode a promotion for type $\mu\alpha.\;I \;\&amp;\; A \;\&amp;\; (\alpha \otimes \alpha)$ in MALL, since it would allow for fix point combinators. Some additional recursion construct would be needed for that.</p>

<p>Note: I believe that it's possible to use MALL together with a coinduction principle (introduction of $\mu$'s dual) to keep the system normalizing and obtain a promotion for this encoding of $!A$. Allowing recursive types in <em>MALL + coinduction</em> would then make it Turing complete. But as long as MALL is considered alone, allowing recursive types is not a big deal.</p>

CC BY-SA 3.0
2013-01-13T17:47:05.593Z
Also notice that the suggested type is briefly mentioned on page 101 (last page) of the paper.
Stéphane Gimenez
CC BY-SA 3.0
2013-01-13T16:47:26.463Z
2013-01-13T16:47:26.463Z
Stéphane Gimenez
<p>If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator:
$$
\begin{array}{lcl}
\omega &amp; = &amp; (\lambda x.\,x\;x)\;(\lambda x.\,x\;x)\\ 
Y &amp; = &amp; \lambda f.\,(\lambda x.\,f\;(x\;x))\; (\lambda x.\,f\;(x\;x)) \\
\end{array}
$$
It's clear that all of these combinators end up duplicating a variable somewhere in their definition. </p>

<p>Furthermore, all of these combinators are typeable in the simply-typed lambda calculus, if you extend it with recursive types $\mu\alpha.\,A(\alpha)$, where $\alpha$ is allowed to occur negatively in the recursive type. </p>

<p>However, what happens if you add full (negative-occurence) recursive types to the exponential-free fragment of linear logic (i.e., MALL)? </p>

<p>Then you don't have an exponential $!A$ to give you contraction. You can encode the <em>type</em> of exponentials using something like 
$$
!A \triangleq \mu\alpha.\;I \;\&amp;\; A \;\&amp;\; (\alpha \otimes \alpha)
$$
but I don't see how to define the introduction rule for it, since that seems to require a fixed point combinator to define. And I was trying to define exponentials, to get contraction, to get a fixed-point combinator!</p>

<p>Is it the case that MALL plus unrestricted recursive types is still normalizing‽</p>

CC BY-SA 3.0
2013-01-08T15:03:27.270Z
I was thinking about this just the other day, and spent a few hours toying with some ideas but could neither find a way to express a recursive value nor convince myself it wasn't possible. My intuition is that it's not! I didn't consider the other direction though--if you assume the introduction rule for ! and recursive types, does that let you define a fixed-point combinator?
C. A. McCann
CC BY-SA 3.0
2013-01-10T07:34:14.603Z
I always thought that a $\lambda$-term in which every variable occurs at most once is typeable in the simply typed fragment. So that would show you cannot define a fixpoint combinator in which variables are used linearly.
Andrej Bauer
CC BY-SA 3.0
2013-01-12T11:04:42.847Z
I think you've just answered the question for MLL, but the additives $A & B$ *do* allow variables to be duplicated (linearity then implies single occurrences in reduction sequences, roughly).
Neel Krishnaswami
<lo.logic><pl.programming-languages><linear-logic>
Is MALL + unrestricted recursive types Turing-complete?
Neel Krishnaswami
# Is MALL + unrestricted recursive types Turing-complete?

(Asked by: username_0 on 2013-01-08)

If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator:
$$
\begin{array}{lcl}
\omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\;x)\\
Y & = & \lambda f.\,(\lambda x.\,f\;(x\;x))\; (\lambda x.\,f\;(x\;x)) \\
\end{array}
$$
It's clear that all of these combinators end up duplicating a variable somewhere in their definition.

Furthermore, all of these combinators are typeable in the simply-typed lambda calculus, if you extend it with recursive types $\mu\alpha.\,A(\alpha)$, where $\alpha$ is allowed to occur negatively in the recursive type.

However, what happens if you add full (negative-occurence) recursive types to the exponential-free fragment of linear logic (i.e., MALL)?

Then you don't have an exponential $!A$ to give you contraction. You can encode the *type* of exponentials using something like
$$
!A \triangleq \mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)
$$
but I don't see how to define the introduction rule for it, since that seems to require a fixed point combinator to define. And I was trying to define exponentials, to get contraction, to get a fixed-point combinator!

Is it the case that MALL plus unrestricted recursive types is still normalizing‽

**Tags:** lo.logic, pl.programming-languages, linear-logic

> **Comments:**
> **username_1**: I was thinking about this just the other day, and spent a few hours toying with some ideas but could neither find a way to express a recursive value nor convince myself it wasn't possible. My intuition is that it's not! I didn't consider the other direction though--if you assume the introduction rule for ! and recursive types, does that let you define a fixed-point combinator?  
> **username_2**: I always thought that a $\lambda$-term in which every variable occurs at most once is typeable in the simply typed fragment. So that would show you cannot define a fixpoint combinator in which variables are used linearly.  
> **username_0**: I think you've just answered the question for MLL, but the additives $A & B$ *do* allow variables to be duplicated (linearity then implies single occurrences in reduction sequences, roughly).  

---

## 1 answers

### Answer by username_3 on 2013-01-13. Score: 10 | Accepted answer

If additive commutations are omited in MALL, it's easy to show that the size of a proof decreases with every cut-elimination step. If additive commutations are allowed, the proof is not as easy, but it was provided in the original “Linear Logic” paper. It's called Small Normalization Theorem (Corollary 4.22, p71), which says that as long as the contraction–promotion rule is not involved (which is the case in MALL) normalization holds. The argument does not rely on formulas themselves, they could be infinite (e.g. recursively defined).

It means that it's not possible to encode a promotion for type $\mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$ in MALL, since it would allow for fix point combinators. Some additional recursion construct would be needed for that.

Note: I believe that it's possible to use MALL together with a coinduction principle (introduction of $\mu$'s dual) to keep the system normalizing and obtain a promotion for this encoding of $!A$. Allowing recursive types in *MALL + coinduction* would then make it Turing complete. But as long as MALL is considered alone, allowing recursive types is not a big deal.

> **Comments:**
> **username_3**: Also notice that the suggested type is briefly mentioned on page 101 (last page) of the paper.  

---

