# Is MALL + unrestricted recursive types Turing-complete?

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‽

• 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 Jan 8 '13 at 15:03
• 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 Jan 10 '13 at 7:34
• 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 Jan 12 '13 at 11:04

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.