I have an issue with the notion of saturated sets as defined in class:
it seems to be tailored specifically to the exact system it's for,
and it's unclear how it should be extended to fit an extended system
with additional eliminators and reduction rules.

In the POPLMark reloaded[^1] paper,
they provide an inductive definition of strongly normalizing terms
and a notion of reducibility candidates/saturated sets based on this definition,
and I think it's much clearer how the proof of normalization can be extended.

To demonstrate, I'm going to consider System F extended with booleans,
and try to prove normalization directly using their inductive definition.
First, here are the complete typing rules including booleans and the conditional.

```
┌───────────┐
│ Γ ⊢ M : σ │
└───────────┘

x : σ ∈ Γ        Γ, x : σ ⊢ M : τ         Γ ⊢ M : σ → τ    Γ ⊢ N : σ
--------- Var    ----------------- Abs    -------------------------- App
Γ ⊢ x : σ        Γ ⊢ λx. M : σ → τ        Γ ⊢ M N : τ

Γ ⊢ M : σ    α ∉ FV(Γ)         Γ ⊢ M : ∀α. σ    α ∉ FV(τ)
---------------------- TAbs    -------------------------- TApp
Γ ⊢ M : ∀α. σ                  Γ ⊢ M : σ{α ↦ τ}

--------------- True    ---------------- False
Γ ⊢ true : Bool         Γ ⊢ false : Bool

Γ ⊢ b : Bool    Γ ⊢ M : A    Γ ⊢ N : A
-------------------------------------- If
Γ ⊢ if b then M else N : A
```

## Strongly normalizing terms

Strongly normalizing terms are defined mutually with
strongly normalizing neutral terms and strong head reduction.
For short, I interchangeably refer to strongly normalizing terms as "normal terms",
and strongly normalizing neutral terms as "neutral terms",
since there is no separate notion of normal and neutral terms that precludes reduction.

The underlying principles are:
1. Neutral terms are variables and eliminators neutral in the head position
   and normal in all other arguments;
2. Normal terms are neutral terms and constructors with normal components,
   backward closed under head reduction;
3. Head reduction consists of β-reduction on normal arguments,
   and congruence rules for eliminators in the head position.
Reduction is defined mutually with normality to ensure backward closure of normal terms,
since otherwise looping terms may disappear after reduction,
e.g. the function application argument if it is unused, or the other branch of a conditional.
Using these principles, the definition in POPLMark reloaded can be extended to booleans.
(In contrast to the paper, I'll stick to untyped judgements, which is an orthogonal feature.)

```
┌─────────┐
│ M ∈ SNe │
└─────────┘
                     M ∈ SNe    N ∈ SN
------- SNe-Var      ----------------- SNe-App
x ∈ SNe              M N ∈ SNe

M ∈ SNe    N₁, N₂ ∈ SN
-------------------------- SNe-If
if M then N₁ else N₂ ∈ SNe

┌────────┐
│ M ∈ SN │
└────────┘

M ∈ SNe              M ⇝ N    N ∈ SN
------- SN-SNe       --------------- SN-Red
M ∈ SN               M ∈ SN

M ∈ SN
---------- SN-Abs    ---------------- SN-True,False
λx. M ∈ SN           true, false ∈ SN

┌───────┐
│ M ⇝ N │
└───────┘

N ∈ SN                          M ⇝ M'
-------------------- Red-β      ---------- Red-App
(λx. M) N ⇝ M{x ↦ N}            M N ⇝ M' N

N₂ ∈ SN
---------------------------- Red-True
if true then N₁ else N₂ ⇝ N₁

N₁ ∈ SN
----------------------------- Red-False
if false then N₁ else N₂ ⇝ N₂

M ⇝ M'
------------------------------------------- Red-If
if M then N₁ else N₂ ⇝ if M then N₁ else N₂
```

I assume the following property because I don't want to prove it but I'm sure it's true.

**Proposition** (antisubstitution):
1. If N ∈ SN and M{x ↦ N} ∈ SN then M ∈ SN.
2. If N ∈ SN and M{x ↦ N} ∈ SNe then M ∈ SN.
3. If M{x ↦ N} ⇝ M' and M' ∈ SN then M ∈ SN.

Because these are inductive definitions, we will need some lemmas
for properties that formerly held by definition, namely inversion and congruence.

**Lemma** (Inv-App): If (M N) ∈ SN then M ∈ SN.
**Proof**: By induction on SN.
There are two possible cases:
* Case SN-SNe. We have (M N) ∈ SNe, and we wish to show M ∈ SN.
  By inversion on neutrals, the only possible case is SNe-App,
  where M ∈ SNe. Then M ∈ SN by SN-SNe.
* Case SN-Red. We have (M N) ⇝ N' ∈ SN, and we wish to show M ∈ SN.
  By inversion on the reduction, there are two possible cases.
    * Case Red-β. We have M = (λx. M'), N ∈ SN, and N' = M'{x ↦ N}.
	  By antisubstitution, M' ∈ SN, so (λx. M') ∈ SN.
    * Case Red-App. We have M N ⇝ M' N = N' ∈ SN and M ⇝ M'.
	  By the induction hypothesis, M' ∈ SN. By SN-Red, M ∈ SN.

**Lemma** (Reds-If): If M ⇝* M' then (if M then N₁ else N₂) ⇝* (if M' then N₁ else N₂).
**Proof**: By induction on the reflexive, transitive closure of reduction,
using Red-If and the induction hypothesis in the transitive case.

