Linear logic

The fact that the LF type theory uses only unrestricted assumptions has led some to assume that it cannot encode substructural logics such as linear logic. In fact, LF admits a very elegant encoding of linear logic, given below. The key idea is a judgement used to enforce the linear use of each linear assumption.

Contents

 The Encoding

 Syntax

```%%  Types  %%%
tp	: type.  %name tp T.

-o	: tp -> tp -> tp.  %infix right 7 -o.
*	: tp -> tp -> tp.  %infix right 10 *.
&	: tp -> tp -> tp.  %infix right 9 &.
+	: tp -> tp -> tp.  %infix right 8 +.
!	: tp -> tp.
zero	: tp.
top	: tp.

% 1 need not be primitive.
one	: tp
= ! top.

%%  Terms  %%%

term	: type.  %name term M.

lam	: (term -> term) -> term.
app	: term -> term -> term.

tensor	: term -> term -> term.
lett	: term -> (term -> term -> term) -> term.

pair	: term -> term -> term.
pi1	: term -> term.
pi2	: term -> term.

in1	: term -> term.
in2	: term -> term.
case	: term -> (term -> term) -> (term -> term) -> term.

bang	: term -> term.
letb	: term -> (term -> term) -> term.

any	: term -> term.

unit	: term.

% derived syntax for 1
star	: term
= bang unit.
leto	: term -> term -> term
= [t1] [t2] letb t1 ([x] t2).```

 Linearity

Linearity is enforced by employing a linearity judgement for each linear assumption. The linearity judgement ensures that a variable is used linearly (roughly speaking, exactly once) within its scope. (For an example of its use, see the rule of/lam for linear lambda abstraction below, which ensures that its argument is used linearly within its body.)

`linear : (term -> term) -> type.`

For example, a variable is used linearly in a single occurrence of that variable:

`linear/var	: linear ([x] x).`

A variable is used linearly in a lambda abstraction if it is used linearly in the body. (The abstraction's argument must also be used linearly in the body, but that is handled separately, by the abstraction's typing rule.)

```linear/lam	: linear ([x] lam (M x))
<- ({y} linear ([x] M x y)).```

A variable is used linearly in application, if it is used linearly in one of the two subterms and does not appear at all in the other:

```linear/app1	: linear ([x] app (M1 x) M2)
<- linear M1.
linear/app2	: linear ([x] app M1 (M2 x))
<- linear M2.```

The remaining constructs use the same technique. Note that there is no rule for bang; no linear variable may appear within a bang. Also note that a linear variable need not appear within an any (as with unit); however, if it does appear, it must be used linearly.

```linear/tensor1	: linear ([x] tensor (M1 x) M2)
<- linear M1.
linear/tensor2	: linear ([x] tensor M1 (M2 x))
<- linear M2.

linear/lett1	: linear ([x] lett (M1 x) M2)
<- linear M1.
linear/lett2	: linear ([x] lett M1 (M2 x))
<- ({y} {z} linear ([x] M2 x y z)).

linear/pair	: linear ([x] pair (M1 x) (M2 x))
<- linear M1
<- linear M2.

linear/pi1	: linear ([x] pi1 (M x))
<- linear M.

linear/pi2	: linear ([x] pi2 (M x))
<- linear M.

linear/in1	: linear ([x] in1 (M x))
<- linear M.

linear/in2	: linear ([x] in2 (M x))
<- linear M.

linear/case1	: linear ([x] case (M x) M1 M2)
<- linear M.
linear/case2	: linear ([x] case M (M1 x) (M2 x))
<- ({y} linear ([x] M1 x y))
<- ({y} linear ([x] M2 x y)).

linear/letb1	: linear ([x] letb (M1 x) M2)
<- linear M1.
linear/letb2	: linear ([x] letb M1 (M2 x))
<- ({y} linear ([x] M2 x y)).

linear/any1	: linear ([x] any (M x))
<- linear M.
linear/any2	: linear ([x] any M).

linear/unit	: linear ([x] unit).

% derived rules for 1
linear/leto1	: linear ([x] leto (M1 x) M2)
<- linear M1
= [d] linear/letb1 d.
linear/leto2	: linear ([x] leto M1 (M2 x))
<- linear M2
= [d] linear/letb2 ([y] d).```

 Typing rules

The typing rules are standard for linear logic, except that they must check that the linearity invariants are maintained. Thus, the typing rule for any construct that binds a linear variable (lam, for example) has a premise (or premises) ensuring that such variable(s) are used linearly in their scope. However, letb, which binds an unrestricted variable, does not check for linear usage of that variable.

