Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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‽

share|improve this question
    
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
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. –  Andrej Bauer Jan 10 '13 at 7:34
2  
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
add comment

1 Answer

up vote 7 down vote accepted

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.

share|improve this answer
1  
Also notice that the suggested type is briefly mentioned on page 101 (last page) of the paper. –  Stéphane Gimenez Jan 13 '13 at 17:47
1  
This is fantastic. Thank you! –  Neel Krishnaswami Jan 13 '13 at 19:02
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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