**Lemma** (Reds-App): If M ⇝* M' then M N ⇝* M' N.
**Proof**: By induction on the reflexive, transitive closure of reduction,
using Red-App and the induction hypothesis in the transitive case.

## Reducibility candidates

Their definition of reducibility candidates (CR) then captures the same properties SAT did,
namely backward closure under head reduction,
and that SATs/CRs are squeezed between neutrals and normals.

**Definition**: A set R is a reducibility candidate (R ∈ CR) when the following hold:
1. R ⊆ SN;
2. If M ⇝ M' and M' ∈ R then M ∈ R; and
3. SNe ⊆ R.
I refer to these as CR1, CR2, and CR3.

We can prove the same lemmas for CR as we did for SAT,
with an additional backward closure under the reflexive, transitive closure of reduction.

**Lemma 0** (CR2*): Let R ∈ CR. If M ⇝* M' and M' ∈ R then M ∈ R.
**Proof**: By induction on the reflexive, transitive closure of reduction,
using CR2 and the induction hypothesis in the transitive case.

**Lemma 1**: SN ∈ CR.
**Proof**: CR1 holds trivially, CR2 holds by SN-Red, and CR3 holds by SN-SNe.

**Lemma 2**: If A, B ∈ CR, then A ⇒ B ∈ CR, where (M ∈ A ⇒ B) ⇔ for all N ∈ A, M N ∈ B.
**Proof**: Let A, B ∈ CR.
1. Suppose M ∈ A ⇒ B. We need to show that M ∈ SN.
   Picking any variable x, we know x ∈ A since SNe ⊆ A ∈ CR by CR3.
   Then by definition, M x ∈ B ∈ CR, so by M x ∈ SN by CR1.
   Then by Inv-App, M ∈ SN.
2. Suppose M ⇝ M' ∈ A ⇒ B. We need to show that M ∈ A ⇒ B,
   i.e. supposing N ∈ A, M N ∈ B. By supposition, we know M' N ∈ B.
   By Red-App, we know M N ⇝ M' N, and by CR2, we have M N ∈ B.
3. Suppose M ∈ SNe. We need to show that M ∈ A ⇒ B,
   i.e. supposing N ∈ A, M N ∈ B.
   By CR1, we know N ∈ A ⊆ SN, so by SNe-App, we have M N ∈ SNe.
   Then by CR2, we have M N ∈ SNe ⊆ B.

