selected exercises [on linear logic--ed.]
Date: Wed, 13 Nov 91 20:56:17 EST
Here are a few take-home final exam problems in my linear logic course
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
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.