[Prev][Next][Index][Thread]

Term Assignment Paper

To: linear@cs.stanford.edu
Date: Fri, 17 Jul 92 15:31:42 +0100

We should like to announce the impending availability of the following paper. 
We hope to have it ready in a couple of weeks. (ftp-details will be announced 
when they are known.)

Thanks,

Gavin Bierman.




               TERM ASSIGNMENT FOR INTUITIONISTIC LINEAR LOGIC

         Nick Benton, Gavin Bierman, Valeria de Paiva & Martin Hyland
                           University of Cambridge

We consider the problem of deriving a term assignment system for 
intuitionistic linear logic (actually only the multiplicative fragment 
for the moment). Our system differs from previous calculi (e.g. that of 
Abramsky) and has two important properties which they lack. These are the 
*substitution property* (the set of valid deductions is closed under 
substitution) and *subject reduction* (reduction on terms is well-typed). 
We have approached the derivation of a term assignment system in two ways

    1. By considering a *linear* natural deduction system. We can then 
    consider the connectives and their correct formulation. We use the 
    Curry-Howard correspondence to form a term assignment system.

    2. By taking the sequent calculus formulation, as given by Girard. 
    We have considered the rules using our categorical model (details below). 
    By considering the naturality properties of each rule, we can derive 
    a term assignment system.

We show that these two approaches provide equivalent logics and term 
assignment systems. (We give a procedure for mapping proofs from one system 
to the other). 

The main difference between our system and others is in the formulation 
of the *promotion* rule. Our sequent rule is

     x1:!A1,...,xn:!An |- e : B
    ----------------------------
     z1:!A1,...,zn:!An |- promote z1,...,zn for x1,...,xn in e : !B

(note the (vital) change of free variable names)

The natural deduction version is

    D1 |- e1:!A1 
    ...
    Dn |- en:!An         x1:!A1,...,xn:!An |- e : B
   -------------------------------------------------
    D1,...,Dn |- promote e1,...,en for x1,...,xn in e : !B
     
We then consider *reduction* in both systems. In the natural deduction 
system, we can derive beta-reductions and commuting conversions. In the 
sequent system, by considering cut-elimination, we have derived many more 
reductions. We show that all these reductions are instances of the naturality 
equations given by our categorical model. The computational significance 
of these equations is discussed.


THE CATEGORICAL MODEL.

Our categorical model is more general than that of Seeley's (in that we 
don't use additives).

Definition: A categorical model of ILL consists of a  symmetric monoidal 
closed category together with a comonad (!,epsilon,delta) with the properties:

    1. The functor ! is monoidal and epsilon and delta are monoidal natural 
    transformations.

    2. Every (free) !-coalgebra carries naturally the structure of a 
    commutative comonoid in such a way that coalgebra maps are comonoid 
    maps.