**Lemma 3**: Let Aᵢ be some family of sets of terms indexed by i ∈ I (potentially infinite).
If Aᵢ ∈ CR, then ∩ᵢ Aᵢ ∈ CR.
**Proof**: Suppose Aᵢ ∈ CR.
1. Let M ∈ ∩ᵢ Aᵢ. We need to show that M ∈ SN.
   By definition, M ∈ Aᵢ for some Aᵢ, and by CR1, we have M ∈ Aᵢ ⊆ SN.
2. Suppose M ⇝ M' ∈ ∩ᵢ Aᵢ. We need to show that M ∈ ∩ᵢ Aᵢ.
   By definition, M' ∈ Aᵢ for every Aᵢ.
   By CR2, we have M ∈ Aᵢ for every Aᵢ, so M ∈ ∩ᵢ Aᵢ.
3. Suppose M ∈ SNe. We need to show that M ∈ ∩ᵢ Aᵢ.
   By CR3, we have M ∈ Aᵢ for every Aᵢ, so M ∈ ∩ᵢ Aᵢ.

## Type interpretations

With the addition of booleans, we need an interpretation of the type of booleans.
The positive formulation states that elements of the interpretation
reduce to normal constructor forms or is neutral;
the negative formulation states that elements of the interpretation
behave "as expected" when eliminated.
For booleans, the latter looks like this:

**_not_ the Definition** (semantic booleans): M ∈ ⟦Bool⟧ξ ⇔ for all σ and N₁, N₂ ∈ ⟦σ⟧ξ,
(if M then N₁ else N₂) ∈ ⟦σ⟧ξ.

However, Joe Cutler says this doesn't work (don't tell him I said he said this),
and I can't be bothered to check, so I'll stick with the positive formulation.
We also need to show that it, too, is a reducibility candidate.

**Definition** (semantic booleans): M ∈ ⟦Bool⟧ξ ⇔ M ∈ SNe or M ⇝* true or M ⇝* false.

**Lemma 4**: ⟦Bool⟧ξ ∈ CR.
**Proof**:
1. We need to show that if M ∈ ⟦Bool⟧ξ, then M ∈ SN.
   By definition of ⟦Bool⟧ξ, there are three cases.
   If M ∈ SNe, then M ∈ SN by SN-SNe.
   If M ⇝* true or M ⇝* false, then induct on the reflexive, transitive closure.
   In the reflexive case, we use SN-True and SN-False.
   In the transitive case, we use SN-Red followed by the induction hypothesis.
2. We need to show that if M ⇝ M' ∈ ⟦Bool⟧ξ, then M ∈ ⟦Bool⟧ξ.
   By definition of ⟦Bool⟧ξ, there are three cases.
   If M' ∈ SNe, then by SN-SNe and SN-Red, we have M ∈ SNe, so M ∈ ⟦Bool⟧ξ
   If M' ⇝* true or M ⇝* false, by transitivity, M ⇝ M' ⇝* true or false.
3. We need to show that if M ∈ SNe, then M ∈ ⟦Bool⟧ξ, which holds by definition.

With these four lemmas, the interpretation of types is a reducibility candidate.

**Definition** (type interpretation): Let ξ be a function from type variables to CRs.
We define ⟦·⟧ξ recursively on types:
* ⟦α⟧ξ ≔ ξ(α)
* ⟦σ → τ⟧ξ ≔ ⟦σ⟧ξ ⇒ ⟦τ⟧ξ
* ⟦∀α. σ⟧ξ ≔ ∩ₓ ⟦σ⟧(ξ, α ↦ x) where X ∈ CR
* ⟦Bool⟧ξ ≔ semantic booleans as above

**Lemma 5**: ⟦σ⟧ξ ∈ CR.
**Proof**: By induction on types, using Lemmas 2, 3, 4
for functions, polymorphism, and booleans, respectively.

