[Prev][Next][Index][Thread]
Bounded Linear Logic
Date: Tue, 18 Jul 89 14:41:34 EDT
BOUNDED LINEAR LOGIC
A Modular Approach to Polynomial Time Computability
(Preliminary Report)
by
J-Y. Girard , A. Scedrov, and P.J. Scott
1. Introduction
Typing is a way of describing the interactive behavior of
algorithms. Usual typing systems are mainly concerned with
input-output specifications, e.g., given terms f: A=>B and
a:A , the computation of f(a) by normalization yields a
result of type B. However, one can dream of more refined typings
that would not only ensure ethereal termination, but would for
instance yield feasible resource bounds. It seems that time
complexity does not lend itself naturally to modular manipulation.
We seek something more primitive.
Previous work on linear logic shows that the nontrivial part
of the dynamics of usual type systems lies in the contraction
rule. In two opposite extremes one can:
- remove the contraction rule, which produces real-time
dynamics but trivial expressive power,
- freely restore contraction through the unlimited exponential
connectives !A, which produces tremendous expressive power
without any realistic control on the dynamics.
Between these two extremes we propose Bounded Linear Logic, BLL.
In linear logic, exclamation mark is a typing instruction which
indicates that the datum is available in the memory for an unlimited
number of calls. Instead, bounded liner logic contains bounded
exclamation marks, new kind of typing instructions that indicate that
the datum is in the memory for at most x (direct or indirect) calls,
where x is the bound. The familiar Gentzen rules, when rewritten as
logical rules for bounded exclamation marks, naturally generate
polynomials.
This work contains two basic results:
(i). BLL strongly normalizes in polynomial time. To any proof
(that is, a typed algorithm) one can associate a polynomial which, in
the interesting cases, majorizes the length of the computation in the
size of the input.
(ii). Every polynomial-time computable function can be typed in BLL.
This result makes use of a very limited part of the full system. One
should not infer that what remains is a conservative extension of the
limited subsystem. The remaining part cannot produce any new functions
(because of (i) ), but it is likely to produce new algorithms.
On a more conceptual level, BLL introduces an intrinsic, proof-
theoretic (rather than machine-theoretic) paradigm for polynomial
time computation. All functional dependencies in BLL are feasible.
Moreover, BLL includes polymorphism. This permits uniform, natural
definitions of algebraic data types (without coding) and an inherent
notion of feasible computation over such types.
2. Resource Polynomials
Let (x-1 , n) be the binomial coefficient x-1 choose n
(obtained by dividing (x-1)*...*(x-n) by n!), where n = 0,1,2,... .
In particular (x-1 , 0) = 1 . A monomial is any (finite) product
(x-1 , n) * ... * (z-1 , p) , where the variables x , ... , z
are distinct.
A waste polynomial is any sum of monomials, e.g., 0 , 1 , x-1 ,
y , x + ( z*(z-1)/2 ) , etc.
A resource polynomial is any sum of monomials that involves at
least one constant 1 (in other words of the form 1 + w , w a waste ).
Resource polynomials are closed under sum, product, and composition.
Given resource polynomials p, q write p$q to denote that q-p
is a waste polynomial. If p$p' and q$q' ,then their composites
q;p $ q';p' .
3. The Syntax of Bounded Linear Logic (BLL)
Types (= formulae) : atomic formulae have the form t(p^) ;
here t is a second-order variable and p^ here denotes a non-empty
list of resource polynomials. Types are closed under the
following operations:
(i) A @ B (A tensor B = conjunction with no sharing of
variables),
(ii) A -o B (A linearly implies B = functions looking at
their argument exactly once),
(iii) !x<p A (bounded exponential with p a resource
polynomial),
(iv) (all t) A (second order universal quantification).
Positive and negative occurrences of resource terms in formulae
are defined by induction as usual; in !x<p A[x] , p occurs
negatively.
Let x_1, ... , x_n occur only positively in B . Then
\ x_1,...,x_n .B is a (second order) abstraction term, say T .
A[T/t] denotes the result of substituting T for t in A ,
i.e. of replacing the atoms t(p_1,...,p_n) in A by
B[p_1,...,p_n].
Given types A and A' , write A < A' if A and A' only differ
in their choice of resource polynomials, and
(i) for any positive occurence of resource poly p in A , the
homologous p' in A' is such that p$p'.
(ii) for any negative occurence of resource poly p in A , the
homologous p' in A' is such that p'$p .
GENTZEN SEQUENTS
Sequents have the form Gamma |-- B , where Gamma is a finite
(possibly empty) set of formulae. The formulae in Gamma are
considered indexed but not ordered. [Notation: because of the
limitations of the keyboard we write x<p for "x less than or
equal to p" , p,q,v range over resource polynomials, w ranges
over waste polynomials.]
Resource Axiom: Gamma, B |-- B' , where B < B' and all
formulae in Gamma begin with a bounded exclamation mark.
(Special case: B |-- B ).
Cut: Gamma |-- A Delta , A |-- B
-------------------------------------
Gamma, Delta |-- B
@
Gamma, A , B |-- C Gamma |-- A Delta |-- B
-------------------- -----------------------------
Gamma, A @ B |-- C Gamma, Delta |-- A @ B
-o
Gamma |-- A Delta, B |-- C Gamma, A |-- B
-------------------------------- ------------------
Gamma, Delta, A -o B |-- C Gamma |-- A -o B
all
Gamma, A[T/t] |-- B Gamma |-- A
------------------------ --------------------- (*)
Gamma, (all t) A |-- B Gamma |-- (all t) A
(*) t not free in A
Dereliction:
Gamma, A[1] |-- B
------------------------
Gamma, !x<p A[x] |-- B
Contraction:
Gamma, !x<p A[x], !x<q A[p+x] |-- B
-------------------------------------
Gamma, !x<p+q+w A[x] |-- B
! Rule:
..., !y<q(x) A[v(x)-q(x)+y], ... |-- B[x]
--------------------------------------------
..., !y<v(p)+w A[y], ... |-- !x<p B[x] ,
where v(x) = q(1)+...+q(x) and where all formulae on the
left have the indicated form.
We remind the reader that in Gentzen sequent calculi, as well as
in natural deduction calculus, proofs can be represented by lambda
terms, cf. reference [3], Chapter 5. This representation can be
extended to BLL.
4. The Main Theorem
The data type of tally natural numbers of level x is:
N_x := (all t) !y<x (t(y) -o t(y+1)) -o t(1) -o t(x)
Note: erasing the polynomial bounds gives the linear logic
version of the type of natural numbers:
(all t) !(t -o t) -o t -o t
Similarly, we may look at binary lists (and thus binary
numbers) generated by two successors (append 0 or 1) :
Bin_x := (all t) !y<x (t(y) -o t(y+1)) -o
!y<x (t(y) -o t(y+1)) -o t(1) -o t(x)
To each proof P in BLL, we can associate a measure m(P),
which turns out to be a resource polynomial in the free
resource variables of P.
Theorem (Strong Normalization). Given any proof P in
BLL , there are at most m(P)**3 steps in any reduction
of P .
Corollary. Let F be a proof of N_x -o N_p(x),
representing the numerical function f. Given an input
numeral m less than n , represented by a proof M of
N_n , normalization of F(M) yields output f(m) less
than p(n). The normalization time is a fixed polynomial
in n.
BIBLIOGRAPHY
[1] J-Y. Girard. Linear Logic, TCS(50), 1987.
[2] J-Y. Girard. Towards a Geometry of Interaction,
In: Categories in Computer Science and Logic,
ed. by J.W. Gray and A. Scedrov, Contemporary Math.,
vol. 92, Amer. Math. Soc., 1989.
[3] J-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types.
Cambridge Tracts in Theoretical Computer Science,
vol. 7, Cambridge University Press, 1989.
Current Addresses of Authors:
Jean-Yves Girard
Equipe de Logique
UA 753 du CNRS
Mathematiques, t. 45-55,
Univ. Paris 7
2 Place Jussieu
75251 Paris Cedex 05
France
Andre Scedrov
Dept. of Computer Science
Building 460
Stanford University
Stanford, CA 94305-2140
U.S.A.
arpanet: andre@polya.stanford.edu
andre@csli.stanford.edu
Philip J. Scott
Dept. of Mathematics
University of Ottawa
585 King Edward
Ottawa, Ontario
Canada K1N 6N5
bitnet: scpsg@uottawa