```of : term -> tp -> type.

of/lam		: of (lam M) (T1 -o T2)
<- ({x} of x T1 -> of (M x) T2)
<- linear M.

of/app		: of (app M1 M2) T2
<- of M1 (T1 -o T2)
<- of M2 T1.

of/tensor	: of (tensor M1 M2) (T1 * T2)
<- of M1 T1
<- of M2 T2.

of/lett		: of (lett M1 M2) T
<- of M1 (T1 * T2)
<- ({x} of x T1 -> {y} of y T2 -> of (M2 x y) T)
<- ({y} linear ([x] M2 x y))
<- ({x} linear ([y] M2 x y)).

of/pair		: of (pair M1 M2) (T1 & T2)
<- of M1 T1
<- of M2 T2.

of/pi1		: of (pi1 M) T1
<- of M (T1 & T2).

of/pi2		: of (pi2 M) T2
<- of M (T1 & T2).

of/in1		: of (in1 M) (T1 + T2)
<- of M T1.

of/in2		: of (in2 M) (T1 + T2)
<- of M T2.

of/case		: of (case M M1 M2) T
<- of M (T1 + T2)
<- ({x} of x T1 -> of (M1 x) T)
<- ({x} of x T2 -> of (M2 x) T)
<- linear M1
<- linear M2.

of/bang		: of (bang M) (! T)
<- of M T.

of/letb		: of (letb M1 M2) T2
<- of M1 (! T1)
<- ({x} of x T1 -> of (M2 x) T2).

of/any		: of (any M) T
<- of M zero.

of/unit		: of unit top.

% derived rules for 1
of/star		: of star one
= of/bang of/unit.

of/leto		: of (leto M1 M2) T
<- of M1 one
<- of M2 T
= [d2] [d1] of/letb ([x] [d] d2) d1.```

 Subject Reduction

As a metatheoretic example, we may prove the subject reduction property using this encoding. First we define the relevant worlds:

```%block block	: block {x:term}.
%block bind	: some {t:tp} block {x:term} {d:of x t}.```

Next we define reduction:

