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 simplytyped 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.
import 20160320onelambdacalculusmanytimes as Part1 module 20161030onelambdacalculusmanytimes2 where
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:
import Algebra import Relation.Binary as RB import Relation.Binary.List.Pointwise as RBLP open Part1.Syntax Atom hiding (w′) open import Data.Nat using (ℕ; suc; zero) open import Data.Fin using (Fin; suc; zero) open import Data.List using (List; _∷_; []; _++_) open import Data.List.Any using (here; there) open import Data.Product using (proj₁; proj₂) open import Function using (_$_) open import Function.Equivalence using (_⇔_; id; map; equivalence) open import Relation.Binary.PropositionalEquality open Data.List.Any.Membership (setoid Type) using (_∈_; _⊆_; module ⊆Reasoning) private open ⊆Reasoning hiding (_≈⟨_⟩_) module M = Algebra.Monoid (Data.List.monoid Type) ++identityʳ = proj₂ M.identity ++assoc = M.assoc infixr 2 _≡⟨_⟩_ _≡⟨_⟩_ : ∀ x x ≡ y → y IsRelatedTo z → x IsRelatedTo z _ ≡⟨ refl ⟩ y~z = y~z
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 . 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 ).

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 ) 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 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 rule, which took an extra argument—a proof that the desired type was a member of the context :
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 ).
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 admit^{2} the same structural rules. In the previous post, we’ve already proven the following theorem for ND:
If and , then .
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. Γ ⊆ A ∷ Γ, 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, A ∷ A ∷ Γ ⊆ A ∷ Γ and Γ ++ A ∷ B ∷ Δ ⊆ Γ ++ B ∷ A ∷ Δ, 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 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 , 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 . 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 expects both premises to share a context, but the premises have contexts and , 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, 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 .
weaken : ∀ Γ → Δ ⊆ Γ ++ Δ weaken [] i = i weaken (A ∷ Γ) i = there (weaken Γ i)
Forwards movement, or , is a little bit more involved: we move a formula past a context . We do so without moving any formulas in the prefix or the suffix . 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 ; nothing changes. Once we have moved past , we enter the nested function forward′, and . Here, we start moving each index one position back, to make room for the formula . Once we move past , and find the index pointint to , all we have to do is return here. Nothing has to change for the indices pointing into .
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: and .
The first case is trivial, and simply requires rewriting by proofs of right identity and associativity (as the actual sequent is ). For the second case, we prove the statement by moving the forwards across the (using ) and then permuting and . 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))

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

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. ↩