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‽