## Soundness and normalization

The definitions of semantic typing remain unchanged, reproduced below,
using ρ for substitution maps from term variables to terms,
ξ for substitution maps from type variables to sets,
and M{ρ} for applying the substitutions of ρ in M.

**Definitions**:
* ⟦M⟧ρ ⇔ M{ρ}
* ρ, ξ ⊧ Γ ⇔ ∀x : σ ∈ Γ, ρ(x) ∈ ⟦σ⟧ξ
* Γ ⊧ M : σ ⇔ ∀ρ, ξ ⊧ Γ, ⟦M⟧ρ ∈ ⟦σ⟧ξ

We can now prove the fundamental soundness theorem.
All of the old cases hold as usual;
I'll cover just the old polymorphism cases along with the new boolean cases.

**Theorem** (soundness): If Γ ⊢ M : σ then Γ ⊧ M : σ.
**Proof**: By induction on the typing derivation.
* Case TAbs: We have premises Γ ⊢ M : σ and α ∉ FV(Γ),
  and we need to show Γ ⊧ M : ∀α. σ,
  i.e. for every ρ, ξ ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦∀α. σ⟧ξ = ∩ₓ ⟦σ⟧{ξ, α ↦ X}.
  By the induction hypothesis, for every ρ', ξ' ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦σ⟧ξ.
  Consequently, for every X ∈ CR, we have ρ, {ξ, α ↦ X} ⊧ Γ implies ⟦M⟧ρ ∈ ⟦σ⟧ξ.
  Since α ∉ FV(Γ), given ρ, ξ ⊧ Γ, we can harmlessly extend to ρ, {ξ, α ↦ X} ⊧ Γ.
  Then for every X ∈ CR, ⟦M⟧ρ ∈ ⟦σ⟧{ξ, α ↦ X}, i.e. ⟦M⟧ρ ∈ ∩ₓ ⟦σ⟧{ξ, α ↦ X}.
* Case TApp: We have premises Γ ⊢ M : ∀α. σ and α ∉ FV{τ},
  and we need to show Γ ⊧ M : σ{α ↦ τ},
  i.e. for every ρ, ξ ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦σ{α ↦ τ}⟧ξ = ⟦σ⟧{ξ, α ↦ ⟦τ⟧ξ}.
  By the induction hypothesis, we have ⟦M⟧ρ ∈ ⟦∀α. σ⟧ξ = ∩ₓ ⟦σ⟧{ξ, α ↦ X}.
  By Lemma 5, ⟦τ⟧ξ ∈ CR, so we can instantiate X with ⟦τ⟧ξ.
* Case True: We need to show Γ ⊧ true : Bool,
  i.e. for every ρ, ξ ⊧ Γ, we have ⟦true⟧ρ ∈ ⟦Bool⟧ξ.
  This holds trivially by true ⇝* true.
