[Prev][Next][Index][Thread]
Term Assignment for ILL
To: linear@cs.stanford.edu
Date: Thu, 13 Aug 92 17:43:43 +0100
The following paper is now available by anonymous ftp.
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.
_______________________________________________________________________________
This paper is available by anonymous ftp from IMPERIAL COLLEGE. If you can
not use ftp, send me your postal address.
% ftp theory.doc.ic.ac.uk
Name: anonymous
Password: <<Your e-mail address>>
ftp> cd theory/papers/dePaiva
ftp> binary
ftp> get taill.dvi.Z
ftp> bye
The BibTeX entry for this paper is
@techreport{benton92,
author = "Nick Benton and Gavin Bierman and Valeria de Paiva and Martin
Hyland",
title = "Term Assignment for Intuitionistic Linear Logic",
number = 262,
institution = "Computer Laboratory, University of Cambridge",
month = aug,
year = 1992
}