# From modal necessity in ILL to DILL

Posted on 2019-07-03 by Oleg Grenrus linear

This post is my notes showing that if you apply a modal necessity construction as described by Pfenning and Davies1 to linear logic, you get dual intuitionistic linear logic2 by Barber. Maybe this is a well known fact, please tell me if it is so! Also we'll connect that to recent developments, where variables have multiplicities.

## #Validity

Let us briefly recap necessity/validity from a judgmental reconstruction of modal logic3. There are judgments which do not depend on hypotheses about the truth of propositions. Pfenning and Davies introduce the new judgment that A is valid. Evidence for the validity of A is simply unconditional evidence for A.

1. If `∙ ⊢ A true` then `A valid`.
2. If `A valid` then `Γ ⊢ A true`.

After that Pfenning and Davies internalize the judgment as a proposition, we'll follow their notation and write `□A` for the proposition expressing that A is valid.

At this point we should note that these all makes sense in a linear logic setting. Using the resource-interpretation of linear logic, we can say that if A is valid then to construct A we don't need any (linear) resources: it's an environment-friendly thing.

Pfenning and Davies then separate context into true and valid parts. We'll do the same, but use Γ for a collection of valid assumptions, and Δ for the collection of true assumptions. (i.e. swapping their notation). At this point it becomes clear that Γ is intuitionistic context, and Δ is linear context. We'll write contexts as `Γ, a : A ; Δ , b : B` separating context parts by semicolon, and individual assumptions (or parts) by comma. For empty part we'll write `∙`.

Next we need to adapt the Pfenning and Davies rules for the linear setting. Their system is not linear, so we need to make some adjustments. We'll go through the rules one-by-one.

Hypothesis / variable / axiom. We change the `ID` rule (from my last post, desribing Multiplicative-Additive Intuitionistic Linear Logic) to allow any intuitionistic context. Original `ID` rule is `a : A ⊢ a : A`; we additionally allow an arbitrary intuitionistic context Γ (remember: it can be formed from nothing at all).

``````------------------ Lin-ID
Γ; a : A ⊢ a : A``````

We'll also need a rule to use variable from an intuionistic context. Using an assumption from intuitionistic context doesn't "consume" anything. Note that linear part is required to be empty, `Δ = ∙`

``````---------------------- Int-ID
Γ, a : A ; ∙ ⊢ a : A``````

Right rule for □. This rule is very simple, note how the `Δ = ∙` on both sides of the line.

`````` Γ ; ∙ ⊢ a : A
------------------ □R
Γ ; ∙ ⊢ box a : □A``````

Left rule for □. The correct rule is not immediately obvious, but here it is anyway

`````` Γ , a : A ; Δ  ⊢  c : C
--------------------------------------------- □L
Γ ; Δ , ba : □A ⊢ case ba of box a -> c : C``````

These rules feels weird. We can show that rules are locally sound and complete. Local soundness describes a single step of admissibility of cut, kind of β-reduction step. Local completeness describes a way to η-expand. These are simple checks, so we know that right and left rules are well-balanced: not too powerful nor weak. To be fair, I have only seen local soundness and completeness checks done for natural deduction calculi, but I think it makes sense for sequent calculi as well; though we need to invoke `CUT` for local soundness.

Local soundness The way right and left rules are set up, a proof term with right rule on the left, and left rule on the right have to be glued together with `CUT`. If `CUT` is admissible (hopefully it is), then we can reduce the term, removing the `CUT` rule (often pushing it deeper into the term). In sequent calculi `CUT` rules show where we need to compute.

Assume that we have CUT rules for intuitionistic and linear contexts, `Int-CUT` and `Lin-CUT` respectively. If there is `Lin-CUT` with □R and □L premises:

``````     𝓓                          𝓔
------------              ----------------
Γ ; ∙ ⊢ A                 Γ , A  ; Δ ⊢ C
------------ □R           ---------------- □L
Γ ; ∙ ⊢ □A                Γ ; Δ , □A ⊢ C
------------------------------------------------------ Lin-CUT
Γ ; Δ ⊢ let ba = box a in case ba of box a' -> c : C``````

