# All The Language

Welcome! I'm . I study natural language, programming languages and logical languages. Basically, all the language...

This post is a continuation of One λ-calculus, many times…, in which I explored the use of natural deduction and sequent calculus systems as type systems for the simply-typed lambda calculus.1 In this post, I will have a look at the variants of these systems which have explicit structural rules: Gentzen’s NJ and LJ.

The structure of this post will be similar to that of the previous installment—which means that we will start out by having a look at the syntax of NJ, then have a look at its semantics and relation to the system ND we discussed last time, and finally we will do the same for LJ. But first, the syntax:

module Syntax (Atom : Set) where


We can reuse our notions of types and sequents from the previous post:

  data Type : Set where
El  : Atom → Type
_⇒_ : Type → Type → Type

data Sequent : Set where
_⊢_ : List Type → Type → Sequent

Now, the usual axiomatisation for NJ is as follows:

There are three notable changes when comparing this to the system SC:

• Weakening. The axiom no longer allows for arbitrary contexts to be present, it has to be $A \vdash A$. An implication of this is that we no longer have the option to have unused formulas in our context. If we do want to have unused formulas, we can add these using the weakening rule (or $w$).

• Contraction. When we apply a binary rule, we no longer pass the entire context to both sides—instead, we have to choose how to split the context. So what do we do if there is a formula which we want to use in both branches of the proof? We can use the contraction (or $c$) rule, which copies a formula, and then pass a copy to either branch.

• Permutation. The third change lies in the structure of our contexts and with the $ax$ rule. In the previous system, we thought of our contexts as sets, even though we implemented them with lists. This showed itself in the definition of the $ax$ rule, which took an extra argument—a proof that the desired type $A$ was a member of the context $\Gamma$:

When we start thinking of the contexts as lists, we lose the ability to have variables point to arbitrary positions in the context—they can only point to the first element in the context. In other words, our system is ordered. To regain the freedom we’ve lost, we add a third new rule which allows us to swap elements in the context: permutation (or $p$).

Below, I’ve implemented the resulting system in Agda:

  infix 3 NJ_

data NJ_ : Sequent → Set where
ax : NJ A ∷ [] ⊢ A
⇒i : NJ A ∷ Γ ⊢ B → NJ Γ ⊢ A ⇒ B
⇒e : NJ Γ ⊢ A ⇒ B → NJ Δ ⊢ A → NJ Γ ++ Δ ⊢ B
w  : NJ Γ ⊢ B → NJ A ∷ Γ ⊢ B
c  : NJ A ∷ A ∷ Γ ⊢ B → NJ A ∷ Γ ⊢ B
p  : ∀ Γ → NJ Γ ++ A ∷ B ∷ Δ ⊢ C → NJ Γ ++ B ∷ A ∷ Δ ⊢ C


### Admissible Structural Rules in ND

If we are to have any hope of proving the equivalence between the implicit and the explicit systems, we should be able to prove that the implicit systems admit2 the same structural rules. In the previous post, we’ve already proven the following theorem for ND:

If $\Gamma \subseteq \Gamma\prime$ and $\Gamma \vdash A$, then $\Gamma\prime \vdash A$.

And we’ve also shown that we can very easily use this theorem to define weakening, because there is a proof that “weakening”, i.e. , holds for the subset relationship.

    w′ : ND Γ ⊢ B → ND A ∷ Γ ⊢ B
w′ = struct there

Therefore, all we need to show to extend this to contraction and permutation is that their respective equations, and , hold for the subset relation as well. This is simply a matter of reindexing. For contraction, if our “index” (made up of here and there) points to the first formula, we keep it the same. Otherwise, we subtract one. That way, the first two formulas are contracted, and the rest is adjusted accordingly.

    c′ : ND A ∷ A ∷ Γ ⊢ B → ND A ∷ Γ ⊢ B
c′ = struct contract′
where
contract′ : A ∷ A ∷ Γ ⊆ A ∷ Γ
contract′ (here px) = here px
contract′ (there i) = i


And for permutation, we skip through our index until we’ve passed the $\Gamma$ portion of the context, and then we swap the first two formulas.

    p′ : ∀ Γ → ND Γ ++ A ∷ B ∷ Δ ⊢ C → ND Γ ++ B ∷ A ∷ Δ ⊢ C
