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‽

  • $\begingroup$ 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? $\endgroup$ Jan 8, 2013 at 15:03
  • 2
    $\begingroup$ 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. $\endgroup$ Jan 10, 2013 at 7:34
  • 2
    $\begingroup$ 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). $\endgroup$ Jan 12, 2013 at 11:04

1 Answer 1


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.

  • 1
    $\begingroup$ Also notice that the suggested type is briefly mentioned on page 101 (last page) of the paper. $\endgroup$ Jan 13, 2013 at 17:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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