* Case False: As above.
* Case If: We have premises Γ ⊢ M : Bool, Γ ⊢ N₁ : σ, Γ ⊢ N₂ : σ,
  and we need to show Γ ⊧ if M then N₁ else N₂,
  i.e. for every ρ, ξ ⊧ Γ, we have (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ.
  By the induction hypotheses, we have ⟦M⟧ρ ∈ ⟦Bool⟧ξ and ⟦Nᵢ⟧ρ ∈ ⟦σ⟧ξ.
  By Lemma 5, we have ⟦M⟧ρ, ⟦Nᵢ⟧ρ ∈ CR, and by CR1, we have ⟦M⟧ρ, ⟦Nᵢ⟧ρ ∈ SN.
  By definition of ⟦Bool⟧ξ, there are three cases to consider.
    * ⟦M⟧ρ ∈ SNe: By SNe-If, we know that (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ SNe.
	  Then by CR3, we have (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ.
    * ⟦M⟧ρ ⇝* true or false: By Reds-If, Red-True/-False, and transitivity, we have
	  (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ⇝* ⟦N₁⟧ρ or ⟦N₂⟧ρ ∈ ⟦σ⟧ξ.
	  Then by CR2*, (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ.

Strong normalization holds as a corollary like before.

**Corollary** (strong normalization): If Γ ⊢ M : σ then M ∈ SN.
**Proof**: By soundness, unfolding the definition of semantic typing, we have
∀ρ, ξ, (∀x : τ ∈ Γ, ρ(x) ∈ ⟦τ⟧ξ) ⇒ M{ρ} ∈ ⟦σ⟧ξ.
Pick ρ(x) ↦ x and ξ(α) ↦ SAT. We need to show that ∀x : τ ∈ Γ, x ∈ ⟦τ⟧ξ.
By CR3, ⟦τ⟧ξ ⊆ SNe, so by SN-Var, x ∈ ⟦τ⟧ξ.
Then we have M ∈ ⟦σ⟧ξ ∈ CR, and by CR1, M ∈ SN.

## Normalization and infinite reductions

However, this proof of strong normalization is still stated using the inductive definition,
not the original statement of strong normalization,
which states that there are no infinite reduction sequences,
where the usual notion of reduction is single-step congruent β-reduction.
We can show that the former implies the latter,
assuming the corresponding antisubstitution property for the latter,
as well as various inversion properties.

**Proposition** (antisubstitution): If N and M{x ↦ N} have no infinite reduction sequences,
then M has no infinite reduction sequences.

**Proposition** (inversion): If M has no infinite reduction sequences,
then neither do its syntactic components.
For example, if (M N) has no infinite reduction sequences, then neither do M nor N.

**Lemma** (soundness of SN):
1. If M ∈ SN then M has no infinite reduction sequences.
2. If M ∈ SNe then M has no infinite reduction sequences.
3. If M ⇝ M' and M' has no infinite reduction sequences,
   then M has no infinite reduction sequences.
**Proof**: By mutual induction.
The first and second parts are fairly direct by the induction hypotheses.
We look at the third part in detail.
* Case SN-Red: We have M ⇝ N and N ∈ SN.
  By the first induction hypothesis, N has no infinite reduction sequences.
  Then by the third induction hypothesis, M has no infinite reduction sequeces.
* Case Red-β: We have ((λx. M) N) ⇝ M{x ↦ N} and N ∈ SN,
  where M{x ↦ N} has no infinite reduction sequences.
  By the first induction hypothesis, N has no infinite reduction sequences.
  By antisubstitution, M has no infinite reduction sequences,
  so neither does ((λx. M) N)
* Case Red-App: We have (M N) ⇝ (M' N) and M ⇝ M",
  where (M' N) has no infinite reduction sequences.
  By inversion, M', N have no infinite reduction sequences.
  By the third induction hypothesis, M has no infinite reduction sequences.
  Then (M N) has no infinite reduction sequence.
* Case Red-True: We have (if true then N₁ else N₂) ⇝ N₁ and N₂ ∈ SN,
  where N₁ has no infinite reduction sequences.
  By the first induction hypothesis, N₂ has no infinite reduction sequences.
  Then (if true then N₁ else N₂) has no infinite reduction sequences.
* Case Red-False: As above.
* Case Red-If: We have (if M then N₁ else N₂) ⇝ (if M' then N₁ else N₂) and M ⇝ M',
  where (if M' then N₁ else N₂) has no infinite reduction sequences.
  By inversion, M', N₁, and N₂ have no infinite reduction sequences.
  By the third induction hypothesis, M has no infinite reduction sequences.
  Then (if M then N₁ else N₂) has no infinite reduction sequences.

**Corollary** (no infinite reductions): If Γ ⊢ M : σ, then M has no infinite reduction sequences.

---

[^1]: Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. (2019). POPLMark reloaded: Mechanizing proofs by logical relations. Journal of Functional Programming, 29(e19). DOI:[10.1017/S0956796819000170](https://doi.org/10.1017/S0956796819000170 )