p′ Γ = struct (permute′ Γ)
where
permute′ : ∀ Γ → Γ ++ A ∷ B ∷ Δ ⊆ Γ ++ B ∷ A ∷ Δ
permute′ []      (here px)         = there (here px)
permute′ []      (there (here px)) = here px
permute′ []      (there (there i)) = there (there i)
permute′ (C ∷ Γ) (here px)         = here px
permute′ (C ∷ Γ) (there i)         = there (permute′ Γ i)


So, do we have enough to prove equivalence between the two systems? No, sadly we do not. If we have a look at the two versions of $\small{\Rightarrow}\!e$, we see that they use contexts quite differently…

If we were to try and use the second version to simulate the first, we’d find that we end up with two copies of the context $\Gamma$. We would need some souped up version of contraction to contract these two contexts back into one… If, on the other hand, we were to try and use the first version to simulate the second, we run into a different problem: the first version of $\small{\Rightarrow}\!e$ expects both premises to share a context, but the premises have contexts $\Gamma$ and $\Delta$, respectively. So we need two versions of weakening which can add an entire context to the right or left, respectively.

At this point, it may be a better idea to just derive a new, more permissive set of structural rules. This is what we’ll do in the next section.

### More Expressive Structural Rules

The usual structural rules for NJ are theoretically sufficient, but in practice they are rather limiting. Therefore, in this section, we will present more permissive variants, and show that they too are admissible in ND. Below you will see the more expressive variants of the structural rules. Instead of weakening, contracting or permuting formulas, these rules permute entire contexts.

I’ve added one new rule, $\small f^+$ or “forward”. It’s in parenthesis because it is an obvious instance of permutation. I’ve nontheless added it, because it is a useful lemma on the way to proving permutation.

Since we already have a structural theorem (struct) for ND, we only have to show that these equations hold for the subset relationship.

Weakening is still quite trivial. Instead of applying there once, we now apply it multiple times, until we’ve removed the entire context $\Gamma$.

    weaken : ∀ Γ → Δ ⊆ Γ ++ Δ
weaken []      i = i
weaken (A ∷ Γ) i = there (weaken Γ i)


Forwards movement, or $\small f^+$, is a little bit more involved: we move a formula $A$ past a context $\Sigma$. We do so without moving any formulas in the prefix $\Gamma$ or the suffix $\Delta$. The definition of forwards movement is split into two maps on indices: forward and forward′. In forward, we define the mapping for indices which point to some position in $\Gamma$; nothing changes. Once we have moved past $\Gamma$, we enter the nested function forward′, and $\Sigma$. Here, we start moving each index one position back, to make room for the formula $A$. Once we move past $\Sigma$, and find the index pointint to $A$, all we have to do is return here. Nothing has to change for the indices pointing into $\Delta$.

    forward : ∀ Γ Σ → (Γ ++ Σ) ++ A ∷ Δ ⊆ (Γ ++ A ∷ Σ) ++ Δ
forward (C ∷ Γ) Σ (here px) = here px
forward (C ∷ Γ) Σ (there i) = there (forward Γ Σ i)
forward []      Σ        i  = forward′ Σ i
where
forward′ : ∀ Σ → Σ ++ A ∷ Δ ⊆ A ∷ Σ ++ Δ
forward′      []        i  = i
forward′ (C ∷ Σ) (here px) = there (here px)
forward′ (C ∷ Σ) (there i) with forward′ Σ i
forward′ (C ∷ Σ) (there i) | here px = here px
forward′ (C ∷ Σ) (there i) | there j = there (there j)


With a rule for forwards movement in hand, we can start to prove permutation. The proof itself is broken down in two cases: $\Pi = \emptyset$ and $\Pi = A , \Pi'$.

The first case is trivial, and simply requires rewriting by proofs of right identity and associativity (as the actual sequent is $((\Gamma,\Sigma), (\emptyset,\Delta))$). For the second case, we prove the statement by moving the $A$ forwards across the $\Sigma$ (using $\small f^+$) and then permuting $\Sigma$ and $\Pi'$. The proof in Agda, however, is rather hard to read. This is because there is no pleasant way to intersperse code and rewrites (à la rewrite). To help you decipher the proof, I’ve inserted the intermediate terms as comments.

    permute : ∀ Γ Σ Π → (Γ ++ Σ) ++ (Π ++ Δ) ⊆ (Γ ++ Π) ++ (Σ ++ Δ)
