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