We can admit Cut, reduce the proof, cutting "smaller" things.

``````    𝓓                    𝓔
-----------      ---------------
Γ ; ∙ ⊢ A        Γ , A ; Δ ⊢ C
----------------------------------- Int-CUT
Γ ; Δ ⊢ let a' = a in c : C``````

Or more succinctly:

``````let ba = box a in case ba of box a' -> c
===>
let a' = a in c``````

Local completeness We can expand

``````--------------------- Lin-ID
Γ ; x : □A ⊢ x : □A``````

into

``````---------------- Int-ID
Γ , A ; ∙ ⊢  A
---------------- □R
Γ , A ; ∙ ⊢ □A
-------------------------------------------- □L
Γ ; x : □A ⊢ case x of box y -> box y : □A``````

Or more succinctly:

``````x
===>
case x of box y -> box y``````

## #Dual intuitionistic linear logic

Now if you take a look at the Dual Intuitionistic Linear Logic (1994) report by Andrew Barber, you'll notice that the DILL system is exactly what is described above.

There are two axiom rules, two cut rules, ... The only differences is that necessity is written as !A, not □A.

Of course it's not required to have two separate contexts, but programming in DILL is a lot more convenient, than in ILL with only a linear context.

## #Box is comonad and comonoid

As a small digression, having the rules for □, we can show

``````∙ ; □A ⊢ A         -- extract
∙ ; □A ⊢ □□A       -- duplicate
∙ ; □A ⊢ □A ⊗ □A   -- split
∙ ; □A ⊢ 1         -- delete``````

where for the last two we need to modify rules for ⊗ and 1 from my last post, but these modifications, as the proofs itself are quite straight-forward.

## #Connecting the dots

In this post we saw how simple construction of validity applied to linear logic (ILL) gives DILL. Pfenning and Davies already mention that their □ corresponds to linear ! (pronounced "of course"4).

A (hopefully) interesting exercise is to work through possibility modality, ⋄. Will it give linear ? (pronounced "why not"). I have no idea.

On the other hand, I think that "!A means that A doesn't require any resources" is a nice intuition. If `A = 5€`, it would be nice to have `!A` indeed!

There are recent developments in linear logic

which instead of having two contexts, use a single context but have an annotation on each assumption. For example, look at the GrMini from Granule paper, and syntax in Atkey & Wood extended abstract: they are quite the same, but different from what we just seen. The difference is well illustrated by ⊗R-rule: (our) two context approach rule is

`````` Γ ; Δ₁ ⊢ a : A     Γ ; Δ₂ ⊢ b : B
----------------------------------- ⊗R
Γ ; Δ₁ , Δ₂ ⊢ Pair a b : A ⊗ B``````

where we split the (linear) context into "structural" parts. Instead we could use a single context, and parametrise it by usages, and split the usages, not the context:

`````` Γ{R} ⊢ a : A     Γ{S} ⊢ b : B
------------------------------- ⊗R
Γ{R+S} ⊢ Pair a b : A ⊗ B``````

Generalising what you use as annotations, you can get Pfenning and Davies’ modal type theory or Barber's DILL, as Atkey and Wood show in their abstract.

To find out how Granule and Atkey & Wood systems differ, it's probably easies to find them on the internet or at conference and discuss directly :)

In hindsight, using annotations/multiplicities/... is an "obvious" discovery. If you try to formalise linear logic fragment in Coq or Agda, removing things from the context needs a lot more plumbing than just marking as used.

This brief post connects dots from few quite old papers with recent developments. In my opinion, the old stuff is relatively simple, and hopefully helps to understand the new stuff.

1. Frank Pfenning and Rowan Davies, A judgmental reconstruction of modal logic (2001)↩︎

2. Andrew Barber, Dual Intuitionistic Linear Logic (1994)↩︎

3. A modal logic is a logic with fancy prefix operators: modalities. I learned about that paper following Proof Theory Foundations -videos by Brigitte Pientka at Oregon Programming Languages Summer School (OPLSS) 2014.↩︎

Site proudly generated by Hakyll