permute Γ Σ [] =
begin
(Γ ++ Σ) ++ Δ
≡⟨ ++-assoc Γ Σ Δ ⟩
Γ ++ (Σ ++ Δ)
≡⟨ cong (_++ (Σ ++ Δ)) (sym (++-identityʳ Γ)) ⟩
(Γ ++ []) ++ (Σ ++ Δ)
∎
permute Γ Π (A ∷ Σ) =
begin
(Γ ++ Π) ++ (A ∷ Σ ++ Δ)
⊆⟨ forward Γ Π ⟩
(Γ ++ A ∷ Π) ++ (Σ ++ Δ)
≡⟨ cong (_++ (Σ ++ Δ)) (sym (++-assoc Γ (A ∷ []) Π)) ⟩
((Γ ++ (A ∷ [])) ++ Π) ++ (Σ ++ Δ)
⊆⟨ permute (Γ ++ A ∷ []) Π Σ ⟩
((Γ ++ (A ∷ [])) ++ Σ) ++ (Π ++ Δ)
≡⟨ cong (_++ (Π ++ Δ)) (++-assoc Γ (A ∷ []) Σ) ⟩
(Γ ++ A ∷ Σ) ++ (Π ++ Δ)
∎


In our previous version of contraction, all we had to do was merge any references to the first two formulas in our context.

    contract : ∀ Γ → (Γ ++ Γ) ++ Δ ⊆ Γ ++ Δ
contract []      i = i
contract (A ∷ Γ) (here px) = here px
contract (A ∷ Γ) (there i)
rewrite ++-assoc Γ (A ∷ Γ) Δ with forward [] Γ i
contract (A ∷ Γ) (there i) | here px = here px
contract (A ∷ Γ) (there i) | there j
rewrite sym (++-assoc Γ Γ Δ) = there (contract Γ j)


Boop.

    w⁺′ : ∀ Γ → ND Δ ⊢ A → ND Γ ++ Δ ⊢ A
w⁺′ Γ = struct (weaken Γ)

c⁺′ : ∀ Γ → ND (Γ ++ Γ) ++ Δ ⊢ A → ND Γ ++ Δ ⊢ A
c⁺′ Γ = struct (contract Γ)

p⁺′ : ∀ Γ Σ Π → ND (Γ ++ Σ) ++ (Π ++ Δ) ⊢ A
→ ND (Γ ++ Π) ++ (Σ ++ Δ) ⊢ A
p⁺′ Γ Σ Π = struct (permute Γ Σ Π)


Boop.

    s⁺′ : ∀ Γ Σ → ND (Γ ++ Σ) ++ Π ⊢ A
