selected exercises [on linear logic--ed.]

To: types
Subject: selected exercises [on linear logic--ed.]
From: andre@saul.cis.upenn.edu (Andre Scedrov)
Date: Fri, 15 Nov 91 04:41:41 EST
Sender: meyer@theory.lcs.mit.edu
Date: Wed, 13 Nov 91 20:56:17 EST
To: linear@cs.stanford.edu

Here are a few take-home final exam problems in my linear logic course 
at Penn:  

1. Let  *  denote tensor,  ~  linear negation.  Show that the sequent

           |-  A * B ,  ~A * B ,  A * ~B ,  ~A * ~B   

   is not provable in LL, although seemingly "all resources are accounted 
   for".  

2. Show that the Small Normalization Theorem implies that cut-elimination 
   in the multiplicative additive fragment (i.e., "core LL" in Gallier's 
   terminology) is at most exponential.  

3. Give a better measure than the one given in the proof of Small 
   Normalization Theorem in Girard's TCS paper on LL.  

4. Analyze confluence property for reduction of proof nets with boxes 
   for T, &, and ! .  

5. Referring to "elementary part of linear intuitionistic logic" in 
   the Girard-Lafont paper in TAPSOFT '87, SLNCS vol. 250, a sequent 
   Gamma |- A  can be translated into core LL as  |- ~ Gamma, A . 

     a) Show that this translation of the elementary part of linear 
        intuitionistic logic into core LL is not conservative. 

     b) Show that this translation of the *, -o fragment of linear 
        intuitionistic logic into core LL is conservative. 

     c) Investigate the intermediate cases.  

6. (Extra credit)  Consider "untyped" proof nets, i.e., proof nets without
   formulas, but with a labeling of links and boxes.  Use strongly 
   normalizing untyped proof nets to modify the proof of Strong 
   Normalization for 2nd order LL in Girard's TCS paper in the    
   style of Mitchell's SN proof for system F (for the latter see 
   pp. 204-206 in "Logical Foundations of Functional Programming", ed. by 
   G. Huet, Addison-Wesley, 1990.). Hint: CR's will consist of strongly 
   normalizing untyped proof nets, but ask for more closure conditions 
   indicated by the Standardization Lemma in Girard's proof in TCS. 

7. (Extra credit)  Use conversion classes of normalizing untyped proof 
   nets to modify Girard's proof of Strong Normalization for 2nd order 
   LL in the style of the normalization proof for system F given on pp. 
   361-364 of Contemporary Math., vol. 92, J.W. Gray and A. Scedrov, eds., 
   Amer. Math. Soc., 1989.  This argument aims for normalization only.