Re: Cut-Elimination in Linear Logic

sanjiva@cse.iitd.ernet.in · Fri, 21 Nov 2003 12:33:09 +0530 (IST)

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

[I'm not sure my earlier attempts to reply got through, and I don't have a
copy saved. Please excuse. -S. ]

Phil:

If you are interested in working exactly within LU, and not with
an equivalent variant system like Frank's, then the canonical reference
for cut elim in LU is Jacqueline Vauzeille's paper in Annals of Pure and
Applied Logic 62:1-16, 1993.  It has some minor (fixable) typos in some of
the definitions but is otherwise an excellently detailed paper.

The paper contains some crucial lemmas (regarding proofs with
a positive [dually negative] formula on the right [dually left] of
a sequent), that cover the case to which your example refers
(i.e., the proof for A, A -o !B; |- ; !B).

The lemmas allow replacing a proof of the sequent of this shape by another
proof, on which the cut elimination process can proceed.

What is shown is that if there is a proof of a sequent in LU, there
is a proof in LU-{cuts}.  This is a bit weaker than saying that if
t is a term decorating a LU proof with  cuts, then the cut free
proof can be obtained by reducing t.  It's worthwhile checking
out whether the stronger statement holds for *closed* terms.

What (I believe -- see * below) these lemmas CAN be made to do is to
replace a proof of the sequent of this shape by an "equivalent" one.  The
transformation, if I recall correctly (I worked this out some 9-10 years
ago) involves eta-expansions, rearrangements involving explicit
substitutions etc.

(*) In the decoration I was examining, linearly maintained assumptions
were decorated by "addresses", whereas classically maintained ones by
variables.  !-L and out-L involved building skeletons for using explicit
substitutions "let z = [ ] in t", whereas !-R and out-R had no explicit
constructors (!? not an issue since there is only one formula on the
right).
Your example, assuming f:A -o !B, y: A would be decorated as
let z = [f y] in <z,z>, which ought not to reduce to <f y, f y>.

I think I understand what LU fragment you're looking at (Neutral+Positive
Int. Logic), so I think it it somewhat incorrect to say you don't
have polarities -- you have !A, which is positive.
I guess you mean that all atomic formulae are of neutral polarity,
and all positive formulae are obtained by the !-L and !-R rules.

Will be happy to discuss further.

Best,
Sanjiva

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
> Frank Pfenning wrote:
>
>>   Literally, what you call "cut" in your example is not an instance of
>> your cut rule, because the formulas "B" and "!B" do not match, ...
>
> Whoops, I forgot to use !L before the cut.  I should have written,
>
>                             ------Id              ------Id
>                             B;|-;B                B;|-;B
>                             ------Dereliction     ------Dereliction
>                             ;B|-;B                ;B|-;B
>                             -------!R             -------!R
>                             ;B|-;!B               ;B|-;!B
>                             ---------------------------------otimes-R
>                             ;B|-;!B otimes !B
>                             ------------------!L
>     A, A-o!B;|-;!B          !B;|-;!B otimes !B
>     ------------------------------------------Cut
>     A, A-o!B;|-;!B
>
> Thanks for the citations!  -- P
>