```reduce : term -> term -> type.

red/refl	: reduce M M.
red/trans	: reduce M1 M3
<- reduce M1 M2
<- reduce M2 M3.

% beta rules
red/beta	: reduce (app (lam M1) M2) (M1 M2).
red/beta*	: reduce (lett (tensor M1 M2) M) (M M1 M2).
red/beta&1	: reduce (pi1 (pair M1 M2)) M1.
red/beta&2	: reduce (pi2 (pair M1 M2)) M2.
red/beta+1	: reduce (case (in1 M) M1 M2) (M1 M).
red/beta+2	: reduce (case (in2 M) M1 M2) (M2 M).
red/beta!	: reduce (letb (bang M1) M2) (M2 M1).

% compatibility
red/lam		: reduce (lam M) (lam M')
<- ({x} reduce (M x) (M' x)).
red/app		: reduce (app M1 M2) (app M1' M2')
<- reduce M1 M1'
<- reduce M2 M2'.
red/tensor	: reduce (tensor M1 M2) (tensor M1' M2')
<- reduce M1 M1'
<- reduce M2 M2'.
red/lett	: reduce (lett M1 M2) (lett M1' M2')
<- reduce M1 M1'
<- ({x} {y} reduce (M2 x y) (M2' x y)).
red/pair	: reduce (pair M1 M2) (pair M1' M2')
<- reduce M1 M1'
<- reduce M2 M2'.
red/pi1		: reduce (pi1 M) (pi1 M')
<- reduce M M'.
red/pi2		: reduce (pi2 M) (pi2 M')
<- reduce M M'.
red/in1		: reduce (in1 M) (in1 M')
<- reduce M M'.
red/in2		: reduce (in2 M) (in2 M')
<- reduce M M'.
red/case        : reduce (case M M1 M2) (case M' M1' M2')
<- reduce M M'
<- ({x} reduce (M1 x) (M1' x))
<- ({x} reduce (M2 x) (M2' x)).
red/bang	: reduce (bang M) (bang M')
<- reduce M M'.
red/letb        : reduce (letb M1 M2) (letb M1' M2')
<- reduce M1 M1'
<- ({x} reduce (M2 x) (M2' x)).
red/any		: reduce (any M) (any M')
<- reduce M M'.

% commuting conversions
red/app/lett	: reduce
(app (lett M1 M2) M3)
(lett M1 ([x] [y] app (M2 x y) M3)).
red/app/case	: reduce
(app (case M1 M2a M2b) M3)
(case M1 ([x] app (M2a x) M3) ([x] app (M2b x) M3)).
red/app/letb	: reduce
(app (letb M1 M2) M3)
(letb M1 ([x] app (M2 x) M3)).
red/app/any	: reduce
(app (any M1) M2)
(any M1).

red/pi1/lett	: reduce
(pi1 (lett M1 M2))
(lett M1 ([x] [y] pi1 (M2 x y))).
red/pi1/case	: reduce
(pi1 (case M1 M2a M2b))
(case M1 ([x] pi1 (M2a x)) ([x] pi1 (M2b x))).
red/pi1/letb	: reduce
(pi1 (letb M1 M2))
(letb M1 ([x] pi1 (M2 x))).
red/pi1/any	: reduce
(pi1 (any M))
(any M).

red/pi2/lett	: reduce
(pi2 (lett M1 M2))
(lett M1 ([x] [y] pi2 (M2 x y))).
red/pi2/case	: reduce
(pi2 (case M1 M2a M2b))
(case M1 ([x] pi2 (M2a x)) ([x] pi2 (M2b x))).
red/pi2/letb	: reduce
(pi2 (letb M1 M2))
(letb M1 ([x] pi2 (M2 x))).
red/pi2/any	: reduce
(pi2 (any M))
(any M).

red/lett/lett	: reduce
(lett (lett M1 M2) M3)
(lett M1 ([x] [y] lett (M2 x y) M3)).
red/lett/case	: reduce
(lett (case M1 M2a M2b) M3)
(case M1 ([x] lett (M2a x) M3) ([x] lett (M2b x) M3)).
red/lett/letb	: reduce
(lett (letb M1 M2) M3)
(letb M1 ([x] lett (M2 x) M3)).
red/lett/any	: reduce
(lett (any M1) M2)
(any M1).

red/case/lett	: reduce
(case (lett M1 M2) M3a M3b)
(lett M1 ([x] [y] case (M2 x y) M3a M3b)).
red/case/case	: reduce
(case (case M1 M2a M2b) M3a M3b)
(case M1 ([x] case (M2a x) M3a M3b) ([x] case (M2b x) M3a M3b)).
red/case/letb	: reduce
(case (letb M1 M2) M3a M3b)
(letb M1 ([x] case (M2 x) M3a M3b)).
red/case/any	: reduce
(case (any M1) M2a M2b)
(any M1).

red/letb/lett	: reduce
(letb (lett M1 M2) M3)
(lett M1 ([x] [y] letb (M2 x y) M3)).
red/letb/case	: reduce
(letb (case M1 M2a M2b) M3)
(case M1 ([x] letb (M2a x) M3) ([x] letb (M2b x) M3)).
red/letb/letb	: reduce
(letb (letb M1 M2) M3)
(letb M1 ([x] letb (M2 x) M3)).
red/letb/any	: reduce
(letb (any M1) M2)
(any M1).

red/any/lett	: reduce
(any (lett M1 M2))
(lett M1 ([x] [y] any (M2 x y))).
red/any/case	: reduce
(any (case M1 M2a M2b))
(case M1 ([x] any (M2a x)) ([x] any (M2b x))).
red/any/letb	: reduce
(any (letb M1 M2))
(letb M1 ([x] any (M2 x))).
red/any/any	: reduce
(any (any M))
(any M).```

Next we define syntactic equality and establish some uninteresting properties about it.

```tp-eq : tp -> tp -> type.
tp-eq/i		: tp-eq T T.

term-eq : term -> term -> type.
term-eq/i	: term-eq M M.```

Next we prove an important lemma: when a variable x is used linearly in a term M1, and M1 is substituted for a linear variable in a term M2 that does not mention x, than x is used linearly in the result.

```compose-linear : linear M1 -> linear M2 -> linear ([x] M1 (M2 x)) -> type.
%mode compose-linear +X1 +X2 -X3.```

Next we prove a technical lemma. It states that if x does not appear in M1, and M1 reduces to M2, then x does not appear in M2.

```reduce-closed : ({x:term} reduce M1 (M2 x)) -> ({x:term} term-eq M2' (M2 x)) -> type.
%mode reduce-closed +X1 -X2.```

With these lemmas in hand, we can prove the subject reduction theorem. In fact, there are two theorems to be proved simultaneously. One (sr) states that types are preserved by reduction, and the other (srl) states that linearity is preserved by reduction.

```srl : ({x} reduce (M x) (M' x))
-> ({x} of x T -> of (M x) T')
-> linear M
%
-> linear M' -> type.

sr : reduce M M'
-> of M T
%
-> of M' T -> type.
%mode srl +X1 +X2 +X3 -X4.
%mode sr +X1 +X2 -X3.```

Read more Twelf case studies and other Twelf documentation.