→ ND (Γ ++ Π) ++ Σ ⊢ A
s⁺′ Γ Σ f
= subst (λ Σ → ND (Γ ++ Π) ++ Σ ⊢ A)      (++-identityʳ Σ)
$p⁺′ Γ Σ Π$ subst (λ Π → ND (Γ ++ Σ) ++ Π ⊢ A) (sym (++-identityʳ Π))
$f  ### Deriving Structural Rules in NJ We can derive these same extended structural rules in NJ. For instance, below we derive the equivalent weakening rule:  w⁺′ : ∀ Γ → NJ Δ ⊢ A → NJ Γ ++ Δ ⊢ A w⁺′ [] f = f w⁺′ (B ∷ Γ) f = w (w⁺′ Γ f)  The remainder of the proofs are rather similar to those for ND,  f⁺′ : ∀ Γ Σ → NJ (Γ ++ Σ) ++ (A ∷ Δ) ⊢ B → NJ (Γ ++ A ∷ Σ) ++ Δ ⊢ B f⁺′ Γ [] f -- NJ (Γ ++ A ∷ []) ++ Δ ⊢ .B rewrite ++-identityʳ Γ -- NJ (Γ ++ A ∷ []) ++ Δ ⊢ B | ++-assoc Γ (A ∷ []) Δ -- NJ Γ ++ A ∷ Δ ⊢ B = f f⁺′ Γ (C ∷ Σ) f rewrite ++-assoc Γ (A ∷ C ∷ Σ) Δ -- NJ Γ ++ A ∷ C ∷ Σ ++ Δ ⊢ B = p Γ g where g : NJ Γ ++ C ∷ A ∷ Σ ++ Δ ⊢ B g rewrite sym (++-assoc Γ (C ∷ []) (A ∷ Σ ++ Δ)) -- NJ (Γ ++ C ∷ []) ++ A ∷ Σ ++ Δ ⊢ B | sym (++-assoc (Γ ++ C ∷ []) (A ∷ Σ) Δ) -- NJ ((Γ ++ C ∷ []) ++ A ∷ Σ) ++ Δ ⊢ B = f⁺′ (Γ ++ C ∷ []) Σ h where h : NJ ((Γ ++ C ∷ []) ++ Σ) ++ A ∷ Δ ⊢ B h rewrite ++-assoc Γ (C ∷ []) Σ = f   p⁺′ : ∀ Γ Σ Π → NJ (Γ ++ Σ) ++ (Π ++ Δ) ⊢ A → NJ (Γ ++ Π) ++ (Σ ++ Δ) ⊢ A p⁺′ Γ Σ [] f -- NJ (Γ ++ []) ++ Σ ++ Δ ⊢ A rewrite ++-identityʳ Γ -- NJ Γ ++ Σ ++ Δ ⊢ A | sym (++-assoc Γ Σ Δ) -- NJ (Γ ++ Σ) ++ Δ ⊢ A = f p⁺′ Γ Σ (B ∷ Π) f -- NJ (Γ ++ B ∷ Π) ++ Σ ++ Δ ⊢ A rewrite sym (++-assoc Γ (B ∷ []) Π) -- NJ ((Γ ++ B ∷ []) ++ Π) ++ Σ ++ Δ ⊢ A = p⁺′ (Γ ++ B ∷ []) Σ Π g where g : NJ ((Γ ++ B ∷ []) ++ Σ) ++ Π ++ Δ ⊢ A g rewrite ++-assoc Γ (B ∷ []) Σ -- NJ (Γ ++ B ∷ Σ) ++ Π ++ Δ ⊢ A = f⁺′ Γ Σ f   c⁺′ : ∀ Γ → NJ (Γ ++ Γ) ++ Δ ⊢ A → NJ Γ ++ Δ ⊢ A c⁺′ [] f = f c⁺′ (B ∷ Γ) f = c$ p⁺′ [] Γ (B ∷ B ∷ [])        $c⁺′ Γ$ p⁺′ [] (B ∷ B ∷ []) (Γ ++ Γ) $g where g : NJ (B ∷ B ∷ Γ ++ Γ) ++ Δ ⊢ A g rewrite ++-assoc (B ∷ B ∷ Γ) Γ Δ = f⁺′ [] (B ∷ Γ) h where h : NJ B ∷ Γ ++ B ∷ Γ ++ Δ ⊢ A h rewrite sym (++-assoc (B ∷ Γ) (B ∷ Γ) Δ) = f   s⁺′ : ∀ Γ Σ → NJ (Γ ++ Σ) ++ Π ⊢ A → NJ (Γ ++ Π) ++ Σ ⊢ A s⁺′ Γ Σ f = subst (λ Σ → NJ (Γ ++ Π) ++ Σ ⊢ A) (++-identityʳ Σ)$ p⁺′ Γ Σ Π
$subst (λ Π → NJ (Γ ++ Σ) ++ Π ⊢ A) (sym (++-identityʳ Π))$ f

    ax′ : A ∈ Γ → NJ Γ ⊢ A
ax′ (here px) rewrite px = s⁺′ [] Γ (w⁺′ Γ ax)
ax′ (there x)            = w (ax′ x)


It turns out to be very useful to define two helper functions which introduce and eliminate the empty context to the right. This is because doesn’t automatically reduce. Therefore, any proof in which the empty context occurs to the right would involve rewriting by ++‑identityʳ.

    ∅i : NJ Γ ⊢ A → NJ Γ ++ [] ⊢ A
∅i f rewrite ++-identityʳ Γ = f
∅e : NJ Γ ++ [] ⊢ A → NJ Γ ⊢ A
∅e f rewrite ++-identityʳ Γ = f


