Modal Logic and Modal Types

There is not a single modal logic, there are a large family of modal logics depending on what axioms there are.

Necessitation rule

Every modal logic includes the necessitation rule (N) and distribution axiom (K), which together forms the minimum modal logic system K.

The distribution axiom is as follows, there’s no controversy here.

⊢ ▢(p -> q) -> (▢p -> ▢q)

Some confusion may arise with the necessitation rule. The correct formulation is as follows:

if ⊢ p, then ⊢ ▢p.

Any attempt to simplify the formulation to ⊢ p -> ▢p will cause problems, as the latter means completely different things. The necessitation rule says that if p is unconditionally true, then ▢p is also unconditionally true. The latter says, if p is true, then ▢p is true as well. The latter is obviously problematic, as p is true in current world, doesn’t make it true in all accessible worlds.

System S4 adds two axioms to system K:

The two axioms correspond to reflexivity and transitivity of the accessibility relation in Kripke semantics.

Subject reduction

A variant of the nessitation rule says that we can infer ▢p if all the hypothesis used in inferring p is of the form ▢q. This variant works well in logic, except proof simplification doesn’t observe subject reduction, which causes problem in type systems.

According to Curry-Howard correspondence, types correspond to propositions, terms correspond to proofs, and proof simplification correspond to evaluation. The problem with proof simplification will yield an unsound type system.

The problem can be demonstrated by the following example:

b: B, f: B -> ▢A ⊢ (\x: ▢A. box x) (f b) :  ▢▢A
b: B, f: B -> ▢A ⊢ box (f b) :  ▢▢A

As can be seen from the above, after one evaluation step, the term cannot be type checked anymore.

That’s the main motivation in [1] to distinguish between valid propositions and true propositions, which leads to a two-environment type system. The two most important typing rules in the system are as follows:

           Δ; Ø ⊢ t: T
         -----------------
         Δ; Γ ⊢ box t: ▢T


 Δ; Γ ⊢ t1: ▢T       (Δ, x:T); Γ ⊢ t2: U
 ------------------------------------------
      Δ; Γ ⊢ let box x = t1 in t2: U

Sound Call-by-value system

In a call-by-value setting, the previous problem cannot occur. That implies there is no need to distinguish between true and valid propositions. A simpler system can be formulated with just one environment:

            ▢Γ ⊢ t : T
           ---------------
           Γ ⊢ box t : ▢T

             Γ ⊢ t : ▢T
           ---------------
           Γ ⊢ unbox t : T

In the above, ▢Γ means only keep variables of modal types in the environment. Local soundness still holds:

 Γ ⊢ unbox (box t): T      ~~~~>    Γ ⊢ t: T

However, local completeness doesn’t hold for naive encoding:

 Γ ⊢ t: ▢T    ~~~~>  Γ ⊢ box (unbox t): ▢T

Local completeness holds with the following trick:

 Γ ⊢ t: ▢T    ~~~~>  Γ ⊢ (\x:▢T. box (unbox x)) t: ▢T

Kripke-style system

The paper [1] also introduces a Kripke-style type system, where the relation to kripke semantics is more direct. But the system is more verbose, as a stack of environments are required to modal the worlds.

Reference

  1. A Modal Analysis of Staged Computation, R. Davies et F. Pfenning, 2001.