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

re: Bounded Linear Logic

Date: Fri, 28 Jul 89 11:03:38 BST

I have been trying to make sense of Bounded Linear Logic for myself,
in particular the novel feature: the bounded of-course !x<p.A[x].
NB In this, x becomes bound, and is not free in p (as Phil Scott confirmed).
Waste and resource polynomials become 0<p and 1<p respectively, where
< means less-or-equal. I have also modified the convention viz-a-viz
counting an summation: from 0 instead of 1; this removes some peculiarities
>from the "of course rule".

I claim that the "Resource Axiom" is in fact five separate axioms/rules
(viz. my Id, <+, <-, <! and W) and that the "!-rule" is two rules (! and M).
I have ignored the second order part and added the unit for @; apart from
these changes, the reader is invited to prove equivalence between the
Girard-Scedrov-Scott rules and the following:

				Gamma |-- A	Delta , A |-- B
	-------	Id		------------------------------- Cut
	A |-- A				Gamma, Delta |-- B

	Gamma, A , B |-- C		Gamma |-- A     Delta |-- B
        ------------------ @L		--------------------------- @R
	Gamma, A @ B |-- C              Gamma, Delta |-- A @ B

	  Gamma |-- C
        -------------- 1L		----- 1R
	Gamma, 1 |-- C			|-- 1

	Gamma |-- A     Delta, B |-- C		 Gamma, A |-- B
	------------------------------ -oL	---------------- -oR
	Gamma, Delta, A -o B |-- C		Gamma |-- A -o B

	0<p<q	 x positive in T[x]	0<p<q	x negative in T[x]
	--------------------------- <+	-------------------------- <-
		T[p] |-- T[q]			T[q] |-- T[p]

(T is meant to be a primitive type --- or a type variable in the
second order language --- dependent on certain variables with
specified signature; alternatively such dependence may be omitted,
since it is created with negative signature by !y<x.T.)

		0<p<q			     ..., A[x],... |-- B[x]
	----------------------- <!	-------------------------------- !
	!x<q.A[x] |-- !x<p.A[x]		..., !x<p.A[x],... |-- !x<p.B[x]

(The rule <! might also be called wastage.)

The remaining rules (which are the interesting ones) I write as axioms:

	W:		    !x<0.A[x]	|--  1

	C:		!x<(p+q).A[x]	|--  !x<p.A[x]  @  !x<q.A[p+x]

	D:		    !x<1.A[x]	|--  A[0]

	M:   !y<{sum z<p. q(z)}. A[y]	|--  !x<p.!y<q(x).A[y + sum z<x.q(z)]

NOW HERE IS MY POINT

If we replace 1, @ and ! of BLL by 0, + and sum  (where sum z<q.p means
p(0)+p(2)+...+p(q-1)) we obtain the four important axioms of summation of
functions with function bounds (exercise!).

C/W are the binary and nullary axioms for summation up to a sum, and
M/D for summation up to a summation (D is a "left unit law").

(1 is the unit because multiplication is a special case of summation; in fact
0, +, 1, sum and < are the primitive operations of resource polynomials,
not multiplication. We also need the obvious axioms of linearity of
summation and monotonicity of sum and summation, and also the
"right unit law" sum x<q.1=q. This axiomatises waste/resource polynomials.)

I think this throws some light on the mysterious "of course rule"

What I had set out to do was to translate the whole thing into category
theory, ie "hyperdoctrines".  It is clear what the base category must be:
strings of variables as objects, and polynomials as morphisms, with
0, +, 1, sum and < as additional structure on the hom-sets.

Bounded of-course !x<p.(-) is "adjoint" to the substitution functor along p.
Naturally I don't really mean adjoint: there are no unit and counit laws
for this "quantifier" just as there aren't for the "conjunction" @
(they are replaced in linear logic by C and W respectively).

However universal quantification (over unions and expansions of domains)
does satisfy <!, W, C, D and M.  Moreover the syntactic presentation
makes invisible the intention that quantification commute with substitution,
which is the Beck-Chevalley condition on quantifiers.

Paul Taylor.