### Implicit and Explicit Structural Rules

  module NJ⇔ND where

⟹ : NJ S → ND S
⟹  ax         = ax₀
⟹ (⇒i f  )    = ⇒i (⟹ f)
⟹ (⇒e {Γ = Γ} f g)    = ⇒e (inl (⟹ f)) (inr (⟹ g))
where
inl : ND Γ ⊢ A → ND Γ ++ Δ ⊢ A
inl {Δ = Δ} f = ND.s⁺′ [] Δ (ND.w⁺′ Δ f)
inr : ND Δ ⊢ A → ND Γ ++ Δ ⊢ A
inr f = ND.w⁺′ Γ f

⟹ (w    f)    = ND.w′   (⟹ f)
⟹ (c    f)    = ND.c′   (⟹ f)
⟹ (p  Γ f)    = ND.p′ Γ (⟹ f)

⟸ : ND S → NJ S
⟸ (ax  x)     = NJ.ax′ x
⟸ (⇒i  f)     = ⇒i  (⟸ f)
⟸ (⇒e  {Γ = Γ} f g)   = NJ.∅e (NJ.c⁺′ Γ (NJ.∅i (⇒e (⟸ f) (⟸ g))))


### Sequent Calculus with Explicit Structural Rules

  infix 3 LJ_

data LJ_ : Sequent → Set where
ax  : LJ A ∷ [] ⊢ A
cut : LJ Γ ⊢ A → LJ A ∷ Δ ⊢ B → LJ Γ ++ Δ ⊢ B
⇒l  : LJ Γ ⊢ A → LJ B ∷ Δ ⊢ C → LJ A ⇒ B ∷ Γ ++ Δ ⊢ C
⇒r  : LJ A ∷ Γ ⊢ B → LJ Γ ⊢ A ⇒ B
w   : LJ Γ ⊢ B → LJ A ∷ Γ ⊢ B
c   : LJ A ∷ A ∷ Γ ⊢ B → LJ A ∷ Γ ⊢ B
p   : ∀ Γ → LJ Γ ++ A ∷ B ∷ Δ ⊢ C → LJ Γ ++ B ∷ A ∷ Δ ⊢ C

    ∅i : LJ Γ ⊢ A → LJ Γ ++ [] ⊢ A
∅i f rewrite ++-identityʳ Γ = f
∅e : LJ Γ ++ [] ⊢ A → LJ Γ ⊢ A
∅e f rewrite ++-identityʳ Γ = f

  module LJ⇔NJ where

⟹ : LJ S → NJ S
⟹  ax       = ax
⟹ (cut {Δ = Δ} f g) = NJ.s⁺′ [] Δ (⇒e (⇒i (⟹ g)) (⟹ f))
⟹ (⇒l  {Δ = Δ} f g) = NJ.s⁺′ [] Δ (⇒e (⇒i (⟹ g)) (⇒e ax (⟹ f)))
⟹ (⇒r  f)   = ⇒i  (⟹ f)
⟹ (w   f)   = w   (⟹ f)
⟹ (c   f)   = c   (⟹ f)
⟹ (p Γ f)   = p Γ (⟹ f)

⟸ : NJ S → LJ S
⟸  ax       = ax
⟸ (⇒i  f)   = ⇒r  (⟸ f)
⟸ (⇒e  f g) = cut (⟸ f) (LJ.∅e (⇒l (⟸ g) ax))
⟸ (w   f)   = w   (⟸ f)
⟸ (c   f)   = c   (⟸ f)
⟸ (p Γ f)   = p Γ (⟸ f)

  module LJ⇔SC where

⟹ : LJ S → SC S
⟹ f = ND⇔SC.⟹ (NJ⇔ND.⟹ (LJ⇔NJ.⟹ f))

⟸ : SC S → LJ S
⟸ f = LJ⇔NJ.⟸ (NJ⇔ND.⟸ (ND⇔SC.⟸ f))


1. Or, alternatively, as axiomatisations of minimal propositional logic.

2. As used here, admit or admissible is a technical term, usually contrasted with derivable. Derivable rules are rules that we can construct directly, without inspecting the proofs that we’re given as arguments. On the other hand, admissible means that we can define these rules, but that we have to inspect and rewrite the proofs we’re given.