(no subject)

Philip Wadler <wadler@inf.ed.ac.uk> · Wed, 19 Nov 2003 13:21:02 +0100

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

I have a basic question about the system LU, as introduced by:

   J.-Y. Girard, On The Unity of Logic,
   Annals of Pure and Applied Logic 59:201--217, 1993.

I need here only a small fragment of the system, and do not require
polarities.  Write G for Gamma, D for Delta, L for Lambda, P for Pi.

Sequents have the form:

   G; G' |- D'; D

Weakening and contraction apply to G' and D', but not G and D.

Here are some of the rules:

   ------Id
   A;|-;A

   G;G'|-D';D,A   A,L;G'|-D';P
   ---------------------------Cut
   G,L;G'|-D';D,P

   G,A;G'|-D';D
   ------------Dereliction
   G;A,G'|-D';D

   ;G'|-D';A
   ----------!R
   ;G'|-D';!A

   G;A,G'|-D';D
   -------------!L
   G,!A;G'|-D';D

Consider the following proof

                           ------Id              ------Id
                           B;|-;B                B;|-;B
                           ------Dereliction     ------Dereliction
                           ;B|-;B                ;B|-;B
                           -------!R             -------!R
                           ;B|-;!B               ;B|-;!B
                           ---------------------------------otimes-R
   A, A-o!B;|-;!B          ;B|-;!B otimes !B
   ------------------------------------------Cut
   A, A-o!B;|-;!B

How does one eliminate the Cut from this proof?

This problem is closely related to one identified in the natural 
deduction
formulation of linear logic by Hyland et al., and also discussed in my 
paper,
"There's no substitute for linear logic".

Cheers,  -- P

Philip Wadler, Professor of Theoretical Computer Science
Informatics, University of Edinburgh
JCMB, King's Buildings, Mayfield Road
Edinburgh EH9 3JZ SCOTLAND
+44 131 650 5174 http://homepages.inf.ed.ac.uk/wadler/