Structural Normalization (1: STLC to Sequent Calculus)

17 May, 2026

{Previously: Part 0}

What I'm calling structural normalization -- a normalization procedure for simply-typed lambda calculus derived from concepts from structural proof theory -- can be achieved as a round trip with four stops.

STLC -> intuitionistic sequent calculus (LJ)
Cut elimination for LJ (to LJ-)
LJ- to canonical forms STLC (CF)
Home again: transliteration of canonical forms (CF) back to STLC

However, our actual itinerary is going to involve a backroad from 1 to 3. Instead of proving Cut Elimination as a translation from LJ into LJ-, we'll proof Cut Admissibility for LJ-, which allows us to go directly from STLC to LJ-, applying Cut Admissibility along the way. This lets us avoid defining two separate sequent calculi.

(Revised) Itinerary

The purpose of this blog post series is to describe a mechanized development I recently carried out of the following translations, which constitute my itinerary for the series:

STLC -> LJ-, assuming Cut Admissibility for LJ-
Cut Admissibility for LJ-
LJ- to CF
CF to STLC

In this post, I will cover step 1. (Note that steps 1 and 2 are somewhat out of order, but I think step 2 is a little more motivated once we have step 1 in place, and anyway it's the least "novel" in terms of things that have been well-documented and mechanized already.)

STLC

I will define STLC as the collection of proof terms for the following system of propositional natural deduction, defining the judgment $Γ ⊢ A true$ .

\frac{}{Γ, x : A true ⊢ A true} (x) \frac{Γ, x : A true ⊢ B true}{Γ ⊢ A \to B true} (λ x .) \frac{Γ ⊢ A \to B true Γ ⊢ A true}{Γ ⊢ B true} (app)

Note that if we were to think of $\to$ as logical implication, spell the $(x)$ rule as ${h y p}^{x}$ , the $(λ x .)$ rule as $\to I$ (implication introduction), and the $a p p$ rule as $\to E$ (implication elimination), we would have a natural deduction calculus for what Prawitz calls "minimal logic" (propositional logic with implication $\to$ as its sole connective).

Example 1. $λ x . x$ as a derivation of $A \to A true$ :

\frac{}{x : A true ⊢ A true} (x)

\frac{}{\cdot ⊢ A \to A true} (λ x .)

Example 2. $(λ x . x) y$ as a derivation of $y : B true ⊢ B true$ :

\frac{}{y : B true, x : B true ⊢ B true} (x)

\frac{}{y : B true ⊢ B \to B true} (λ x .) \frac{}{y : B true ⊢ B true} (y)

\frac{}{y : B true ⊢ B true} (app)

LJ-

I will define LJ- as the calculus defining the judgment $Γ ⟹ A$ with the following inference rules, in which $p$ denotes an atomic proposition.

\frac{}{Γ, x : p ⟹ p} ({id}_{p}^{x}) \frac{Γ, x : A ⟹ B}{Γ ⟹ A \to B} (\to R^{x}) \frac{Γ, A \to B ⟹ A Γ, A \to B, B ⟹ C}{Γ, A \to B ⟹ C} (\to L)

STLC -> LJ-

We want to prove the following theorem:

Theorem: STLC -> LJ-. For all STLC terms $M$ deriving $Γ ⊢ A true$ , there exists a derivation of $⌜ Γ ⌝ ⟹ A$ (where $⌜ - ⌝$ just strips off the "true"s).

The computational content of this theorem will be a translation of STLC terms to LJ- derivations.

Proof: by induction on the structure of $M$ .

STLC introduction rules (in the minimal fragment, just $λ$ ) correspond quite directly to LJ- right rules for the same connective:

Case $M = λ x . N$ : $Γ ⊢ A \to B true$ , where $N$ : $Γ, x : A true ⊢ B true$ .

Need to show $⌜ Γ ⌝ ⟹ A \to B$ .

By IH on $N$ , there's a derivation $𝒟$ of $⌜ Γ ⌝, x : A ⟹ B$
By rule $(\to R^{x})$ , $⌜ Γ ⌝ ⟹ A \to B$ , as needed.

However, the "elimination rules" don't map nicely onto the LJ- left rules:

Case $M = app (F, N)$ : $Γ ⊢ B true$ , where $F$ : $Γ ⊢ A \to B true$ and $N$ : $Γ ⊢ A true$ .

Need to show: $⌜ Γ ⌝ ⟹ B$ .

By IH on $F$ , we have a derivation $𝒟_{F}$ of $⌜ Γ ⌝ ⟹ A \to B$
By IH on $N$ , we have a derivation $𝒟_{N}$ of $⌜ Γ ⌝ ⟹ A$

Now we will construct a derivation of the goal with an extra premise of $A \to B$ :

By weakening $𝒟_{N}$ , we have $𝒟_{N}^{'}$ of $⌜ Γ ⌝, A \to B ⟹ A$
By {???}0, we have a derivation $ℰ$ of $⌜ Γ ⌝, A \to B, B ⟹ B$
By rule $(\to L)$ , we have $ℰ^{'} =$

𝒟_{N}^{'} ℰ

\frac{⌜ Γ ⌝, A \to B ⟹ A ⌜ Γ ⌝, A \to B, B ⟹ B}{⌜ Γ ⌝, A \to B ⟹ B} (\to L)

Finally, by putting together $𝒟_{F}$ and $ℰ^{'}$ , we'd like to conclude by some principle {???}1 our goal $⌜ Γ ⌝ ⟹ B$ .

We're missing two pieces, which turn out to be key metatheorems for LJ-:

The hole {???}0 can be filled with Identity Admissibility, which shows that $Γ, A ⟹ A$ for arbitrary $A$ , even when we limit the rule to propositional atoms;
The hole {???}1 can be filled with Cut Admissibility, which allows us to compose proofs of a cut formula AKA "lemma" with proofs that use that lemma to get a direct proof. That is, if $Γ, A ⟹ C$ and $Γ, A ⟹ C$ , then $Γ ⟹ C$ .

We'll talk about the proofs of these later but leave them as holes for now.

Finally we have the variable case:

Case $M = (x)$ : $Γ, x : A true ⊢ A true$ .

Need to show: $⌜ Γ ⌝, A ⟹ A$ .

The goal follows by Identity Admissibility (same as {???}0 in the previous case).

Mechanization

I mechanized the above development (and the rest of the series outlined in the itinerary) in Twelf. Because I'm interested in the computational content of these proofs, I wanted to mechanize them so I could run them as programs. I chose Twelf for the same reasons Frank outlines in his paper "Structural Cut Elimination" (whose title inspires mine):

Most proofs require tedious data structures (such as multi-sets) and use complex termination measures. They also involve global conditions on occurrences of parameters in sequent derivations. In this paper we present new proofs of cut elimination [in LF/Elf]. Multi-sets are avoided altogether in these proofs, and termination measures are replaced by three nested structural inductions. Parameters are treated as variables bound in derivations, thus naturally capturing occurrence conditions.

Unfortunately, development on Twelf has mostly ceased, and most modern proof assistants still don't offer this same convenience. But, happily, you can still install and run Twelf today, even in your browser.

What follows is my Twelf code implementing the STLC -> LJ- proof (view it in the online webserver!). This post is getting long enough to risk not getting finished before I need to get up and do something else, so for now I will just leave the code here sans explanation, perhaps discussing its details and the results of running it in the next installment.

var-to-hyp : tm A -> left A -> type.
%mode var-to-hyp +Tm -Left.

nd-to-sc : tm A -> right A -> type.
%mode nd-to-sc +X1 -X2.

% variable case as a block
%block var-conc 
: some {A:tp} {RA:left A -> right A}
  block {x:tm A} {h:left A} {d:var-to-hyp x h}
  {thm : nd-to-sc x (RA h)}.


nd-to-sc/lam
  : nd-to-sc (lam ([x:tm A] M x : tm B))
    (arr-R ([h:left A] D h))
   <- ({h : left A} 
          identity A h
          (RA h : right A))
   <- ({x:tm A} {h:left A}
          var-to-hyp x h
       -> nd-to-sc x (RA h)
       -> nd-to-sc (M x) (D h)).

nd-to-sc/app
  : nd-to-sc
    (app (Fn : tm (arr A B))
         (Arg : tm A) 
      : tm B)
    (DB : right B)
   <- nd-to-sc Fn (Dfn : right (arr A B))
   <- nd-to-sc Arg (Darg : right A)
   <- ({h:left (arr A B)}
        {x:left B} identity B x (DidB h x : right B))
   <- ca (arr A B) Dfn
      % left (arr A B) -> right B
      ([h:left (arr A B)]
       arr-L
          (DidB h)
          (Darg)
          h)
      DB.

%worlds (var-conc) (nd-to-sc _ _).
%total D (nd-to-sc D _).