## § Strong normalization of STLC

- Recall that in the category Hask, objects are types, morphisms are functions/expressions.
- Recall that in the category of contexts, objects are contexts, morphisms are substitutions.
- A local predicate $L$ will relate to an object (type/context) a collection of morphisms (type → expressions of that type, typing context → substitutions of the variables of the typing context where the expressions have the type as per the context).
- Consider STLC with the typing rules:

```
------
Γ⊢():Unit
```

```
Γ ⊢ (f:A→B); Γ ⊢ (x:A)
----------------
Γ⊢ f@x:B
```

```
Γ,(a:A) ⊢ (body:B)
----------------
Γ ⊢ (λa.body:A→B)
```

- Define the logical prediate
`Ltype: Type → Set(Expression)`

, by induction on the rules:

```
--------------------------
() ∈ LType(Unit)
```

```
f ∈ LType(A→B); x∈LType(A)
--------------------------
f @ x ∈ LType(B)
```

```
body ∈ LType(B); (∀ aval∈ Ltype(A), body[a/aval] ∈ Ltype(B))
--------------------------
λa.body ∈ LType(A→B)
```

- It is clear that
`x ∈ LType(T)`

implies that `x`

is strongly normalizing. - When we try to prove that
`Γ ⊢ x : T`

implies `x ∈ LType(T)`

, we get stuck on the case of the lambda, because it's impossible to prove that a well typed term `(λa.body):A→B`

is such that upon substitution, `body[a/aval]`

will be strongly normalizing.

- So we control the context as well, and create another relatoin
`LCtx(Γ)`

. For a given context `Γ: Var → Type`

, we say that a substitution `γ: Var → Expr`

is in `LCtx(Γ)`

iff `dom(γ) = dom(Γ)`

, and that for all `x∈ dom(Γ)`

, that `γ(x) : Γ(x)`

and `γ(x) ∈ LType(Γ(x))`

. Maybe written with a little abuse of notation, this means that if `(x:T)∈ Γ`

, then `γ(x):T`

, and `γ(x)∈ LType(T)`

. That is, `γ`

is a set of assignments for the typing context `Γ`

where each assignment is strongly normalizing.